Documentation

TauCeti.Analysis.Distribution.SchwartzSpace.ZLattice

Summing Schwartz functions over a lattice #

A Schwartz function decays faster than every power of ‖x‖, while the power ‖x‖ ^ r is summable over a discrete subgroup L of a finite-dimensional real normed space as soon as r < -rank L (Mathlib's ZLattice.summable_norm_sub_rpow). Comparing the two, every translate ℓ ↦ f (v + ℓ) of a Schwartz function is absolutely summable over L. By Peetre's inequality 1 + ‖ℓ‖ ≤ (1 + ‖x‖) (1 + ‖x + ℓ‖) the domination is uniform for x in a ball, so the periodization x ↦ ∑' ℓ : L, f (x + ℓ) is continuous.

The summability of both sides and the continuity of the periodization are the analytic inputs to Poisson summation over a full lattice L in a finite-dimensional real inner product space, which is not proved here,

∑' ℓ : L, f (v + ℓ) = (covolume L)⁻¹ * ∑' m : L^∨, exp (2πi ⟪v, m⟫) • 𝓕 f m,

for a Schwartz function f. The lattice side is summable by the comparison above, and the dual side because the Fourier transform of a Schwartz function is again a Schwartz function and the phases exp (2πi ⟪v, m⟫) have norm one. Both are recorded on their own, in absolute form and in the plain form for a complete codomain, so that each side can be manipulated on its own.

Main statements #

source
theorem ZLattice.summable_norm_poisson_left {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : Submodule ℤ E) [DiscreteTopology ↥L] (f : SchwartzMap E F) (v : E) :
Summable fun (ℓ : ↥L) => ‖f (v + ↑ℓ)‖

The translates ℓ ↦ f (v + ℓ) of a Schwartz function are absolutely summable over a discrete subgroup L of a finite-dimensional real normed space.

source
theorem ZLattice.summable_poisson_left {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : Submodule ℤ E) [DiscreteTopology ↥L] [CompleteSpace F] (f : SchwartzMap E F) (v : E) :
Summable fun (ℓ : ↥L) => f (v + ↑ℓ)

The translates ℓ ↦ f (v + ℓ) of a Schwartz function with values in a Banach space are summable over a discrete subgroup L of a finite-dimensional real normed space.

source
theorem ZLattice.summable_one_add_norm_pow_mul_norm {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : Submodule ℤ E) [DiscreteTopology ↥L] (f : SchwartzMap E F) (k : ℕ) :
Summable fun (ℓ : ↥L) => (1 + ‖↑ℓ‖) ^ k * ‖f ↑ℓ‖

On a discrete subgroup L of a finite-dimensional real normed space, a Schwartz function decays faster than every power of 1 + ‖ℓ‖: the family ℓ ↦ (1 + ‖ℓ‖) ^ k * ‖f ℓ‖ is summable for every k.

source
theorem ZLattice.exists_summable_forall_norm_poisson_left_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : Submodule ℤ E) [DiscreteTopology ↥L] (f : SchwartzMap E F) (R : ℝ) :
∃ (u : ↥L → ℝ), Summable u ∧ ∀ (ℓ : ↥L), ∀ x ∈ Metric.closedBall 0 R, ‖f (x + ↑ℓ)‖ ≤ u ℓ

The translates ℓ ↦ f (x + ℓ) of a Schwartz function are dominated, uniformly for x in a closed ball, by a single summable family over a discrete subgroup L.

source
theorem ZLattice.continuous_tsum_poisson_left {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (L : Submodule ℤ E) [DiscreteTopology ↥L] [CompleteSpace F] (f : SchwartzMap E F) :
Continuous fun (x : E) => ∑' (ℓ : ↥L), f (x + ↑ℓ)

The periodization x ↦ ∑' ℓ : L, f (x + ℓ) of a Schwartz function over a discrete subgroup L is continuous.

source
theorem ZLattice.summable_norm_poisson_right_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (f : SchwartzMap E F) (v : E) :
Summable fun (m : ↥(dual L)) => ‖Complex.exp (2 * ↑Real.pi * Complex.I * ↑(inner ℝ v ↑m)) • FourierTransform.fourier ⇑f ↑m‖

The Fourier transform of a Schwartz function, twisted by the phases exp (2πi ⟪v, m⟫), is absolutely summable over the dual L^∨ of a full lattice L: the dual side of Poisson summation.

source
theorem ZLattice.summable_poisson_right_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℂ F] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] [CompleteSpace F] (f : SchwartzMap E F) (v : E) :
Summable fun (m : ↥(dual L)) => Complex.exp (2 * ↑Real.pi * Complex.I * ↑(inner ℝ v ↑m)) • FourierTransform.fourier ⇑f ↑m

The Fourier transform of a Schwartz function with values in a complex Banach space, twisted by the phases exp (2πi ⟪v, m⟫), is summable over the dual L^∨ of a full lattice L.

source
theorem ZLattice.summable_norm_poisson_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (f : SchwartzMap E ℂ) (v : E) :
Summable fun (m : ↥(dual L)) => ‖FourierTransform.fourier ⇑f ↑m * Complex.exp (2 * ↑Real.pi * Complex.I * ↑(inner ℝ v ↑m))‖

The Fourier transform of a complex-valued Schwartz function, times the phases exp (2πi ⟪v, m⟫), is absolutely summable over the dual L^∨ of a full lattice L.

source
theorem ZLattice.summable_poisson_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (f : SchwartzMap E ℂ) (v : E) :
Summable fun (m : ↥(dual L)) => FourierTransform.fourier ⇑f ↑m * Complex.exp (2 * ↑Real.pi * Complex.I * ↑(inner ℝ v ↑m))

The Fourier transform of a complex-valued Schwartz function, times the phases exp (2πi ⟪v, m⟫), is summable over the dual L^∨ of a full lattice L: the dual side of Poisson summation.