instance instNonemptyFin {d : ℕ} [Fact (0 < d)] : Nonempty (Fin d)

def PSF_Conditions {d : ℕ} (f : EuclideanSpace ℝ (Fin d) → ℂ) : Prop

Equations

• PSF_Conditions f = (Summable f ∧ sorry)

theorem PSF_L {d : ℕ} [Fact (0 < d)] (Λ : Submodule ℤ (EuclideanSpace ℝ (Fin d))) [DiscreteTopology ↥Λ] [IsZLattice ℝ Λ] {f : EuclideanSpace ℝ (Fin d) → ℂ} (hf : PSF_Conditions f) (v : EuclideanSpace ℝ (Fin d)) : ∑' (ℓ : ↥Λ), f (v + ↑ℓ) = 1 / ↑(ZLattice.covolume Λ MeasureTheory.volume) * ∑' (m : ↥(bilinFormOfRealInner.dualSubmodule Λ)), Real.fourierIntegral f ↑m * Complex.exp (2 * ↑Real.pi * Complex.I * ↑(RCLike.wInner 1 v ((WithLp.equiv 2 ((i : Fin d) → (fun (x : Fin d) => ℝ) i)) ↑m)))

theorem PSF_L' {d : ℕ} [Fact (0 < d)] (Λ : Submodule ℤ (EuclideanSpace ℝ (Fin d))) [DiscreteTopology ↥Λ] [IsZLattice ℝ Λ] {f : EuclideanSpace ℝ (Fin d) → ℂ} (hf : PSF_Conditions f) : ∑' (ℓ : ↥Λ), f ↑ℓ = 1 / ↑(ZLattice.covolume Λ MeasureTheory.volume) * ∑' (m : ↥(bilinFormOfRealInner.dualSubmodule Λ)), Real.fourierIntegral f ↑m

theorem SchwartzMap.PoissonSummation_Lattices {d : ℕ} [Fact (0 < d)] (Λ : Submodule ℤ (EuclideanSpace ℝ (Fin d))) [DiscreteTopology ↥Λ] [IsZLattice ℝ Λ] (f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ) (v : EuclideanSpace ℝ (Fin d)) : ∑' (ℓ : ↥Λ), f (v + ↑ℓ) = 1 / ↑(ZLattice.covolume Λ MeasureTheory.volume) * ∑' (m : ↥(bilinFormOfRealInner.dualSubmodule Λ)), Real.fourierIntegral ⇑f ↑m * Complex.exp (2 * ↑Real.pi * Complex.I * ↑(RCLike.wInner 1 v ((WithLp.equiv 2 ((i : Fin d) → (fun (x : Fin d) => ℝ) i)) ↑m)))

@[simp]

theorem SchwartzMap.fourierInversion (𝕜 : Type u_1) [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] [CompleteSpace E] {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (f : SchwartzMap V E) : Real.fourierIntegralInv (Real.fourierIntegral ⇑f) = ⇑f

theorem Continuous.pos_iff_exists_nhd_pos {E : Type u_1} [TopologicalSpace E] {f : E → ℝ} (hf₁ : Continuous f) (x : E) : 0 < f x ↔ ∃ U ∈ nhds x, ∀ y ∈ U, 0 < f y

theorem Continuous.pos_iff_exists_measurable_nhd_pos {E : Type u_1} [TopologicalSpace E] [MeasureTheory.MeasureSpace E] [BorelSpace E] {f : E → ℝ} (hf₁ : Continuous f) (x : E) : 0 < f x ↔ ∃ U ∈ nhds x, MeasurableSet U ∧ ∀ y ∈ U, 0 < f y

instance instIsOpenPosMeasureVolume_spherePacking {E : Type u_1} [NormedAddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [MeasureTheory.MeasureSpace E] [BorelSpace E] [MeasureTheory.volume.IsAddLeftInvariant] [MeasureTheory.volume.Regular] [NeZero MeasureTheory.volume] : MeasureTheory.volume.IsOpenPosMeasure

theorem Continuous.integral_zero_iff_zero_of_nonneg {E : Type u_1} [NormedAddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [MeasureTheory.MeasureSpace E] [BorelSpace E] [MeasureTheory.volume.IsAddLeftInvariant] [MeasureTheory.volume.Regular] [NeZero MeasureTheory.volume] {f : E → ℝ} (hf₁ : Continuous f) (hf₂ : MeasureTheory.Integrable f MeasureTheory.volume) (hnn : ∀ (x : E), 0 ≤ f x) : ∫ (v : E), f v = 0 ↔ f = 0

theorem SchwartzMap.toFun_eq_zero_iff_zero {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) : ⇑f = 0 ↔ f = 0

theorem SchwartzMap.integral_zero_iff_zero_of_nonneg {d : ℕ} {f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℝ} (hnn : ∀ (x : EuclideanSpace ℝ (Fin d)), 0 ≤ f x) : ∫ (v : EuclideanSpace ℝ (Fin d)), f v = 0 ↔ f = 0

instance instDecidableEqEuclideanSpaceRealFinOfNat_spherePacking {d : ℕ} (v : EuclideanSpace ℝ (Fin d)) : Decidable (v = 0)

Equations

• instDecidableEqEuclideanSpaceRealFinOfNat_spherePacking v = Classical.propDecidable (v = 0)

instance instDecidableEqEuclideanSpaceRealFin_spherePacking {d : ℕ} : DecidableEq (EuclideanSpace ℝ (Fin d))

Equations

• instDecidableEqEuclideanSpaceRealFin_spherePacking = Classical.typeDecidableEq (EuclideanSpace ℝ (Fin d))

theorem Complex.exp_neg_real_I_eq_conj {d : ℕ} (x m : EuclideanSpace ℝ (Fin d)) : exp (-(2 * ↑Real.pi * I * ↑(RCLike.wInner 1 x m))) = (starRingEnd ℂ) (exp (2 * ↑Real.pi * I * ↑(RCLike.wInner 1 x m)))