Lumenary.HarmonicAnalysis

Formal library

• roots_of_unity_sumtheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **Orthogonality of characters on `ℤ/N`.** If `z^N = 1` and `z ≠ 1`, then
  `1 + z + ⋯ + z^{N-1} = 0`. Proof: `(∑ zᵏ)(z − 1) = z^N − 1 = 0` and `z − 1 ≠ 0`. With
  `z = e^{2πi(m−n)/N}` this says the discrete exponentials are orthogonal — the finite model of
  Fourier series and the basis of the fast Fourier transform. -/
  theorem roots_of_unity_sum {z : ℂ} {N : ℕ} (hz : z ^ N = 1) (hz1 : z ≠ 1) :
      ∑ k ∈ Finset.range N, z ^ k = 0 := by
    have h : (∑ k ∈ Finset.range N, z ^ k) * (z - 1) = 0 := by
      rw [geom_sum_mul, hz, sub_self]
    exact (mul_eq_zero.mp h).resolve_right (sub_ne_zero.mpr hz1)

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HarmonicAnalysis.leanTry it in the Lean web editor

• orthonormal_exponentialstheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **The exponentials are orthonormal** in `L²` of the circle `ℝ/Tℤ` with normalised Haar
  measure: `⟪eₘ, eₙ⟫ = δₘₙ` for `eₙ(x) = e^{2πinx/T}`. This is Mathlib's `orthonormal_fourier`;
  `span_fourierLp_closure_eq_top` adds that their span is dense, so they form a Hilbert basis. -/
  theorem orthonormal_exponentials (T : ℝ) [Fact (0 < T)] :
      Orthonormal ℂ (fun n : ℤ => fourierLp (T := T) 2 n) :=
    orthonormal_fourier

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HarmonicAnalysis.leanTry it in the Lean web editor

• parsevaltheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **Parseval's identity.** For `f ∈ L²(ℝ/Tℤ)`, `∑ₙ |f̂(n)|² = ∫ |f|²` (normalised measure).
  This is Mathlib's `hasSum_sq_fourierCoeff`, a consequence of the exponentials forming a Hilbert
  basis. -/
  theorem parseval (T : ℝ) [Fact (0 < T)] (f : Lp ℂ 2 (@AddCircle.haarAddCircle T _)) :
      HasSum (fun n : ℤ => ‖fourierCoeff f n‖ ^ 2)
        (∫ t : AddCircle T, ‖f t‖ ^ 2 ∂AddCircle.haarAddCircle) :=
    hasSum_sq_fourierCoeff f

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HarmonicAnalysis.leanTry it in the Lean web editor

• fourier_coeff_tendsto_zerotheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **Riemann–Lebesgue lemma for `L²` functions on the circle**, from Parseval: the series
  `∑ |f̂(n)|²` converges, so its terms tend to `0` (along the cofinite filter, i.e. as `|n| → ∞`),
  and hence so do the coefficients `f̂(n) = √(|f̂(n)|²)`. -/
  theorem fourier_coeff_tendsto_zero (T : ℝ) [Fact (0 < T)]
      (f : Lp ℂ 2 (@AddCircle.haarAddCircle T _)) :
      Tendsto (fun n : ℤ => fourierCoeff f n) cofinite (𝓝 0) := by
    have hsq : Tendsto (fun n : ℤ => ‖fourierCoeff f n‖ ^ 2) cofinite (𝓝 0) :=
      (parseval T f).summable.tendsto_cofinite_zero
    have hnorm : Tendsto (fun n : ℤ => ‖fourierCoeff f n‖) cofinite (𝓝 0) := by
      have h := (Real.continuous_sqrt.tendsto 0).comp hsq
      rw [Real.sqrt_zero] at h
      refine h.congr fun n => ?_
      simp only [Function.comp_apply, Real.sqrt_sq (norm_nonneg _)]
    exact tendsto_zero_iff_norm_tendsto_zero.mpr hnorm

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HarmonicAnalysis.leanTry it in the Lean web editor

• riemann_lebesguetheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **Riemann–Lebesgue lemma** on `ℝ`: for integrable `f`, `f̂(ξ) = ∫ e^{−2πixξ} f(x) dx → 0`
  as `|ξ| → ∞`. This applies Mathlib's `tendsto_integral_exp_inner_smul_cocompact` (stated on any
  finite-dimensional real inner product space; for `ℝ` the cocompact filter is `|ξ| → ∞`). -/
  theorem riemann_lebesgue (f : ℝ → ℂ) :
      Tendsto (fun ξ : ℝ => ∫ x : ℝ, 𝐞 (-(ξ * x)) • f x) (cocompact ℝ) (𝓝 0) := by
    simpa using tendsto_integral_exp_inner_smul_cocompact f

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HarmonicAnalysis.leanTry it in the Lean web editor

• fourier_boundtheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **The Fourier transform is bounded from `L¹` to `L^∞`:** `|f̂(ξ)| ≤ ∫ |f|` for every `ξ`,
  because `|∫ g| ≤ ∫ |g|` and the character `e^{−2πixξ}` has modulus `1`. (For non-integrable `f`
  both sides are `0` under Lean's convention for the Bochner integral.) -/
  theorem fourier_bound (f : ℝ → ℂ) (ξ : ℝ) :
      ‖∫ x : ℝ, 𝐞 (-(ξ * x)) • f x‖ ≤ ∫ x : ℝ, ‖f x‖ := by
    calc ‖∫ x : ℝ, 𝐞 (-(ξ * x)) • f x‖ ≤ ∫ x : ℝ, ‖𝐞 (-(ξ * x)) • f x‖ :=
          norm_integral_le_integral_norm _
      _ = ∫ x : ℝ, ‖f x‖ := by
          congr 1
          ext x
          simp

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HarmonicAnalysis.leanTry it in the Lean web editor

• planchereltheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **Plancherel's theorem.** The Fourier transform, defined on `L¹ ∩ L²` and extended by
  continuity, is an isometry of `L²(ℝ)`: `‖𝓕 f‖₂ = ‖f‖₂` (indeed a unitary map, with inverse the
  conjugate transform). This is Mathlib's `MeasureTheory.Lp.norm_fourier_eq`. -/
  theorem plancherel (f : Lp (α := ℝ) ℂ 2) : ‖𝓕 f‖ = ‖f‖ :=
    Lp.norm_fourier_eq f

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HarmonicAnalysis.leanTry it in the Lean web editor

• gaussian_self_dualtheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **The Gaussian `e^{−πx²}` is its own Fourier transform**, with the normalisation
  `f̂(ξ) = ∫ f(x) e^{−2πixξ} dx`. Obtained from Mathlib's `fourier_gaussian_pi`, which computes the
  transform of `e^{−πbx²}` for `Re b > 0`, by setting `b = 1` and simplifying `1/1^{1/2} = 1`. -/
  theorem gaussian_self_dual :
      (𝓕 fun x : ℝ => cexp (-π * x ^ 2)) = fun ξ : ℝ => cexp (-π * ξ ^ 2) := by
    have h := fourier_gaussian_pi (b := 1) (by simp)
    simpa using h

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HarmonicAnalysis.leanTry it in the Lean web editor

• poisson_summationtheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **Poisson summation formula.** For a Schwartz function `f` on `ℝ`,
  `∑ₙ f(x + n) = ∑ₖ f̂(k) e^{2πikx}`; at `x = 0`, `∑ f(n) = ∑ f̂(k)`. The left side is a
  `1`-periodic function whose Fourier coefficients are the `f̂(k)`. This is Mathlib's
  `SchwartzMap.tsum_eq_tsum_fourier`. -/
  theorem poisson_summation (f : SchwartzMap ℝ ℂ) (x : ℝ) :
      ∑' n : ℤ, f (x + n) = ∑' k : ℤ, 𝓕 f k * fourier k (x : UnitAddCircle) :=
    SchwartzMap.tsum_eq_tsum_fourier f x

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HarmonicAnalysis.leanTry it in the Lean web editor

• theta_functional_equationtheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **Jacobi's theta functional equation** `θ(−1/τ) = (−iτ)^{1/2} θ(τ)` for
  `θ(τ) = ∑ₙ e^{πin²τ}` on the upper half-plane — Poisson summation applied to a Gaussian. Riemann
  derived the functional equation of `ζ(s)` from it. This is Mathlib's `jacobiTheta_S_smul`. -/
  theorem theta_functional_equation (τ : UpperHalfPlane) :
      jacobiTheta ↑(ModularGroup.S • τ) = (-I * τ) ^ (1 / 2 : ℂ) * jacobiTheta τ :=
    jacobiTheta_S_smul τ

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HarmonicAnalysis.leanTry it in the Lean web editor

• baseltheoremApplies a library theorempropext, Classical.choice, Quot.sound

  /-- **`∑ 1/n² = π²/6`**, which Mathlib proves with Fourier series (Parseval applied to Bernoulli
  polynomials). The `n = 0` term is `1/0 = 0` in Lean's conventions. This is Mathlib's
  `hasSum_zeta_two`. -/
  theorem basel : HasSum (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 2) (π ^ 2 / 6) :=
    hasSum_zeta_two

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/HarmonicAnalysis.leanTry it in the Lean web editor