5.3. Mathlib candidates: integral and Fourier tools🔗

Analytic tools that support Radon inversion and invariant integration: Schwartz sections, polar coordinates, the Dirichlet integral, Gaussian Schwartz estimates, and the Hilbert-transform symbol.

Integral and Fourier tools

Theorem5.3.1

Statement uses 2

Statement dependency previews

Preview

Theorem 5.2.3

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Radon sections of Schwartz functions are Schwartz. For a Schwartz function f on E and a unit direction u, the section \mathscr Rf(u,\cdot) equals the Schwartz function \mathcal F^{-1}[\omega\mapsto\mathcal Ff(\omega u)] (last declaration). The slice \omega\mapsto\mathcal Ff(\omega u) is Schwartz because the ray map \omega\mapsto\omega u is temperate and antilipschitz (SchwartzMap.compCLMOfAntilipschitz), so its inverse Fourier transform is Schwartz; the Fourier slice theorem identifies the two Fourier transforms, almost-everywhere Fourier inversion (upstream-candidate mathlib_fourier_inversion_ae) turns this into almost-everywhere equality, and continuity of both sides upgrades it to equality everywhere. Continuity of the section (second declaration) is dominated convergence with the Japanese-bracket dominator, available uniformly in the offset because a point of the line \mathbb Ru and a point of (\mathbb Ru)^\perp are orthogonal, whence \|pu+y\|\ge\|y\|; the Schwartz decay is used in the form \|f(x)\|\le C(1+\|x\|)^{-k} (first declaration). This is what makes one-dimensional Schwartz theory — in particular Fourier multipliers such as the filter of filtered backprojection — available on Radon sections.

Lean code for Theorem5.3.1●5 declarations

theoremdefined in LeanRidgelet/ToMathlib/RadonTransform.lean

complete

theorem MeasureTheory.schwartz_norm_le_one_add_norm_rpow.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : SchwartzMap E ℂ)
  (k : ℕ) : ∃ C, ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ (-↑k)

theorem MeasureTheory.schwartz_norm_le_one_add_norm_rpow.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (f : SchwartzMap E ℂ) (k : ℕ) :
  ∃ C,
    ∀ (x : E),
      ‖f x‖ ≤ C * (1 + ‖x‖) ^ (-↑k)

Schwartz decay in Japanese-bracket form: `‖f x‖ ≤ C (1 + ‖x‖)^{-k}`.

theoremdefined in LeanRidgelet/ToMathlib/RadonTransform.lean

complete

theorem MeasureTheory.continuous_radonTransform_schwartz.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (f : SchwartzMap E ℂ) (u : E) :
  Continuous (MeasureTheory.radonTransform (⇑f) u)

theorem MeasureTheory.continuous_radonTransform_schwartz.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (f : SchwartzMap E ℂ) (u : E) :
  Continuous
    (MeasureTheory.radonTransform (⇑f) u)

The Radon section of a Schwartz function is continuous.

defdefined in LeanRidgelet/ToMathlib/RadonTransform.lean

complete

def MeasureTheory.radonSchwartzSection.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (f : SchwartzMap E ℂ) {u : E}
  (hu : ‖u‖ = 1) : SchwartzMap ℝ ℂ

def MeasureTheory.radonSchwartzSection.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (f : SchwartzMap E ℂ) {u : E}
  (hu : ‖u‖ = 1) : SchwartzMap ℝ ℂ

Implementation after :=

:=
  𝓕⁻ (SchwartzMap.compCLMOfAntilipschitz (𝕜 := ℝ) (hasTemperateGrowth_smul_right u)
    (antilipschitzWith_smul_right hu) (𝓕 f))

The Radon section of a Schwartz function, realized as a Schwartz function: the inverse
Fourier transform of the Fourier slice `ω ↦ 𝓕 f (ω • u)`.

theoremdefined in LeanRidgelet/ToMathlib/RadonTransform.lean

complete

theorem MeasureTheory.fourier_radonSchwartzSection.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (f : SchwartzMap E ℂ) {u : E}
  (hu : ‖u‖ = 1) :
  FourierTransform.fourier ⇑(MeasureTheory.radonSchwartzSection f hu) =
    fun ω ↦ FourierTransform.fourier (⇑f) (ω • u)

theorem MeasureTheory.fourier_radonSchwartzSection.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (f : SchwartzMap E ℂ) {u : E}
  (hu : ‖u‖ = 1) :
  FourierTransform.fourier
      ⇑(MeasureTheory.radonSchwartzSection
          f hu) =
    fun ω ↦
    FourierTransform.fourier (⇑f) (ω • u)

theoremdefined in LeanRidgelet/ToMathlib/RadonTransform.lean

complete

theorem MeasureTheory.radonTransform_eq_radonSchwartzSection.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  (f : SchwartzMap E ℂ) {u : E} (hu : ‖u‖ = 1) :
  MeasureTheory.radonTransform (⇑f) u =
    ⇑(MeasureTheory.radonSchwartzSection f hu)

theorem MeasureTheory.radonTransform_eq_radonSchwartzSection.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (f : SchwartzMap E ℂ) {u : E}
  (hu : ‖u‖ = 1) :
  MeasureTheory.radonTransform (⇑f) u =
    ⇑(MeasureTheory.radonSchwartzSection f
        hu)

**The Radon section of a Schwartz function is a Schwartz function**: for every unit
direction, `R[f](u, ·)` coincides with the Schwartz function `radonSchwartzSection f hu`. The
proof identifies their Fourier transforms by the Fourier slice theorem, concludes almost
everywhere equality by Fourier inversion, and upgrades it to everywhere equality by
continuity.

Theorem5.3.2

uses 0

Used by 6

Reverse dependency previews

Preview

Theorem 2.1.18

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Polar coordinates for the Bochner integral. Mathlib's Measure.toSphere and Measure.measurePreserving_homeomorphUnitSphereProd give the polar decomposition of an additive Haar measure, but the integral formula is recorded only for radial integrands (integral_fun_norm_addHaar). The general formula \int_EF\,d\mu=\int_{\mathbb S}\int_0^\infty r^{d-1}F(ru)\,dr\,d\mu_{\mathbb S}(u),\qquad d=\dim E, is proved here by the same route: restrict to E∖{0}, transport along the polar homeomorphism (product form, first declaration), transport integrability (second declaration), and unwind the density of Measure.volumeIoiPow after Fubini (iterated form).

Lean code for Theorem5.3.2●15 declarations

theoremdefined in LeanRidgelet/ToMathlib/PolarCoordinates.lean

complete

theorem MeasureTheory.integral_eq_integral_prod_toSphere.{u_1, u_2}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasurableSpace E] {G : Type u_2} [NormedAddCommGroup G]
  [NormedSpace ℝ G] [Nontrivial E] (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E] [μ.IsAddHaarMeasure]
  (F : E → G) :
  ∫ (x : E), F x ∂μ =
    ∫ (p : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
      F
        (↑p.2 •
          ↑p.1) ∂μ.toSphere.prod
        (MeasureTheory.Measure.volumeIoiPow (Module.finrank ℝ E - 1))

theorem MeasureTheory.integral_eq_integral_prod_toSphere.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E]
  {G : Type u_2} [NormedAddCommGroup G]
  [NormedSpace ℝ G] [Nontrivial E]
  (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E]
  [μ.IsAddHaarMeasure] (F : E → G) :
  ∫ (x : E), F x ∂μ =
    ∫ (p :
      ↑(Metric.sphere 0 1) ×
        ↑(Set.Ioi 0)),
      F
        (↑p.2 •
          ↑p.1) ∂μ.toSphere.prod
        (MeasureTheory.Measure.volumeIoiPow
          (Module.finrank ℝ E - 1))

**Polar coordinates**, product form: the Bochner integral over a nontrivial
finite-dimensional normed space with an additive Haar measure equals the integral over
`sphere × (0, ∞)` of `F (r • u)` against `μ.toSphere.prod (volumeIoiPow (dim E - 1))`.

theoremdefined in LeanRidgelet/ToMathlib/PolarCoordinates.lean

complete

theorem MeasureTheory.integrable_prod_toSphere_of_integrable.{u_1, u_2}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasurableSpace E] {G : Type u_2} [NormedAddCommGroup G]
  (μ : MeasureTheory.Measure E) [FiniteDimensional ℝ E] [BorelSpace E]
  [μ.IsAddHaarMeasure] {F : E → G} (hF : MeasureTheory.Integrable F μ) :
  MeasureTheory.Integrable (fun p ↦ F (↑p.2 • ↑p.1))
    (μ.toSphere.prod
      (MeasureTheory.Measure.volumeIoiPow (Module.finrank ℝ E - 1)))

theorem MeasureTheory.integrable_prod_toSphere_of_integrable.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E]
  {G : Type u_2} [NormedAddCommGroup G]
  (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E]
  [μ.IsAddHaarMeasure] {F : E → G}
  (hF : MeasureTheory.Integrable F μ) :
  MeasureTheory.Integrable
    (fun p ↦ F (↑p.2 • ↑p.1))
    (μ.toSphere.prod
      (MeasureTheory.Measure.volumeIoiPow
        (Module.finrank ℝ E - 1)))

Integrability in polar coordinates.

theoremdefined in LeanRidgelet/ToMathlib/PolarCoordinates.lean

complete

theorem MeasureTheory.integrable_volumeIoiPow_iff.{u_2} {G : Type u_2}
  [NormedAddCommGroup G] [NormedSpace ℝ G] (n : ℕ) (H : ℝ → G) :
  MeasureTheory.Integrable (fun r ↦ H ↑r)
      (MeasureTheory.Measure.volumeIoiPow n) ↔
    MeasureTheory.IntegrableOn (fun r ↦ r ^ n • H r) (Set.Ioi 0)
      MeasureTheory.volume

theorem MeasureTheory.integrable_volumeIoiPow_iff.{u_2}
  {G : Type u_2} [NormedAddCommGroup G]
  [NormedSpace ℝ G] (n : ℕ) (H : ℝ → G) :
  MeasureTheory.Integrable (fun r ↦ H ↑r)
      (MeasureTheory.Measure.volumeIoiPow
        n) ↔
    MeasureTheory.IntegrableOn
      (fun r ↦ r ^ n • H r) (Set.Ioi 0)
      MeasureTheory.volume

Integrability against `volumeIoiPow n` is integrability against the density `r ^ n`, the
integrability counterpart of `MeasureTheory.integral_volumeIoiPow`.

theoremdefined in LeanRidgelet/ToMathlib/PolarCoordinates.lean

complete

theorem MeasureTheory.ae_integrableOn_Ioi_of_integrable.{u_1, u_2}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasurableSpace E] {G : Type u_2} [NormedAddCommGroup G]
  [NormedSpace ℝ G] (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E] [μ.IsAddHaarMeasure]
  {F : E → G} (hF : MeasureTheory.Integrable F μ) :
  ∀ᵐ (u : ↑(Metric.sphere 0 1)) ∂μ.toSphere,
    MeasureTheory.IntegrableOn
      (fun r ↦ r ^ (Module.finrank ℝ E - 1) • F (r • ↑u)) (Set.Ioi 0)
      MeasureTheory.volume

theorem MeasureTheory.ae_integrableOn_Ioi_of_integrable.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E]
  {G : Type u_2} [NormedAddCommGroup G]
  [NormedSpace ℝ G]
  (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E]
  [μ.IsAddHaarMeasure] {F : E → G}
  (hF : MeasureTheory.Integrable F μ) :
  ∀ᵐ (u :
    ↑(Metric.sphere 0 1)) ∂μ.toSphere,
    MeasureTheory.IntegrableOn
      (fun r ↦
        r ^ (Module.finrank ℝ E - 1) •
          F (r • ↑u))
      (Set.Ioi 0) MeasureTheory.volume

**Almost every radial section of an integrable function is integrable on the positive
half-line.** The polar decomposition of an integrable function is integrable on the product
`sphere × (0, ∞)`, so almost every fibre over the sphere is integrable.

theoremdefined in LeanRidgelet/ToMathlib/PolarCoordinates.lean

complete

theorem MeasureTheory.integral_eq_integral_toSphere_integral_Ioi.{u_1, u_2}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasurableSpace E] {G : Type u_2} [NormedAddCommGroup G]
  [NormedSpace ℝ G] [Nontrivial E] (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E] [μ.IsAddHaarMeasure]
  {F : E → G} (hF : MeasureTheory.Integrable F μ) :
  ∫ (x : E), F x ∂μ =
    ∫ (u : ↑(Metric.sphere 0 1)),
      ∫ (r : ℝ) in Set.Ioi 0,
        r ^ (Module.finrank ℝ E - 1) • F (r • ↑u) ∂μ.toSphere

theorem MeasureTheory.integral_eq_integral_toSphere_integral_Ioi.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E]
  {G : Type u_2} [NormedAddCommGroup G]
  [NormedSpace ℝ G] [Nontrivial E]
  (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E]
  [μ.IsAddHaarMeasure] {F : E → G}
  (hF : MeasureTheory.Integrable F μ) :
  ∫ (x : E), F x ∂μ =
    ∫ (u : ↑(Metric.sphere 0 1)),
      ∫ (r : ℝ) in Set.Ioi 0,
        r ^ (Module.finrank ℝ E - 1) •
          F (r • ↑u) ∂μ.toSphere

**Polar coordinates**, iterated form: `∫ F = ∫_{sphere} ∫_{r > 0} r^{d-1} F (r • u) dr du`.

defdefined in LeanRidgelet/ToMathlib/PolarCoordinates.lean

complete

def MeasureTheory.sphereNeg.{u_3} (E : Type u_3) [NormedAddCommGroup E] :
  ↑(Metric.sphere 0 1) → ↑(Metric.sphere 0 1)

def MeasureTheory.sphereNeg.{u_3}
  (E : Type u_3) [NormedAddCommGroup E] :
  ↑(Metric.sphere 0 1) →
    ↑(Metric.sphere 0 1)

Implementation after :=

:=
  fun u => ⟨-(u : E), by simp⟩

The antipodal map on the unit sphere.

theoremdefined in LeanRidgelet/ToMathlib/PolarCoordinates.lean

complete

theorem MeasureTheory.map_sphereNeg_toSphere.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E]
  (μ : MeasureTheory.Measure E) [FiniteDimensional ℝ E] [BorelSpace E]
  [μ.IsAddHaarMeasure] :
  MeasureTheory.Measure.map (MeasureTheory.sphereNeg E) μ.toSphere =
    μ.toSphere

theorem MeasureTheory.map_sphereNeg_toSphere.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E]
  (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E]
  [μ.IsAddHaarMeasure] :
  MeasureTheory.Measure.map
      (MeasureTheory.sphereNeg E)
      μ.toSphere =
    μ.toSphere

**The sphere measure is invariant under the antipodal map.** Mathlib computes
`Measure.toSphere` but records none of its symmetries; this one follows from the invariance of an
additive Haar measure under negation, because the cone over the reflected set is the reflection of
the cone.

theoremdefined in LeanRidgelet/ToMathlib/PolarCoordinates.lean

complete

theorem MeasureTheory.integral_sphereNeg.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E]
  {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G]
  (μ : MeasureTheory.Measure E) [FiniteDimensional ℝ E] [BorelSpace E]
  [μ.IsAddHaarMeasure] (F : ↑(Metric.sphere 0 1) → G) :
  ∫ (u : ↑(Metric.sphere 0 1)),
      F (MeasureTheory.sphereNeg E u) ∂μ.toSphere =
    ∫ (u : ↑(Metric.sphere 0 1)), F u ∂μ.toSphere

theorem MeasureTheory.integral_sphereNeg.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E]
  {G : Type u_2} [NormedAddCommGroup G]
  [NormedSpace ℝ G]
  (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E]
  [μ.IsAddHaarMeasure]
  (F : ↑(Metric.sphere 0 1) → G) :
  ∫ (u : ↑(Metric.sphere 0 1)),
      F
        (MeasureTheory.sphereNeg E
          u) ∂μ.toSphere =
    ∫ (u : ↑(Metric.sphere 0 1)),
      F u ∂μ.toSphere

Integration against the sphere measure is invariant under the antipodal map.

theoremdefined in LeanRidgelet/ToMathlib/PolarCoordinates.lean

complete

theorem MeasureTheory.integral_eq_integral_toSphere_integral_Iio.{u_1, u_2}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasurableSpace E] {G : Type u_2} [NormedAddCommGroup G]
  [NormedSpace ℝ G] [Nontrivial E] (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E] [μ.IsAddHaarMeasure]
  {F : E → G} (hF : MeasureTheory.Integrable F μ) :
  ∫ (x : E), F x ∂μ =
    ∫ (u : ↑(Metric.sphere 0 1)),
      ∫ (r : ℝ) in Set.Iio 0,
        |r| ^ (Module.finrank ℝ E - 1) • F (r • ↑u) ∂μ.toSphere

theorem MeasureTheory.integral_eq_integral_toSphere_integral_Iio.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E]
  {G : Type u_2} [NormedAddCommGroup G]
  [NormedSpace ℝ G] [Nontrivial E]
  (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E]
  [μ.IsAddHaarMeasure] {F : E → G}
  (hF : MeasureTheory.Integrable F μ) :
  ∫ (x : E), F x ∂μ =
    ∫ (u : ↑(Metric.sphere 0 1)),
      ∫ (r : ℝ) in Set.Iio 0,
        |r| ^ (Module.finrank ℝ E - 1) •
          F (r • ↑u) ∂μ.toSphere

The polar formula with the radial variable on the negative axis. The sphere measure does not
see the reflection, so the negative half-line contributes the whole integral again.

theoremdefined in LeanRidgelet/ToMathlib/PolarCoordinates.lean

complete

theorem MeasureTheory.ae_integrableOn_Iio_of_integrable.{u_1, u_2}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasurableSpace E] {G : Type u_2} [NormedAddCommGroup G]
  [NormedSpace ℝ G] (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E] [μ.IsAddHaarMeasure]
  {F : E → G} (hF : MeasureTheory.Integrable F μ) :
  ∀ᵐ (u : ↑(Metric.sphere 0 1)) ∂μ.toSphere,
    MeasureTheory.IntegrableOn
      (fun r ↦ |r| ^ (Module.finrank ℝ E - 1) • F (r • ↑u)) (Set.Iio 0)
      MeasureTheory.volume

theorem MeasureTheory.ae_integrableOn_Iio_of_integrable.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E]
  {G : Type u_2} [NormedAddCommGroup G]
  [NormedSpace ℝ G]
  (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E]
  [μ.IsAddHaarMeasure] {F : E → G}
  (hF : MeasureTheory.Integrable F μ) :
  ∀ᵐ (u :
    ↑(Metric.sphere 0 1)) ∂μ.toSphere,
    MeasureTheory.IntegrableOn
      (fun r ↦
        |r| ^ (Module.finrank ℝ E - 1) •
          F (r • ↑u))
      (Set.Iio 0) MeasureTheory.volume

Almost every radial section is integrable on the negative half-line too: the sphere measure
does not see the antipodal map, so the statement transports from the positive half-line by
`r ↦ -r`.

theoremdefined in LeanRidgelet/ToMathlib/PolarCoordinates.lean

complete

theorem MeasureTheory.ae_integrable_radial_of_integrable.{u_1, u_2}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasurableSpace E] {G : Type u_2} [NormedAddCommGroup G]
  [NormedSpace ℝ G] (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E] [μ.IsAddHaarMeasure]
  {F : E → G} (hF : MeasureTheory.Integrable F μ) :
  ∀ᵐ (u : ↑(Metric.sphere 0 1)) ∂μ.toSphere,
    MeasureTheory.Integrable
      (fun r ↦ |r| ^ (Module.finrank ℝ E - 1) • F (r • ↑u))
      MeasureTheory.volume

theorem MeasureTheory.ae_integrable_radial_of_integrable.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E]
  {G : Type u_2} [NormedAddCommGroup G]
  [NormedSpace ℝ G]
  (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E]
  [μ.IsAddHaarMeasure] {F : E → G}
  (hF : MeasureTheory.Integrable F μ) :
  ∀ᵐ (u :
    ↑(Metric.sphere 0 1)) ∂μ.toSphere,
    MeasureTheory.Integrable
      (fun r ↦
        |r| ^ (Module.finrank ℝ E - 1) •
          F (r • ↑u))
      MeasureTheory.volume

**The radial section of an integrable function is integrable, at almost every direction.** Both
half-lines together, which is what the two-sided polar formula below needs.

theoremdefined in LeanRidgelet/ToMathlib/PolarCoordinates.lean

complete

theorem MeasureTheory.integral_eq_integral_toSphere_integral_two_sided.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasurableSpace E] {G : Type u_2} [NormedAddCommGroup G]
  [NormedSpace ℝ G] [Nontrivial E] (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E] [μ.IsAddHaarMeasure]
  {F : E → G} (hF : MeasureTheory.Integrable F μ) :
  2 • ∫ (x : E), F x ∂μ =
    ∫ (u : ↑(Metric.sphere 0 1)),
      ∫ (r : ℝ), |r| ^ (Module.finrank ℝ E - 1) • F (r • ↑u) ∂μ.toSphere

theorem MeasureTheory.integral_eq_integral_toSphere_integral_two_sided.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E]
  {G : Type u_2} [NormedAddCommGroup G]
  [NormedSpace ℝ G] [Nontrivial E]
  (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E]
  [μ.IsAddHaarMeasure] {F : E → G}
  (hF : MeasureTheory.Integrable F μ) :
  2 • ∫ (x : E), F x ∂μ =
    ∫ (u : ↑(Metric.sphere 0 1)),
      ∫ (r : ℝ),
        |r| ^ (Module.finrank ℝ E - 1) •
          F (r • ↑u) ∂μ.toSphere

**The two-sided polar formula.** With the radial variable running over all of `ℝ` against the
weight `|r|^{d-1}`, the polar integral computes twice the integral. This is the form that matches
a scale parameter ranging over a full Euclidean space rather than over a half-line, and the factor
`2` is exactly the double cover `(r, u) ↦ r • u` of `E ∖ {0}` by `ℝ ∖ {0} × 𝕊`.

theoremdefined in LeanRidgelet/ToMathlib/PolarCoordinates.lean

complete

theorem MeasureTheory.lintegral_eq_lintegral_prod_toSphere.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E]
  [Nontrivial E] (μ : MeasureTheory.Measure E) [FiniteDimensional ℝ E]
  [BorelSpace E] [μ.IsAddHaarMeasure] (F : E → ENNReal) :
  ∫⁻ (x : E), F x ∂μ =
    ∫⁻ (p : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)),
      F
        (↑p.2 •
          ↑p.1) ∂μ.toSphere.prod
        (MeasureTheory.Measure.volumeIoiPow (Module.finrank ℝ E - 1))

theorem MeasureTheory.lintegral_eq_lintegral_prod_toSphere.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E]
  [Nontrivial E]
  (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E]
  [μ.IsAddHaarMeasure] (F : E → ENNReal) :
  ∫⁻ (x : E), F x ∂μ =
    ∫⁻ (p :
      ↑(Metric.sphere 0 1) ×
        ↑(Set.Ioi 0)),
      F
        (↑p.2 •
          ↑p.1) ∂μ.toSphere.prod
        (MeasureTheory.Measure.volumeIoiPow
          (Module.finrank ℝ E - 1))

**Polar coordinates for the lower Lebesgue integral**, product form. No hypothesis at all: the
polar map is a measurable equivalence and both sides of the change of variables are unsigned.

theoremdefined in LeanRidgelet/ToMathlib/PolarCoordinates.lean

complete

theorem MeasureTheory.lintegral_volumeIoiPow (n : ℕ) {H : ℝ → ENNReal}
  (hH : Measurable H) :
  ∫⁻ (r : ↑(Set.Ioi 0)), H ↑r ∂MeasureTheory.Measure.volumeIoiPow n =
    ∫⁻ (r : ℝ) in Set.Ioi 0, ENNReal.ofReal (r ^ n) * H r

theorem MeasureTheory.lintegral_volumeIoiPow
  (n : ℕ) {H : ℝ → ENNReal}
  (hH : Measurable H) :
  ∫⁻ (r : ↑(Set.Ioi 0)),
      H
        ↑r ∂MeasureTheory.Measure.volumeIoiPow
        n =
    ∫⁻ (r : ℝ) in Set.Ioi 0,
      ENNReal.ofReal (r ^ n) * H r

The lower Lebesgue integral against `volumeIoiPow n` is the one against the density `r ^ n`,
the unsigned counterpart of `MeasureTheory.integral_volumeIoiPow`.

theoremdefined in LeanRidgelet/ToMathlib/PolarCoordinates.lean

complete

theorem MeasureTheory.lintegral_eq_lintegral_toSphere_lintegral_Ioi.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasurableSpace E] [Nontrivial E] (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E] [μ.IsAddHaarMeasure]
  {F : E → ENNReal} (hF : Measurable F) :
  ∫⁻ (x : E), F x ∂μ =
    ∫⁻ (u : ↑(Metric.sphere 0 1)),
      ∫⁻ (r : ℝ) in Set.Ioi 0,
        ENNReal.ofReal (r ^ (Module.finrank ℝ E - 1)) *
          F (r • ↑u) ∂μ.toSphere

theorem MeasureTheory.lintegral_eq_lintegral_toSphere_lintegral_Ioi.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E]
  [Nontrivial E]
  (μ : MeasureTheory.Measure E)
  [FiniteDimensional ℝ E] [BorelSpace E]
  [μ.IsAddHaarMeasure] {F : E → ENNReal}
  (hF : Measurable F) :
  ∫⁻ (x : E), F x ∂μ =
    ∫⁻ (u : ↑(Metric.sphere 0 1)),
      ∫⁻ (r : ℝ) in Set.Ioi 0,
        ENNReal.ofReal
            (r ^
              (Module.finrank ℝ E - 1)) *
          F (r • ↑u) ∂μ.toSphere

**Polar coordinates for the lower Lebesgue integral**, iterated form:
`∫⁻ F = ∫⁻_{sphere} ∫⁻_{r > 0} r^{d-1} F (r • u) dr du`. Measurability of the integrand is the only
hypothesis; this is Tonelli, so there is nothing to assume about convergence.

The same two forms hold for the lower Lebesgue integral, and there the product form needs no hypothesis at all and the iterated form only measurability, both reductions being Tonelli rather than Fubini. That is the form an absolute convergence statement has to be proved with: deciding whether a product integrand is integrable means computing the integral of its norm, and that computation may not presuppose what it is meant to establish.

The fibrewise counterpart is here too: for an integrable F, almost every radial section r\mapsto|r|^{d-1}F(ru) is itself integrable on \mathbb R. It follows from the product integrability by Fubini on the positive half-line, and on the negative half-line by transporting along r\mapsto-r together with invariance of the sphere measure under the antipodal map. This is what keeps the iterated formulas free of any hypothesis beyond integrability of F, and in particular it is what makes the two-sided form below unconditional.

Invariance of the sphere measure under the antipodal map is itself missing from Mathlib, which records how Measure.toSphere is computed but none of its symmetries. It is what turns the polar formula above, whose radial variable runs over (0,\infty), into the two-sided form whose radial variable runs over all of \mathbb R at the cost of a factor 2 — the double cover (r,u)\mapsto ru of E\setminus\{0\}. That two-sided form is the one that matches a scale parameter ranging over a full Euclidean space, and it is what the d-plane reconstruction formula at codimension one evaluates its direction integral with.

Theorem5.3.3

uses 0used by 1✓L∃∀N

The Dirichlet integral. Mathlib knows Real.sinc and its elementary bounds but not the Dirichlet integral \int_0^\infty\frac{\sin t}{t}\,dt=\frac\pi2, which exists only as an improper integral. It is proved here (first declaration) by the Laplace representation 1/t=\int_0^\infty e^{-ut}\,du, Fubini on (0,R]\times(0,\infty) (absolutely convergent because |\sin t|\le t), the elementary primitive of t\mapsto e^{-ut}\sin t, the arctangent integral \int_0^\infty du/(1+u^2)=\pi/2, and the O(1/R) bound on the error term. Conditionally convergent Fourier computations need two companions, also proved here: the uniform bound |\int_a^b\sin u/u\,du|\le3 for all 0\le a\le b (second declaration; short intervals by |\sin u/u|\le1, long ones by integration by parts, which gives \le2/a for a\ge1), and the tail \int_a^\infty\sin u/u\,du as the explicit function \pi/2-\int_0^a\sin u/u\,du with its limit description, uniform bound and limit \pi/2 as a\to0 (remaining declarations, including the scaling and oddness relation in the frequency variable).

Lean code for Theorem5.3.3●7 declarations

theoremdefined in LeanRidgelet/ToMathlib/DirichletIntegral.lean

complete

theorem MeasureTheory.tendsto_intervalIntegral_sin_div_atTop :
  Filter.Tendsto (fun R ↦ ∫ (t : ℝ) in 0..R, Real.sin t / t)
    Filter.atTop (nhds (Real.pi / 2))

theorem MeasureTheory.tendsto_intervalIntegral_sin_div_atTop :
  Filter.Tendsto
    (fun R ↦
      ∫ (t : ℝ) in 0..R, Real.sin t / t)
    Filter.atTop (nhds (Real.pi / 2))

**The Dirichlet integral**: `∫₀^R sin t / t dt → π/2` as `R → ∞`.

theoremdefined in LeanRidgelet/ToMathlib/DirichletIntegral.lean

complete

theorem MeasureTheory.abs_intervalIntegral_sin_div_le {a b : ℝ} (ha : 0 ≤ a)
  (hab : a ≤ b) : |∫ (u : ℝ) in a..b, Real.sin u / u| ≤ 3

theorem MeasureTheory.abs_intervalIntegral_sin_div_le
  {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) :
  |∫ (u : ℝ) in a..b, Real.sin u / u| ≤ 3

**Uniform bound on the partial Dirichlet integrals**: `|∫_a^b sin u / u du| ≤ 3` for all
`0 ≤ a ≤ b`.

defdefined in LeanRidgelet/ToMathlib/DirichletIntegral.lean

complete

def MeasureTheory.sinDivTail (a : ℝ) : ℝ

def MeasureTheory.sinDivTail (a : ℝ) : ℝ

Implementation after :=

:= Real.pi / 2 - ∫ u in (0 : ℝ)..a, Real.sin u / u

The tail of the Dirichlet integral, `∫_a^∞ sin u / u du`, expressed through the Dirichlet
value `π/2`.

theoremdefined in LeanRidgelet/ToMathlib/DirichletIntegral.lean

complete

theorem MeasureTheory.tendsto_intervalIntegral_sin_div_atTop_left (a : ℝ) :
  Filter.Tendsto (fun R ↦ ∫ (u : ℝ) in a..R, Real.sin u / u)
    Filter.atTop (nhds (MeasureTheory.sinDivTail a))

theorem MeasureTheory.tendsto_intervalIntegral_sin_div_atTop_left
  (a : ℝ) :
  Filter.Tendsto
    (fun R ↦
      ∫ (u : ℝ) in a..R, Real.sin u / u)
    Filter.atTop
    (nhds (MeasureTheory.sinDivTail a))

The tail is the limit of the partial integrals `∫_a^R sin u / u du` as `R → ∞`.

theoremdefined in LeanRidgelet/ToMathlib/DirichletIntegral.lean

complete

theorem MeasureTheory.abs_sinDivTail_le {a : ℝ} (ha : 0 ≤ a) :
  |MeasureTheory.sinDivTail a| ≤ 3

theorem MeasureTheory.abs_sinDivTail_le {a : ℝ}
  (ha : 0 ≤ a) :
  |MeasureTheory.sinDivTail a| ≤ 3

The Dirichlet tail is uniformly bounded.

theoremdefined in LeanRidgelet/ToMathlib/DirichletIntegral.lean

complete

theorem MeasureTheory.tendsto_sinDivTail_nhds_zero :
  Filter.Tendsto MeasureTheory.sinDivTail (nhds 0) (nhds (Real.pi / 2))

theorem MeasureTheory.tendsto_sinDivTail_nhds_zero :
  Filter.Tendsto MeasureTheory.sinDivTail
    (nhds 0) (nhds (Real.pi / 2))

The Dirichlet tail tends to the Dirichlet value `π/2` as the inner cut-off shrinks.

theoremdefined in LeanRidgelet/ToMathlib/DirichletIntegral.lean

complete

theorem MeasureTheory.intervalIntegral_sin_mul_div_eq (ω : ℝ) (hω : ω ≠ 0)
  (ε R : ℝ) (hε : 0 < ε) (hεR : ε ≤ R) :
  ∫ (t : ℝ) in ε..R, Real.sin (t * ω) / t =
    ω.sign * ∫ (u : ℝ) in ε * |ω|..R * |ω|, Real.sin u / u

theorem MeasureTheory.intervalIntegral_sin_mul_div_eq
  (ω : ℝ) (hω : ω ≠ 0) (ε R : ℝ)
  (hε : 0 < ε) (hεR : ε ≤ R) :
  ∫ (t : ℝ) in ε..R,
      Real.sin (t * ω) / t =
    ω.sign *
      ∫ (u : ℝ) in ε * |ω|..R * |ω|,
        Real.sin u / u

Scaling and oddness of the partial Dirichlet integrals in the frequency variable.

Theorem5.3.4

uses 0used by 1✓L∃∀N

The Gaussian as a Schwartz function. Mathlib has the Gaussian integral and the Fourier transform of a Gaussian, but no realization of z\mapsto e^{-z^2/2} as an element of Schwartz space. Two ingredients: every derivative is a polynomial multiple of the Gaussian, G^{(n)}=p_nG with p_0=1 and p_{n+1}=p_n'-Xp_n (fifth declaration, by induction on the product rule); and every power is dominated by the Gaussian, |x|^de^{-x^2/2}\le1+2^dd! (second declaration, from x^d/d!\le e^x), whence (1+|x|)^Ne^{-x^2/2}\le2^N(1+2^NN!) (third). With the crude polynomial bound |p(z)|\le C(1+|z|)^d (fourth) these give the Schwartz seminorm estimates directly, since in one variable the norm of the iterated Fréchet derivative is the norm of the iterated derivative.

Lean code for Theorem5.3.4●6 declarations

theoremdefined in LeanRidgelet/ToMathlib/GaussianSchwartz.lean

complete

theorem Real.pow_mul_exp_neg_le_factorial (d : ℕ) {t : ℝ} (ht : 0 ≤ t) :
  t ^ d * Real.exp (-t) ≤ ↑d.factorial

theorem Real.pow_mul_exp_neg_le_factorial (d : ℕ)
  {t : ℝ} (ht : 0 ≤ t) :
  t ^ d * Real.exp (-t) ≤ ↑d.factorial

`t^d e^{-t} ≤ d!` for `t ≥ 0`, from the exponential series.

theoremdefined in LeanRidgelet/ToMathlib/GaussianSchwartz.lean

complete

theorem Real.abs_pow_mul_exp_neg_sq_div_two_le (d : ℕ) (x : ℝ) :
  |x| ^ d * Real.exp (-x ^ 2 / 2) ≤ 1 + 2 ^ d * ↑d.factorial

theorem Real.abs_pow_mul_exp_neg_sq_div_two_le
  (d : ℕ) (x : ℝ) :
  |x| ^ d * Real.exp (-x ^ 2 / 2) ≤
    1 + 2 ^ d * ↑d.factorial

Every power is dominated by the Gaussian: `|x|^d e^{-x²/2} ≤ 1 + 2^d d!`.

theoremdefined in LeanRidgelet/ToMathlib/GaussianSchwartz.lean

complete

theorem Real.one_add_abs_pow_mul_exp_neg_sq_div_two_le (N : ℕ) (x : ℝ) :
  (1 + |x|) ^ N * Real.exp (-x ^ 2 / 2) ≤
    2 ^ N * (1 + 2 ^ N * ↑N.factorial)

theorem Real.one_add_abs_pow_mul_exp_neg_sq_div_two_le
  (N : ℕ) (x : ℝ) :
  (1 + |x|) ^ N * Real.exp (-x ^ 2 / 2) ≤
    2 ^ N * (1 + 2 ^ N * ↑N.factorial)

`(1 + |x|)^N e^{-x²/2} ≤ 2^N (1 + 2^N N!)`.

theoremdefined in LeanRidgelet/ToMathlib/GaussianSchwartz.lean

complete

theorem Real.exists_bound_polynomial_eval (p : Polynomial ℝ) :
  ∃ C d, 0 ≤ C ∧ ∀ (z : ℝ), |Polynomial.eval z p| ≤ C * (1 + |z|) ^ d

theorem Real.exists_bound_polynomial_eval
  (p : Polynomial ℝ) :
  ∃ C d,
    0 ≤ C ∧
      ∀ (z : ℝ),
        |Polynomial.eval z p| ≤
          C * (1 + |z|) ^ d

A crude polynomial bound: `|p(z)| ≤ C (1 + |z|)^d`.

theoremdefined in LeanRidgelet/ToMathlib/GaussianSchwartz.lean

complete

theorem Real.exists_polynomial_iteratedDeriv_gaussian (n : ℕ) :
  ∃ p,
    ∀ (z : ℝ),
      iteratedDeriv n (fun w ↦ ↑(Real.exp (-w ^ 2 / 2))) z =
        ↑(Polynomial.eval z p * Real.exp (-z ^ 2 / 2))

theorem Real.exists_polynomial_iteratedDeriv_gaussian
  (n : ℕ) :
  ∃ p,
    ∀ (z : ℝ),
      iteratedDeriv n
          (fun w ↦
            ↑(Real.exp (-w ^ 2 / 2)))
          z =
        ↑(Polynomial.eval z p *
            Real.exp (-z ^ 2 / 2))

Every derivative of the Gaussian is a polynomial multiple of it, with the recursion
`p_0 = 1`, `p_{n+1} = p_n' - X p_n`.

defdefined in LeanRidgelet/ToMathlib/GaussianSchwartz.lean

complete

def Real.gaussianSchwartz : SchwartzMap ℝ ℂ

def Real.gaussianSchwartz : SchwartzMap ℝ ℂ

Implementation after :=

:= fun z => ((Real.exp (-z ^ 2 / 2) : ℝ) : ℂ)
  smooth' := by
    have h : ContDiff ℝ (⊤ : ℕ∞) (fun z : ℝ => Real.exp (-z ^ 2 / 2)) := by fun_prop
    exact Complex.ofRealCLM.contDiff.comp h
  decay' := by
    intro k n
    obtain ⟨p, hp⟩ := exists_polynomial_iteratedDeriv_gaussian n
    obtain ⟨C, d, hC, hbound⟩ := exists_bound_polynomial_eval p
    refine ⟨C * (2 ^ (k + d) * (1 + 2 ^ (k + d) * ((k + d).factorial : ℝ))), fun z => ?_⟩
    have hz0 : (0 : ℝ) ≤ |z| := abs_nonneg z
    have hexp0 : (0 : ℝ) < Real.exp (-z ^ 2 / 2) := Real.exp_pos _
    have hnorm : ‖iteratedFDeriv ℝ n (fun w : ℝ => ((Real.exp (-w ^ 2 / 2) : ℝ) : ℂ)) z‖
        = |p.eval z| * Real.exp (-z ^ 2 / 2) := by
      rw [norm_iteratedFDeriv_eq_norm_iteratedDeriv, hp z, Complex.norm_real, Real.norm_eq_abs,
        abs_mul, abs_of_pos hexp0]
    rw [hnorm, Real.norm_eq_abs]
    -- `|z|^k |p(z)| ≤ C (1+|z|)^{k+d}`
    have hpoly : |z| ^ k * |p.eval z| ≤ C * (1 + |z|) ^ (k + d) := by
      have h1 : |z| ^ k ≤ (1 + |z|) ^ k :=
        pow_le_pow_left₀ (abs_nonneg z) (by linarith) k
      calc |z| ^ k * |p.eval z| ≤ (1 + |z|) ^ k * (C * (1 + |z|) ^ d) :=
            mul_le_mul h1 (hbound z) (abs_nonneg _) (by positivity)
        _ = C * (1 + |z|) ^ (k + d) := by rw [pow_add]; ring
    have hgauss := one_add_abs_pow_mul_exp_neg_sq_div_two_le (k + d) z
    calc |z| ^ k * (|p.eval z| * Real.exp (-z ^ 2 / 2))
        = (|z| ^ k * |p.eval z|) * Real.exp (-z ^ 2 / 2) := by ring
      _ ≤ (C * (1 + |z|) ^ (k + d)) * Real.exp (-z ^ 2 / 2) :=
          mul_le_mul_of_nonneg_right hpoly hexp0.le
      _ = C * ((1 + |z|) ^ (k + d) * Real.exp (-z ^ 2 / 2)) := by ring
      _ ≤ C * (2 ^ (k + d) * (1 + 2 ^ (k + d) * ((k + d).factorial : ℝ))) :=
          mul_le_mul_of_nonneg_left hgauss hC

The Gaussian `z ↦ e^{-z²/2}` as a complex-valued Schwartz function.

Theorem5.3.5

Statement uses 2

Statement dependency previews

Preview

Theorem 5.2.4

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Definition 2.1.4

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The Hilbert transform and its Fourier symbol. Mathlib has no Hilbert transform. Defined here in the classical normalization \mathscr Hg(x)=\frac1\pi\,\mathrm{p.v.}\int g(t)/(x-t)\,dt (so \mathscr H^2=-1), with its Fourier symbol on Schwartz functions, \mathscr Hg=\mathcal F^{-1}\big[-i\,\mathrm{sign}(\xi)\,\mathcal Fg\big] (the symbol is homogeneous of degree 0, hence identical in every Fourier normalization). Three steps. The truncated integral is first rewritten as the absolutely convergent integral of the odd difference quotient (g(x-s)-g(x+s))/s over (\varepsilon,\infty). Next, on a doubly truncated domain \varepsilon<s<R — the outer cut-off is unavoidable, since the Hilbert kernel is not integrable at infinity and Fubini would fail — Fourier inversion and Fubini produce the partial Dirichlet integral \int_\varepsilon^R\sin(2\pi s\xi)/s\,ds as symbol. Two dominated-convergence passes against the uniform Dirichlet bound then send R\to\infty (symbol: the Dirichlet tail) and \varepsilon\to0 (symbol: -i\,\mathrm{sign}\,\xi, by the Dirichlet integral). In particular the principal-value limit exists at every point of a Schwartz function. Integrability. The last four declarations prove that \mathscr Hg\in L^1 whenever g is Schwartz with \int g=0 — the transform is only O(1/x) in general, so the hypothesis is needed. Taking the limit \varepsilon\to0 in the first step exhibits \mathscr Hg as an absolutely convergent integral of the odd difference quotient over (0,\infty), and from that form the commutator identity x\,\mathscr Hg(x)=\mathscr H\big(t\mapsto t\,g(t)\big)(x)+\tfrac1\pi\int g is the pointwise algebra xg(t)/(x-t)=tg(t)/(x-t)+g(t). With \int g=0 it says that x\,\mathscr Hg is again the Hilbert transform of a Schwartz function; both are square-integrable because the symbol is unimodular and Plancherel applies, and away from the origin \|\mathscr Hg(x)\|=|x|^{-1}\|x\,\mathscr Hg(x)\|\le(1+x^2)^{-1}+\|x\,\mathscr Hg(x)\|^2 by the arithmetic--geometric mean inequality.

Lean code for Theorem5.3.5●11 declarations

defdefined in LeanRidgelet/ToMathlib/HilbertTransform.lean

complete

def MeasureTheory.pvHilbertTransform (g : ℝ → ℂ) (x : ℝ) : ℂ

def MeasureTheory.pvHilbertTransform
  (g : ℝ → ℂ) (x : ℝ) : ℂ

Implementation after :=

:=
  Filter.limUnder (𝓝[>] (0 : ℝ)) fun ε =>
    (1 / (Real.pi : ℂ)) * ∫ t in {t : ℝ | ε < |x - t|}, g t / ((x : ℂ) - (t : ℂ))

The principal-value Hilbert transform in the classical normalization
`𝓗 g (x) = (1/π) p.v. ∫ g t / (x - t) dt`.

theoremdefined in LeanRidgelet/ToMathlib/HilbertTransform.lean

complete

theorem MeasureTheory.setIntegral_hilbert_eq_Ioi (f : SchwartzMap ℝ ℂ) (x : ℝ)
  {ε : ℝ} (hε : 0 < ε) :
  ∫ (t : ℝ) in {t | ε < |x - t|}, f t / (↑x - ↑t) =
    ∫ (s : ℝ) in Set.Ioi ε, (f (x - s) - f (x + s)) / ↑s

theorem MeasureTheory.setIntegral_hilbert_eq_Ioi
  (f : SchwartzMap ℝ ℂ) (x : ℝ) {ε : ℝ}
  (hε : 0 < ε) :
  ∫ (t : ℝ) in {t | ε < |x - t|},
      f t / (↑x - ↑t) =
    ∫ (s : ℝ) in Set.Ioi ε,
      (f (x - s) - f (x + s)) / ↑s

The truncated Hilbert integral as the integral of the odd difference quotient.

theoremdefined in LeanRidgelet/ToMathlib/HilbertTransform.lean

complete

theorem MeasureTheory.intervalIntegral_hilbert_eq_fourier (f : SchwartzMap ℝ ℂ)
  (x : ℝ) {ε R : ℝ} (hε : 0 < ε) (hεR : ε ≤ R) :
  ∫ (s : ℝ) in ε..R, (f (x - s) - f (x + s)) / ↑s =
    ∫ (ξ : ℝ),
      -2 * Complex.I *
          ↑(∫ (s : ℝ) in ε..R, Real.sin (s * (2 * Real.pi * ξ)) / s) *
        (Complex.exp (↑(2 * Real.pi * (x * ξ)) * Complex.I) *
          FourierTransform.fourier (⇑f) ξ)

theorem MeasureTheory.intervalIntegral_hilbert_eq_fourier
  (f : SchwartzMap ℝ ℂ) (x : ℝ) {ε R : ℝ}
  (hε : 0 < ε) (hεR : ε ≤ R) :
  ∫ (s : ℝ) in ε..R,
      (f (x - s) - f (x + s)) / ↑s =
    ∫ (ξ : ℝ),
      -2 * Complex.I *
          ↑(∫ (s : ℝ) in ε..R,
              Real.sin
                  (s *
                    (2 * Real.pi * ξ)) /
                s) *
        (Complex.exp
            (↑(2 * Real.pi * (x * ξ)) *
              Complex.I) *
          FourierTransform.fourier (⇑f) ξ)

The truncated Hilbert integral of a Schwartz function on the Fourier side: the truncated
kernel contributes the partial Dirichlet integral.

theoremdefined in LeanRidgelet/ToMathlib/HilbertTransform.lean

complete

theorem MeasureTheory.setIntegral_hilbert_eq_fourier_tail (f : SchwartzMap ℝ ℂ)
  (x : ℝ) {ε : ℝ} (hε : 0 < ε) :
  ∫ (t : ℝ) in {t | ε < |x - t|}, f t / (↑x - ↑t) =
    ∫ (ξ : ℝ),
      -2 * Complex.I *
          ↑((2 * Real.pi * ξ).sign *
              MeasureTheory.sinDivTail (ε * |2 * Real.pi * ξ|)) *
        (Complex.exp (↑(2 * Real.pi * (x * ξ)) * Complex.I) *
          FourierTransform.fourier (⇑f) ξ)

theorem MeasureTheory.setIntegral_hilbert_eq_fourier_tail
  (f : SchwartzMap ℝ ℂ) (x : ℝ) {ε : ℝ}
  (hε : 0 < ε) :
  ∫ (t : ℝ) in {t | ε < |x - t|},
      f t / (↑x - ↑t) =
    ∫ (ξ : ℝ),
      -2 * Complex.I *
          ↑((2 * Real.pi * ξ).sign *
              MeasureTheory.sinDivTail
                (ε * |2 * Real.pi * ξ|)) *
        (Complex.exp
            (↑(2 * Real.pi * (x * ξ)) *
              Complex.I) *
          FourierTransform.fourier (⇑f) ξ)

The Fourier representation of the `ε`-truncated Hilbert integral of a Schwartz function.

theoremdefined in LeanRidgelet/ToMathlib/HilbertTransform.lean

complete

theorem MeasureTheory.pvHilbertTransform_schwartz (f : SchwartzMap ℝ ℂ)
  (x : ℝ) :
  MeasureTheory.pvHilbertTransform (⇑f) x =
    ∫ (ξ : ℝ),
      -Complex.I * ↑ξ.sign *
        (Complex.exp (↑(2 * Real.pi * (x * ξ)) * Complex.I) *
          FourierTransform.fourier (⇑f) ξ)

theorem MeasureTheory.pvHilbertTransform_schwartz
  (f : SchwartzMap ℝ ℂ) (x : ℝ) :
  MeasureTheory.pvHilbertTransform (⇑f)
      x =
    ∫ (ξ : ℝ),
      -Complex.I * ↑ξ.sign *
        (Complex.exp
            (↑(2 * Real.pi * (x * ξ)) *
              Complex.I) *
          FourierTransform.fourier (⇑f) ξ)

**The Fourier symbol of the Hilbert transform**: on Schwartz functions the principal-value
Hilbert transform is the Fourier multiplier `-i sign ξ`.

theoremdefined in LeanRidgelet/ToMathlib/HilbertTransform.lean

complete

theorem MeasureTheory.pvHilbertTransform_schwartz_eq_fourierInv
  (f : SchwartzMap ℝ ℂ) (x : ℝ) :
  MeasureTheory.pvHilbertTransform (⇑f) x =
    FourierTransformInv.fourierInv
      (fun ξ ↦ -Complex.I * ↑ξ.sign * FourierTransform.fourier (⇑f) ξ) x

theorem MeasureTheory.pvHilbertTransform_schwartz_eq_fourierInv
  (f : SchwartzMap ℝ ℂ) (x : ℝ) :
  MeasureTheory.pvHilbertTransform (⇑f)
      x =
    FourierTransformInv.fourierInv
      (fun ξ ↦
        -Complex.I * ↑ξ.sign *
          FourierTransform.fourier (⇑f) ξ)
      x

**The Fourier symbol of the Hilbert transform**, in terms of Mathlib's inverse Fourier
integral: `𝓗 f = 𝓕⁻ (-i sign ⬝ 𝓕 f)` for every Schwartz function `f`.

theoremdefined in LeanRidgelet/ToMathlib/HilbertTransform.lean

complete

theorem MeasureTheory.integrableOn_schwartz_oddDiff (f : SchwartzMap ℝ ℂ)
  (x : ℝ) :
  MeasureTheory.IntegrableOn (fun s ↦ (f (x - s) - f (x + s)) / ↑s)
    (Set.Ioi 0) MeasureTheory.volume

theorem MeasureTheory.integrableOn_schwartz_oddDiff
  (f : SchwartzMap ℝ ℂ) (x : ℝ) :
  MeasureTheory.IntegrableOn
    (fun s ↦ (f (x - s) - f (x + s)) / ↑s)
    (Set.Ioi 0) MeasureTheory.volume

The odd difference quotient of a Schwartz function is integrable on the positive half-line:
near `0` it is bounded by twice the Lipschitz constant, and at infinity by the function itself.

theoremdefined in LeanRidgelet/ToMathlib/HilbertTransform.lean

complete

theorem MeasureTheory.pvHilbertTransform_schwartz_eq_oddIntegral
  (f : SchwartzMap ℝ ℂ) (x : ℝ) :
  MeasureTheory.pvHilbertTransform (⇑f) x =
    1 / ↑Real.pi * ∫ (s : ℝ) in Set.Ioi 0, (f (x - s) - f (x + s)) / ↑s

theorem MeasureTheory.pvHilbertTransform_schwartz_eq_oddIntegral
  (f : SchwartzMap ℝ ℂ) (x : ℝ) :
  MeasureTheory.pvHilbertTransform (⇑f)
      x =
    1 / ↑Real.pi *
      ∫ (s : ℝ) in Set.Ioi 0,
        (f (x - s) - f (x + s)) / ↑s

**The principal value of the Hilbert transform of a Schwartz function is an absolutely
convergent integral** of the odd difference quotient over the positive half-line.

theoremdefined in LeanRidgelet/ToMathlib/HilbertTransform.lean

complete

theorem MeasureTheory.coord_mul_pvHilbertTransform (g h : SchwartzMap ℝ ℂ)
  (hgh : ∀ (t : ℝ), h t = ↑t * g t) (x : ℝ) :
  ↑x * MeasureTheory.pvHilbertTransform (⇑g) x =
    MeasureTheory.pvHilbertTransform (⇑h) x +
      1 / ↑Real.pi * ∫ (t : ℝ), g t

theorem MeasureTheory.coord_mul_pvHilbertTransform
  (g h : SchwartzMap ℝ ℂ)
  (hgh : ∀ (t : ℝ), h t = ↑t * g t)
  (x : ℝ) :
  ↑x *
      MeasureTheory.pvHilbertTransform
        (⇑g) x =
    MeasureTheory.pvHilbertTransform (⇑h)
        x +
      1 / ↑Real.pi * ∫ (t : ℝ), g t

**The commutator identity for the Hilbert transform**: multiplying by the coordinate turns
`𝓗 g` into the Hilbert transform of `t g(t)`, up to the total mass of `g`. It is the pointwise
identity `x g(t)/(x - t) = t g(t)/(x - t) + g(t)`.

theoremdefined in LeanRidgelet/ToMathlib/HilbertTransform.lean

complete

theorem MeasureTheory.memLp_two_pvHilbertTransform (f : SchwartzMap ℝ ℂ) :
  MeasureTheory.MemLp (MeasureTheory.pvHilbertTransform ⇑f) 2
    MeasureTheory.volume

theorem MeasureTheory.memLp_two_pvHilbertTransform
  (f : SchwartzMap ℝ ℂ) :
  MeasureTheory.MemLp
    (MeasureTheory.pvHilbertTransform ⇑f)
    2 MeasureTheory.volume

**The Hilbert transform of a Schwartz function is square-integrable.** On the Fourier side it
is multiplication by the unimodular symbol `-i sign ξ`, so Plancherel applies.

theoremdefined in LeanRidgelet/ToMathlib/HilbertTransform.lean

complete

theorem MeasureTheory.integrable_pvHilbertTransform_of_integral_eq_zero
  (g : SchwartzMap ℝ ℂ) (hg : ∫ (t : ℝ), g t = 0) :
  MeasureTheory.Integrable (MeasureTheory.pvHilbertTransform ⇑g)
    MeasureTheory.volume

theorem MeasureTheory.integrable_pvHilbertTransform_of_integral_eq_zero
  (g : SchwartzMap ℝ ℂ)
  (hg : ∫ (t : ℝ), g t = 0) :
  MeasureTheory.Integrable
    (MeasureTheory.pvHilbertTransform ⇑g)
    MeasureTheory.volume

**The Hilbert transform of a Schwartz function with vanishing integral is integrable.**

The Hilbert transform of a Schwartz function is only `O(1/x)` in general; the hypothesis
`∫ g = 0` kills the leading term and improves the decay to `O(1/x²)`. The proof does not estimate
the decay directly: by `coord_mul_pvHilbertTransform` the function `x ↦ x 𝓗g(x)` is again the
Hilbert transform of a Schwartz function, hence square-integrable, and away from the origin
`‖𝓗g x‖ = |x|⁻¹ ‖x 𝓗g x‖ ≤ (1 + x²)⁻¹ + ‖x 𝓗g x‖²` by the arithmetic--geometric mean
inequality.