5.2. Mathlib candidates: Radon and Fourier transforms🔗

The Radon transform, its L¹ theory and slice theorem, together with the Fourier-analysis bridges that Mathlib's integral and L² APIs currently lack.

Radon transform

Definition5.2.1

uses 0

Used by 5

Reverse dependency previews

Preview

Definition 2.1.3

Loading preview

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

✓L∃∀N

Radon transform, dual Radon transform, and the line–hyperplane splitting. On a finite-dimensional real inner product space E with values in a normed space, \mathscr Rf(u,p)=\int_{(\mathbb Ru)^\perp}f(pu+y)\,dy,\qquad \mathscr R^\dagger\Phi(x)=\int_{\mathbb S}\Phi(u,\langle u,x\rangle)\,du, where the hyperplane carries its canonical Lebesgue measure and the unit sphere the surface measure volume.toSphere. For a unit vector u, the parametrization (p,y)\mapsto pu+y of E by the line \mathbb Ru and its orthogonal complement is packaged as a measurable equivalence, assembled from the WithLp 2 product coordinates and the orthogonal decomposition E\simeq\mathbb Ru\times_2(\mathbb Ru)^\perp.

Lean code for Definition5.2.1●3 definitions

defdefined in LeanRidgelet/ToMathlib/RadonTransform.lean

complete

def MeasureTheory.radonTransform.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (u : E) (p : ℝ) :
  F

def MeasureTheory.radonTransform.{u_1, u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {F : Type u_2} [NormedAddCommGroup F]
  [NormedSpace ℝ F] (f : E → F) (u : E)
  (p : ℝ) : F

Implementation after :=

:=
  ∫ y : ((ℝ ∙ u)ᗮ : Submodule ℝ E), f (p • u + ↑y)

The Radon transform `R[f](u, p) = ∫_{(ℝu)^⊥} f (p u + y) dy`, integrating over the
orthogonal complement of the line `ℝu` with its canonical Lebesgue measure. It is customarily
used for unit vectors `u`.

defdefined in LeanRidgelet/ToMathlib/RadonTransform.lean

complete

def MeasureTheory.dualRadonTransform.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℝ F] (Φ : E → ℝ → F) (x : E) : F

def MeasureTheory.dualRadonTransform.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {F : Type u_2} [NormedAddCommGroup F]
  [NormedSpace ℝ F] (Φ : E → ℝ → F)
  (x : E) : F

Implementation after :=

:=
  ∫ u : Metric.sphere (0 : E) 1,
    Φ u (inner ℝ (u : E) x) ∂(volume : Measure E).toSphere

The dual Radon transform (backprojection) `R†[Φ](x) = ∫_{𝕊} Φ (u, ⟪u, x⟫) du`, with the
surface measure `volume.toSphere` on the unit sphere of `E`.

defdefined in LeanRidgelet/ToMathlib/RadonTransform.lean

complete

def MeasureTheory.lineOrthogonalSplit.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (u : E) (hu : ‖u‖ = 1) :
  ℝ × ↥(ℝ ∙ u)ᗮ ≃ᵐ E

def MeasureTheory.lineOrthogonalSplit.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (u : E) (hu : ‖u‖ = 1) :
  ℝ × ↥(ℝ ∙ u)ᗮ ≃ᵐ E

Implementation after :=

:=
  (MeasurableEquiv.toLp 2 (ℝ × ((ℝ ∙ u)ᗮ : Submodule ℝ E))).trans
    (((LinearIsometryEquiv.withLpProdCongr 2 (LinearIsometryEquiv.toSpanUnitSingleton u hu)
        (LinearIsometryEquiv.refl ℝ ((ℝ ∙ u)ᗮ : Submodule ℝ E))).trans
      (ℝ ∙ u).orthogonalDecomposition.symm).toMeasurableEquiv)

The parametrization `(p, y) ↦ p • u + y` of `E` by the line `ℝ u` and its orthogonal
complement, as a measurable equivalence, for a unit vector `u`. It is assembled from the
`WithLp 2` product coordinates and the orthogonal decomposition `E ≃ₗᵢ ℝu ×₂ (ℝu)^⊥`.

Theorem5.2.2

uses 1

Used by 3

Reverse dependency previews

Preview

Theorem 2.1.10

Loading preview

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

✓L∃∀N

L¹ theory of the Radon transform. The line–hyperplane splitting preserves Lebesgue measure. Consequently, for integrable f and every unit direction u — a fixed-direction strengthening of the almost-every-direction statement quoted in the tomography literature — almost every hyperplane section of f is integrable, the Radon transform \mathscr Rf(u,\cdot) is integrable on \mathbb R, and \int_{\mathbb R}\mathscr Rf(u,p)\,dp=\int_Ef(x)\,dx,\qquad \|\mathscr Rf(u,\cdot)\|_{L^1(\mathbb R)}\le\|f\|_{L^1(E)}.

Lean code for Theorem5.2.2●6 theorems

theoremdefined in LeanRidgelet/ToMathlib/RadonTransform.lean

complete

theorem MeasureTheory.measurePreserving_lineOrthogonalSplit.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (u : E) (hu : ‖u‖ = 1) :
  MeasureTheory.MeasurePreserving
    (⇑(MeasureTheory.lineOrthogonalSplit u hu)) MeasureTheory.volume
    MeasureTheory.volume

theorem MeasureTheory.measurePreserving_lineOrthogonalSplit.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (u : E) (hu : ‖u‖ = 1) :
  MeasureTheory.MeasurePreserving
    (⇑(MeasureTheory.lineOrthogonalSplit u
        hu))
    MeasureTheory.volume
    MeasureTheory.volume

The line–hyperplane parametrization preserves Lebesgue measure.

theoremdefined in LeanRidgelet/ToMathlib/RadonTransform.lean

complete

theorem MeasureTheory.integrable_comp_lineOrthogonalSplit.{u_1, u_2}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  {F : Type u_2} [NormedAddCommGroup F] {f : E → F}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume) (u : E)
  (hu : ‖u‖ = 1) :
  MeasureTheory.Integrable (fun py ↦ f (py.1 • u + ↑py.2))
    MeasureTheory.volume

theorem MeasureTheory.integrable_comp_lineOrthogonalSplit.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {F : Type u_2} [NormedAddCommGroup F]
  {f : E → F}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (u : E) (hu : ‖u‖ = 1) :
  MeasureTheory.Integrable
    (fun py ↦ f (py.1 • u + ↑py.2))
    MeasureTheory.volume

Transport of integrability through the line–hyperplane parametrization.

theoremdefined in LeanRidgelet/ToMathlib/RadonTransform.lean

complete

theorem MeasureTheory.ae_integrable_radonTransform_section.{u_1, u_2}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  {F : Type u_2} [NormedAddCommGroup F] {f : E → F}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume) (u : E)
  (hu : ‖u‖ = 1) :
  ∀ᵐ (p : ℝ),
    MeasureTheory.Integrable (fun y ↦ f (p • u + ↑y))
      MeasureTheory.volume

theorem MeasureTheory.ae_integrable_radonTransform_section.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {F : Type u_2} [NormedAddCommGroup F]
  {f : E → F}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (u : E) (hu : ‖u‖ = 1) :
  ∀ᵐ (p : ℝ),
    MeasureTheory.Integrable
      (fun y ↦ f (p • u + ↑y))
      MeasureTheory.volume

For integrable `f` and a unit direction `u`, almost every hyperplane section of `f` is
integrable, so the Radon transform is an absolutely convergent integral at almost every
offset `p`.

theoremdefined in LeanRidgelet/ToMathlib/RadonTransform.lean

complete

theorem MeasureTheory.integrable_radonTransform.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume) (u : E)
  (hu : ‖u‖ = 1) :
  MeasureTheory.Integrable (MeasureTheory.radonTransform f u)
    MeasureTheory.volume

theorem MeasureTheory.integrable_radonTransform.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {F : Type u_2} [NormedAddCommGroup F]
  [NormedSpace ℝ F] {f : E → F}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (u : E) (hu : ‖u‖ = 1) :
  MeasureTheory.Integrable
    (MeasureTheory.radonTransform f u)
    MeasureTheory.volume

The Radon transform of an integrable function along any unit direction is integrable: the
`L¹` half of the Fubini corollary, `R : L¹(E) → L¹(ℝ)` in the offset variable.

theoremdefined in LeanRidgelet/ToMathlib/RadonTransform.lean

complete

theorem MeasureTheory.integral_radonTransform.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume) (u : E)
  (hu : ‖u‖ = 1) :
  ∫ (p : ℝ), MeasureTheory.radonTransform f u p = ∫ (x : E), f x

theorem MeasureTheory.integral_radonTransform.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {F : Type u_2} [NormedAddCommGroup F]
  [NormedSpace ℝ F] {f : E → F}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (u : E) (hu : ‖u‖ = 1) :
  ∫ (p : ℝ),
      MeasureTheory.radonTransform f u p =
    ∫ (x : E), f x

The Fubini corollary `∫ p, R[f](u, p) dp = ∫ x, f x dx` for every unit direction `u`.

theoremdefined in LeanRidgelet/ToMathlib/RadonTransform.lean

complete

theorem MeasureTheory.integral_norm_radonTransform_le.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume) (u : E)
  (hu : ‖u‖ = 1) :
  ∫ (p : ℝ), ‖MeasureTheory.radonTransform f u p‖ ≤ ∫ (x : E), ‖f x‖

theorem MeasureTheory.integral_norm_radonTransform_le.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {F : Type u_2} [NormedAddCommGroup F]
  [NormedSpace ℝ F] {f : E → F}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (u : E) (hu : ‖u‖ = 1) :
  ∫ (p : ℝ),
      ‖MeasureTheory.radonTransform f u
          p‖ ≤
    ∫ (x : E), ‖f x‖

The Radon transform contracts the `L¹` norm: `∫ p, ‖R[f](u, p)‖ dp ≤ ∫ x, ‖f x‖ dx`.

Theorem5.2.3

Statement uses 2

Statement dependency previews

Preview

Definition 5.2.1

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Theorem 2.2.1

Loading preview

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

✓L∃∀N

Fourier slice theorem. For integrable f on E with values in a complex normed space, a unit vector u, and every frequency \omega, \mathcal F f(\omega u)=\mathcal F(\mathscr Rf(u,\cdot))(\omega), where the left-hand side is the Fourier transform on E and the right-hand side the one-dimensional Fourier transform, both in the Mathlib 2π convention (𝓕). Also known as the projection-slice or central-slice theorem.

Lean code for Theorem5.2.3●1 theorem

theoremdefined in LeanRidgelet/ToMathlib/RadonTransform.lean

complete

theorem MeasureTheory.fourier_slice_radonTransform.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℂ F] {f : E → F}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume) (u : E)
  (hu : ‖u‖ = 1) (ω : ℝ) :
  FourierTransform.fourier f (ω • u) =
    FourierTransform.fourier (MeasureTheory.radonTransform f u) ω

theorem MeasureTheory.fourier_slice_radonTransform.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  {F : Type u_2} [NormedAddCommGroup F]
  [NormedSpace ℂ F] {f : E → F}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (u : E) (hu : ‖u‖ = 1) (ω : ℝ) :
  FourierTransform.fourier f (ω • u) =
    FourierTransform.fourier
      (MeasureTheory.radonTransform f u) ω

**Fourier slice theorem** (projection-slice theorem): the Fourier transform of an
integrable function on `E`, restricted to the ray through a unit vector `u`, is the
one-dimensional Fourier transform of its Radon transform:
`𝓕 f (ω • u) = 𝓕 (R[f](u, ·)) ω`.

Fourier analysis

Theorem5.2.4

uses 0

Used by 5

Reverse dependency previews

Preview

Theorem 2.1.20

Loading preview

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

✓L∃∀N

Plancherel's theorem on L¹ ∩ L². Mathlib's MeasureTheory.Lp.fourierTransformₗᵢ provides the Fourier transform on L² of a finite-dimensional real inner product space as a linear isometry, with Schwartz and tempered-distribution compatibility, but no statement that on L¹ ∩ L² the isometry is computed by the Fourier integral. That bridge is proved here: for integrable, square-integrable f, the Fourier integral 𝓕 f is an almost-everywhere representative of the L² Fourier transform of the class of f; it is square-integrable; and \int\|\mathcal Ff(\xi)\|^2\,d\xi=\int\|f(x)\|^2\,dx in both Bochner and lintegral form. The proof pairs the L² transform against Schwartz functions through the tempered-distribution compatibility, rewrites with the self-adjointness of the Fourier integral, and identifies the representatives with ae_eq_of_integral_contDiff_smul_eq. The polarized companions (last three declarations) provide the integrability of pointwise products of L² functions and Parseval's relation on L¹ ∩ L², \int\langle\mathcal Ff,\mathcal Fg\rangle=\int\langle f,g\rangle (with the scalar mul-conjugate form), by transporting the unitarity of MeasureTheory.Lp.fourierTransformₗᵢ through the L¹ ∩ L² representation.

Lean code for Theorem5.2.4●7 theorems

theoremdefined in LeanRidgelet/ToMathlib/FourierPlancherel.lean

complete

theorem MeasureTheory.Integrable.fourier_toLp_ae_eq.{u_1, u_2} {E : Type u_1}
  {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E]
  [BorelSpace E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
  {f : E → F} (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) :
  ↑↑(FourierTransform.fourier
          (MeasureTheory.MemLp.toLp f h2)) =ᵐ[MeasureTheory.volume]
    FourierTransform.fourier f

theorem MeasureTheory.Integrable.fourier_toLp_ae_eq.{u_1,
    u_2}
  {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E]
  [MeasurableSpace E] [BorelSpace E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [NormedAddCommGroup F]
  [InnerProductSpace ℂ F]
  [CompleteSpace F] {f : E → F}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (h2 :
    MeasureTheory.MemLp f 2
      MeasureTheory.volume) :
  ↑↑(FourierTransform.fourier
          (MeasureTheory.MemLp.toLp f
            h2)) =ᵐ[MeasureTheory.volume]
    FourierTransform.fourier f

On `L¹ ∩ L²`, the `L²` Fourier transform is computed by the Fourier integral: the
Fourier integral `𝓕 f` is an almost-everywhere representative of `𝓕` applied to the `L²`
class of `f`.

theoremdefined in LeanRidgelet/ToMathlib/FourierPlancherel.lean

complete

theorem MeasureTheory.Integrable.memLp_fourier.{u_1, u_2} {E : Type u_1}
  {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E]
  [BorelSpace E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
  {f : E → F} (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) :
  MeasureTheory.MemLp (FourierTransform.fourier f) 2
    MeasureTheory.volume

theorem MeasureTheory.Integrable.memLp_fourier.{u_1,
    u_2}
  {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E]
  [MeasurableSpace E] [BorelSpace E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [NormedAddCommGroup F]
  [InnerProductSpace ℂ F]
  [CompleteSpace F] {f : E → F}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (h2 :
    MeasureTheory.MemLp f 2
      MeasureTheory.volume) :
  MeasureTheory.MemLp
    (FourierTransform.fourier f) 2
    MeasureTheory.volume

On `L¹ ∩ L²`, the Fourier integral is square-integrable.

theoremdefined in LeanRidgelet/ToMathlib/FourierPlancherel.lean

complete

theorem MeasureTheory.Integrable.integral_norm_fourier_sq.{u_1, u_2}
  {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E]
  [MeasurableSpace E] [BorelSpace E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℂ F]
  [CompleteSpace F] {f : E → F}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) :
  ∫ (ξ : E), ‖FourierTransform.fourier f ξ‖ ^ 2 = ∫ (x : E), ‖f x‖ ^ 2

theorem MeasureTheory.Integrable.integral_norm_fourier_sq.{u_1,
    u_2}
  {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E]
  [MeasurableSpace E] [BorelSpace E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [NormedAddCommGroup F]
  [InnerProductSpace ℂ F]
  [CompleteSpace F] {f : E → F}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (h2 :
    MeasureTheory.MemLp f 2
      MeasureTheory.volume) :
  ∫ (ξ : E),
      ‖FourierTransform.fourier f ξ‖ ^ 2 =
    ∫ (x : E), ‖f x‖ ^ 2

**Plancherel's theorem on `L¹ ∩ L²`**: `∫ ‖𝓕 f ξ‖² dξ = ∫ ‖f x‖² dx`.

theoremdefined in LeanRidgelet/ToMathlib/FourierPlancherel.lean

complete

theorem MeasureTheory.Integrable.lintegral_enorm_fourier_sq.{u_1, u_2}
  {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E]
  [MeasurableSpace E] [BorelSpace E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℂ F]
  [CompleteSpace F] {f : E → F}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) :
  ∫⁻ (ξ : E), ‖FourierTransform.fourier f ξ‖ₑ ^ 2 =
    ∫⁻ (x : E), ‖f x‖ₑ ^ 2

theorem MeasureTheory.Integrable.lintegral_enorm_fourier_sq.{u_1,
    u_2}
  {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E]
  [MeasurableSpace E] [BorelSpace E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [NormedAddCommGroup F]
  [InnerProductSpace ℂ F]
  [CompleteSpace F] {f : E → F}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (h2 :
    MeasureTheory.MemLp f 2
      MeasureTheory.volume) :
  ∫⁻ (ξ : E),
      ‖FourierTransform.fourier f ξ‖ₑ ^
        2 =
    ∫⁻ (x : E), ‖f x‖ₑ ^ 2

**Plancherel's theorem on `L¹ ∩ L²`**, `lintegral` form:
`∫⁻ ‖𝓕 f ξ‖ₑ² dξ = ∫⁻ ‖f x‖ₑ² dx`.

theoremdefined in LeanRidgelet/ToMathlib/FourierPlancherel.lean

complete

theorem MeasureTheory.MemLp.integrable_mul_conj.{u_3} {α : Type u_3}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {u v : α → ℂ}
  (hu : MeasureTheory.MemLp u 2 μ) (hv : MeasureTheory.MemLp v 2 μ) :
  MeasureTheory.Integrable (fun x ↦ u x * (starRingEnd ℂ) (v x)) μ

theorem MeasureTheory.MemLp.integrable_mul_conj.{u_3}
  {α : Type u_3} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {u v : α → ℂ}
  (hu : MeasureTheory.MemLp u 2 μ)
  (hv : MeasureTheory.MemLp v 2 μ) :
  MeasureTheory.Integrable
    (fun x ↦ u x * (starRingEnd ℂ) (v x))
    μ

The pointwise product `u ⋅ conj v` of two square-integrable functions is integrable —
the scalar mul-conjugate form of `MeasureTheory.L2.integrable_inner`.

theoremdefined in LeanRidgelet/ToMathlib/FourierPlancherel.lean

complete

theorem MeasureTheory.Integrable.integral_inner_fourier.{u_1, u_2}
  {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E]
  [MeasurableSpace E] [BorelSpace E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℂ F]
  [CompleteSpace F] {f g : E → F}
  (hf1 : MeasureTheory.Integrable f MeasureTheory.volume)
  (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume)
  (hg1 : MeasureTheory.Integrable g MeasureTheory.volume)
  (hg2 : MeasureTheory.MemLp g 2 MeasureTheory.volume) :
  ∫ (ξ : E),
      inner ℂ (FourierTransform.fourier f ξ)
        (FourierTransform.fourier g ξ) =
    ∫ (x : E), inner ℂ (f x) (g x)

theorem MeasureTheory.Integrable.integral_inner_fourier.{u_1,
    u_2}
  {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E]
  [MeasurableSpace E] [BorelSpace E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [NormedAddCommGroup F]
  [InnerProductSpace ℂ F]
  [CompleteSpace F] {f g : E → F}
  (hf1 :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hf2 :
    MeasureTheory.MemLp f 2
      MeasureTheory.volume)
  (hg1 :
    MeasureTheory.Integrable g
      MeasureTheory.volume)
  (hg2 :
    MeasureTheory.MemLp g 2
      MeasureTheory.volume) :
  ∫ (ξ : E),
      inner ℂ
        (FourierTransform.fourier f ξ)
        (FourierTransform.fourier g ξ) =
    ∫ (x : E), inner ℂ (f x) (g x)

**Parseval's relation on `L¹ ∩ L²`**: the Fourier integral preserves pointwise inner
products of integrable square-integrable functions,
`∫ ⟪𝓕 f ξ, 𝓕 g ξ⟫ dξ = ∫ ⟪f x, g x⟫ dx`. Bridges the unitarity of the `L²` Fourier
transform (`MeasureTheory.Lp.fourierTransformₗᵢ`) to the Fourier integral through the
`L¹ ∩ L²` representation.

theoremdefined in LeanRidgelet/ToMathlib/FourierPlancherel.lean

complete

theorem MeasureTheory.Integrable.integral_fourier_mul_conj_fourier.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E]
  [BorelSpace E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  {u v : E → ℂ} (hu1 : MeasureTheory.Integrable u MeasureTheory.volume)
  (hu2 : MeasureTheory.MemLp u 2 MeasureTheory.volume)
  (hv1 : MeasureTheory.Integrable v MeasureTheory.volume)
  (hv2 : MeasureTheory.MemLp v 2 MeasureTheory.volume) :
  ∫ (ξ : E),
      FourierTransform.fourier u ξ *
        (starRingEnd ℂ) (FourierTransform.fourier v ξ) =
    ∫ (x : E), u x * (starRingEnd ℂ) (v x)

theorem MeasureTheory.Integrable.integral_fourier_mul_conj_fourier.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [MeasurableSpace E] [BorelSpace E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] {u v : E → ℂ}
  (hu1 :
    MeasureTheory.Integrable u
      MeasureTheory.volume)
  (hu2 :
    MeasureTheory.MemLp u 2
      MeasureTheory.volume)
  (hv1 :
    MeasureTheory.Integrable v
      MeasureTheory.volume)
  (hv2 :
    MeasureTheory.MemLp v 2
      MeasureTheory.volume) :
  ∫ (ξ : E),
      FourierTransform.fourier u ξ *
        (starRingEnd ℂ)
          (FourierTransform.fourier v ξ) =
    ∫ (x : E), u x * (starRingEnd ℂ) (v x)

**Parseval's relation on `L¹ ∩ L²`**, scalar mul-conjugate form:
`∫ 𝓕 u ⋅ conj (𝓕 v) = ∫ u ⋅ conj v`.

Theorem5.2.5

Statement uses 2

Statement dependency previews

Preview

Theorem 5.1.5

Loading preview

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

used by 1✓L∃∀N

Convolution with a quadratic chirp is unitary up to a constant. For a self-adjoint invertible A on a space of dimension m and a real \alpha\ne0, convolution with y\mapsto e^{i\alpha\langle y,Ay\rangle} multiplies the squared L^2 norm of every f\in L^1\cap L^2 by exactly \pi^m/(|\alpha|^m|\det A|). No Fresnel integral is evaluated: expanding the square shows the convolution at x is a unit phase times the Fourier transform of the chirped function f(y)e^{i\alpha\langle y,Ay\rangle} at the frequency (\alpha/\pi)Ax, and Plancherel with the linear change of variables x\mapsto(\alpha/\pi)Ax finishes. The polarized form, the L^2 inner product of the chirp convolutions of two functions in L^1\cap L^2, is \pi^m/(|\alpha|^m|\det A|) times their inner product, by the same two steps.

Lean code for Theorem5.2.5●4 theorems

theoremdefined in LeanRidgelet/ToMathlib/QuadraticChirp.lean

complete

theorem MeasureTheory.inner_sub_selfAdjoint_sub.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (A : E →L[ℝ] E) (hA : IsSelfAdjoint A) (x y : E) :
  inner ℝ (x - y) (A (x - y)) =
    inner ℝ x (A x) - 2 * inner ℝ y (A x) + inner ℝ y (A y)

theorem MeasureTheory.inner_sub_selfAdjoint_sub.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] (A : E →L[ℝ] E)
  (hA : IsSelfAdjoint A) (x y : E) :
  inner ℝ (x - y) (A (x - y)) =
    inner ℝ x (A x) -
        2 * inner ℝ y (A x) +
      inner ℝ y (A y)

Expansion of the quadratic form of a self-adjoint operator at a difference.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticChirp.lean

complete

theorem MeasureTheory.integral_mul_cexp_quadratic_eq.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (A : E →L[ℝ] E)
  (hA : IsSelfAdjoint A) (α : ℝ) (f : E → ℂ) (x : E) :
  ∫ (y : E),
      f y *
        Complex.exp (↑(α * inner ℝ (x - y) (A (x - y))) * Complex.I) =
    Complex.exp (↑(α * inner ℝ x (A x)) * Complex.I) *
      FourierTransform.fourier
        (fun y ↦ f y * Complex.exp (↑(α * inner ℝ y (A y)) * Complex.I))
        ((α / Real.pi) • A x)

theorem MeasureTheory.integral_mul_cexp_quadratic_eq.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (A : E →L[ℝ] E) (hA : IsSelfAdjoint A)
  (α : ℝ) (f : E → ℂ) (x : E) :
  ∫ (y : E),
      f y *
        Complex.exp
          (↑(α *
                inner ℝ (x - y)
                  (A (x - y))) *
            Complex.I) =
    Complex.exp
        (↑(α * inner ℝ x (A x)) *
          Complex.I) *
      FourierTransform.fourier
        (fun y ↦
          f y *
            Complex.exp
              (↑(α * inner ℝ y (A y)) *
                Complex.I))
        ((α / Real.pi) • A x)

**The chirp convolution is a phase times a Fourier transform.**  At `x`, the convolution of
`f` with the quadratic chirp `y ↦ exp(i α ⟪y, A y⟫)` is `exp(i α ⟪x, A x⟫)` times the Fourier
transform of the chirped function `y ↦ f(y) exp(i α ⟪y, A y⟫)` at the frequency `(α / π) A x`.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticChirp.lean

complete

theorem MeasureTheory.lintegral_enorm_integral_mul_cexp_quadratic_sq.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  (A : E →L[ℝ] E) (hA : IsSelfAdjoint A) (hdet : A.det ≠ 0) {α : ℝ}
  (hα : α ≠ 0) {f : E → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) :
  ∫⁻ (x : E),
      ‖∫ (y : E),
            f y *
              Complex.exp
                (↑(α * inner ℝ (x - y) (A (x - y))) * Complex.I)‖ₑ ^
        2 =
    ENNReal.ofReal
        (Real.pi ^ Module.finrank ℝ E /
          (|α| ^ Module.finrank ℝ E * |A.det|)) *
      ∫⁻ (y : E), ‖f y‖ₑ ^ 2

theorem MeasureTheory.lintegral_enorm_integral_mul_cexp_quadratic_sq.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (A : E →L[ℝ] E) (hA : IsSelfAdjoint A)
  (hdet : A.det ≠ 0) {α : ℝ} (hα : α ≠ 0)
  {f : E → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (h2 :
    MeasureTheory.MemLp f 2
      MeasureTheory.volume) :
  ∫⁻ (x : E),
      ‖∫ (y : E),
            f y *
              Complex.exp
                (↑(α *
                      inner ℝ (x - y)
                        (A (x - y))) *
                  Complex.I)‖ₑ ^
        2 =
    ENNReal.ofReal
        (Real.pi ^ Module.finrank ℝ E /
          (|α| ^ Module.finrank ℝ E *
            |A.det|)) *
      ∫⁻ (y : E), ‖f y‖ₑ ^ 2

**Convolution with a quadratic chirp is unitary up to a constant.**  For `f ∈ L¹ ∩ L²`,
`∫ ‖∫ f(y) exp(i α ⟪x - y, A (x - y)⟫) dy‖² dx = π^m / (|α|^m |det A|) · ∫ ‖f‖²`, where `m` is the
dimension.  In particular the left side does not depend on anything but the `L²` norm of `f`.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticChirp.lean

complete

theorem MeasureTheory.integral_integral_mul_cexp_quadratic_mul_conj.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  (A : E →L[ℝ] E) (hA : IsSelfAdjoint A) (hdet : A.det ≠ 0) {α : ℝ}
  (hα : α ≠ 0) {f h : E → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume)
  (hh : MeasureTheory.Integrable h MeasureTheory.volume)
  (hh2 : MeasureTheory.MemLp h 2 MeasureTheory.volume) :
  ∫ (x : E),
      (∫ (y : E),
          f y *
            Complex.exp
              (↑(α * inner ℝ (x - y) (A (x - y))) * Complex.I)) *
        (starRingEnd ℂ)
          (∫ (y : E),
            h y *
              Complex.exp
                (↑(α * inner ℝ (x - y) (A (x - y))) * Complex.I)) =
    ↑(Real.pi ^ Module.finrank ℝ E /
          (|α| ^ Module.finrank ℝ E * |A.det|)) *
      ∫ (y : E), f y * (starRingEnd ℂ) (h y)

theorem MeasureTheory.integral_integral_mul_cexp_quadratic_mul_conj.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (A : E →L[ℝ] E) (hA : IsSelfAdjoint A)
  (hdet : A.det ≠ 0) {α : ℝ} (hα : α ≠ 0)
  {f h : E → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hf2 :
    MeasureTheory.MemLp f 2
      MeasureTheory.volume)
  (hh :
    MeasureTheory.Integrable h
      MeasureTheory.volume)
  (hh2 :
    MeasureTheory.MemLp h 2
      MeasureTheory.volume) :
  ∫ (x : E),
      (∫ (y : E),
          f y *
            Complex.exp
              (↑(α *
                    inner ℝ (x - y)
                      (A (x - y))) *
                Complex.I)) *
        (starRingEnd ℂ)
          (∫ (y : E),
            h y *
              Complex.exp
                (↑(α *
                      inner ℝ (x - y)
                        (A (x - y))) *
                  Complex.I)) =
    ↑(Real.pi ^ Module.finrank ℝ E /
          (|α| ^ Module.finrank ℝ E *
            |A.det|)) *
      ∫ (y : E),
        f y * (starRingEnd ℂ) (h y)

**The polarized chirp identity.**  For `f, h ∈ L¹ ∩ L²` and `α ≠ 0`,
`∫ (∫ f(y) e^{iα⟪x-y,A(x-y)⟫} dy) conj(∫ h(y) e^{iα⟪x-y,A(x-y)⟫} dy) dx
  = π^m / (|α|^m |det A|) · ∫ f conj h`.
The two unit phases cancel, and Parseval with the same linear change of variables as in
`MeasureTheory.lintegral_enorm_integral_mul_cexp_quadratic_sq` finishes; no polarization identity
is invoked.

This is the unitarity of the Fresnel transform, and the reason it matters for a reconstruction constant is the word exactly: the modulus of the Fourier transform of a chirp does not depend on the frequency, so a multiplier built by pairing against all level shifts of a quadratic profile comes out constant in the frequency.

Theorem5.2.6

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 1✓L∃∀N

The energy identity of the level-shifted radial family. Pairing a datum f against all level shifts of a composite g\circ q gives a function of the level whose Fourier transform is \mathcal Fg times the frequency profile \int f(y)e^{2\pi i\zeta q(y)}dy of f along q, so by Plancherel its energy is \int|\mathcal Fg(\zeta)|^2\,|\int f(y)e^{2\pi i\zeta q(y)}dy|^2\,d\zeta. When q is the quadratic form of a self-adjoint invertible A centered at x_0 and the center is integrated out too, the chirp identity evaluates the inner weight, and \int\!\!\int\Big\|\int g(\langle y-x_0,A(y-x_0)\rangle+s)f(y)\,dy\Big\|^2ds\,dx_0=\Big(\int|\mathcal Fg(\zeta)|^2\frac{\pi^m}{|2\pi\zeta|^m|\det A|}\,d\zeta\Big)\|f\|_2^2 for bounded integrable g and f\in L^1\cap L^2; the constant is positive for every nonzero g. Polarized: for two profiles g_1,g_2 and two data f,h, \int\!\!\int F_1(x_0,s)\overline{F_2(x_0,s)}\,ds\,dx_0=\Big(\int\mathcal Fg_1(\zeta)\overline{\mathcal Fg_2(\zeta)}\frac{\pi^m}{|2\pi\zeta|^m|\det A|}\,d\zeta\Big)\int f\bar h, in iterated form under a finite weighted cross energy \int|\mathcal Fg_1||\mathcal Fg_2|\,\pi^m/(|2\pi\zeta|^m|\det A|)<\infty and in the L^2(E\times\mathbb R) inner-product form when both profiles have finite constants, in which case each pairing is square-integrable in the center and the level jointly.

Lean code for Theorem5.2.6●18 declarations

defdefined in LeanRidgelet/ToMathlib/QuadraticLevelShift.lean

complete

def MeasureTheory.levelShiftPairing.{u_1} {X : Type u_1} [MeasurableSpace X]
  (g : ℝ → ℂ) (q : X → ℝ) (f : X → ℂ) (μ : MeasureTheory.Measure X)
  (s : ℝ) : ℂ

def MeasureTheory.levelShiftPairing.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  (g : ℝ → ℂ) (q : X → ℝ) (f : X → ℂ)
  (μ : MeasureTheory.Measure X) (s : ℝ) :
  ℂ

Implementation after :=

:=
  ∫ y, g (q y + s) * f y ∂μ

The pairing of a datum `f` against all level shifts of the composite `g ∘ q`.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticLevelShift.lean

complete

theorem MeasureTheory.integrable_levelShift_prod.{u_1} {X : Type u_1}
  [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [MeasureTheory.SFinite μ] {g : ℝ → ℂ} (hgm : Measurable g)
  (hg1 : MeasureTheory.Integrable g MeasureTheory.volume) {q : X → ℝ}
  (hq : Measurable q) {f : X → ℂ} (hf : MeasureTheory.Integrable f μ) :
  MeasureTheory.Integrable (fun p ↦ g (q p.2 + p.1) * f p.2)
    (MeasureTheory.volume.prod μ)

theorem MeasureTheory.integrable_levelShift_prod.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  [MeasureTheory.SFinite μ] {g : ℝ → ℂ}
  (hgm : Measurable g)
  (hg1 :
    MeasureTheory.Integrable g
      MeasureTheory.volume)
  {q : X → ℝ} (hq : Measurable q)
  {f : X → ℂ}
  (hf : MeasureTheory.Integrable f μ) :
  MeasureTheory.Integrable
    (fun p ↦ g (q p.2 + p.1) * f p.2)
    (MeasureTheory.volume.prod μ)

The integrand of the level-shift pairing is integrable on the product of the level line with
the base.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticLevelShift.lean

complete

theorem MeasureTheory.integrable_levelShiftPairing.{u_1} {X : Type u_1}
  [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [MeasureTheory.SFinite μ] {g : ℝ → ℂ} (hgm : Measurable g)
  (hg1 : MeasureTheory.Integrable g MeasureTheory.volume) {q : X → ℝ}
  (hq : Measurable q) {f : X → ℂ} (hf : MeasureTheory.Integrable f μ) :
  MeasureTheory.Integrable (MeasureTheory.levelShiftPairing g q f μ)
    MeasureTheory.volume

theorem MeasureTheory.integrable_levelShiftPairing.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  [MeasureTheory.SFinite μ] {g : ℝ → ℂ}
  (hgm : Measurable g)
  (hg1 :
    MeasureTheory.Integrable g
      MeasureTheory.volume)
  {q : X → ℝ} (hq : Measurable q)
  {f : X → ℂ}
  (hf : MeasureTheory.Integrable f μ) :
  MeasureTheory.Integrable
    (MeasureTheory.levelShiftPairing g q f
      μ)
    MeasureTheory.volume

The level-shift pairing is integrable.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticLevelShift.lean

complete

theorem MeasureTheory.norm_levelShiftPairing_le.{u_1} {X : Type u_1}
  [MeasurableSpace X] {μ : MeasureTheory.Measure X} {g : ℝ → ℂ} {M : ℝ}
  (hgM : ∀ (u : ℝ), ‖g u‖ ≤ M) {q : X → ℝ} {f : X → ℂ}
  (hf : MeasureTheory.Integrable f μ) (s : ℝ) :
  ‖MeasureTheory.levelShiftPairing g q f μ s‖ ≤ M * ∫ (y : X), ‖f y‖ ∂μ

theorem MeasureTheory.norm_levelShiftPairing_le.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  {g : ℝ → ℂ} {M : ℝ}
  (hgM : ∀ (u : ℝ), ‖g u‖ ≤ M) {q : X → ℝ}
  {f : X → ℂ}
  (hf : MeasureTheory.Integrable f μ)
  (s : ℝ) :
  ‖MeasureTheory.levelShiftPairing g q f μ
        s‖ ≤
    M * ∫ (y : X), ‖f y‖ ∂μ

The level-shift pairing is bounded by `M ‖f‖₁` when `‖g‖ ≤ M`.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticLevelShift.lean

complete

theorem MeasureTheory.memLp_two_levelShiftPairing.{u_1} {X : Type u_1}
  [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [MeasureTheory.SFinite μ] {g : ℝ → ℂ} (hgm : Measurable g)
  (hg1 : MeasureTheory.Integrable g MeasureTheory.volume) {M : ℝ}
  (hgM : ∀ (u : ℝ), ‖g u‖ ≤ M) {q : X → ℝ} (hq : Measurable q)
  {f : X → ℂ} (hf : MeasureTheory.Integrable f μ) :
  MeasureTheory.MemLp (MeasureTheory.levelShiftPairing g q f μ) 2
    MeasureTheory.volume

theorem MeasureTheory.memLp_two_levelShiftPairing.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  [MeasureTheory.SFinite μ] {g : ℝ → ℂ}
  (hgm : Measurable g)
  (hg1 :
    MeasureTheory.Integrable g
      MeasureTheory.volume)
  {M : ℝ} (hgM : ∀ (u : ℝ), ‖g u‖ ≤ M)
  {q : X → ℝ} (hq : Measurable q)
  {f : X → ℂ}
  (hf : MeasureTheory.Integrable f μ) :
  MeasureTheory.MemLp
    (MeasureTheory.levelShiftPairing g q f
      μ)
    2 MeasureTheory.volume

The level-shift pairing is square-integrable, being bounded and integrable.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticLevelShift.lean

complete

theorem MeasureTheory.fourier_levelShiftPairing.{u_1} {X : Type u_1}
  [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [MeasureTheory.SFinite μ] {g : ℝ → ℂ} (hgm : Measurable g)
  (hg1 : MeasureTheory.Integrable g MeasureTheory.volume) {q : X → ℝ}
  (hq : Measurable q) {f : X → ℂ} (hf : MeasureTheory.Integrable f μ)
  (ζ : ℝ) :
  FourierTransform.fourier (MeasureTheory.levelShiftPairing g q f μ) ζ =
    FourierTransform.fourier g ζ *
      ∫ (y : X),
        f y * Complex.exp (↑(2 * Real.pi * ζ * q y) * Complex.I) ∂μ

theorem MeasureTheory.fourier_levelShiftPairing.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  [MeasureTheory.SFinite μ] {g : ℝ → ℂ}
  (hgm : Measurable g)
  (hg1 :
    MeasureTheory.Integrable g
      MeasureTheory.volume)
  {q : X → ℝ} (hq : Measurable q)
  {f : X → ℂ}
  (hf : MeasureTheory.Integrable f μ)
  (ζ : ℝ) :
  FourierTransform.fourier
      (MeasureTheory.levelShiftPairing g q
        f μ)
      ζ =
    FourierTransform.fourier g ζ *
      ∫ (y : X),
        f y *
          Complex.exp
            (↑(2 * Real.pi * ζ * q y) *
              Complex.I) ∂μ

**The Fourier transform of the level-shift pairing** is `𝓕 g` times the frequency profile of
`f` along `q`: `𝓕 F(ζ) = 𝓕 g(ζ) ∫ f(y) exp(2πi ζ q(y)) dy`.  A translation of the level is a
phase on the frequency side, and the phase is the profile.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticLevelShift.lean

complete

theorem MeasureTheory.lintegral_enorm_levelShiftPairing_sq.{u_1} {X : Type u_1}
  [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [MeasureTheory.SFinite μ] {g : ℝ → ℂ} (hgm : Measurable g)
  (hg1 : MeasureTheory.Integrable g MeasureTheory.volume) {M : ℝ}
  (hgM : ∀ (u : ℝ), ‖g u‖ ≤ M) {q : X → ℝ} (hq : Measurable q)
  {f : X → ℂ} (hf : MeasureTheory.Integrable f μ) :
  ∫⁻ (s : ℝ), ‖MeasureTheory.levelShiftPairing g q f μ s‖ₑ ^ 2 =
    ∫⁻ (ζ : ℝ),
      ‖FourierTransform.fourier g ζ‖ₑ ^ 2 *
        ‖∫ (y : X),
              f y *
                Complex.exp
                  (↑(2 * Real.pi * ζ * q y) * Complex.I) ∂μ‖ₑ ^
          2

theorem MeasureTheory.lintegral_enorm_levelShiftPairing_sq.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  [MeasureTheory.SFinite μ] {g : ℝ → ℂ}
  (hgm : Measurable g)
  (hg1 :
    MeasureTheory.Integrable g
      MeasureTheory.volume)
  {M : ℝ} (hgM : ∀ (u : ℝ), ‖g u‖ ≤ M)
  {q : X → ℝ} (hq : Measurable q)
  {f : X → ℂ}
  (hf : MeasureTheory.Integrable f μ) :
  ∫⁻ (s : ℝ),
      ‖MeasureTheory.levelShiftPairing g q
            f μ s‖ₑ ^
        2 =
    ∫⁻ (ζ : ℝ),
      ‖FourierTransform.fourier g ζ‖ₑ ^
          2 *
        ‖∫ (y : X),
              f y *
                Complex.exp
                  (↑(2 * Real.pi * ζ *
                        q y) *
                    Complex.I) ∂μ‖ₑ ^
          2

**Plancherel for the level-shift pairing**:
`∫ ‖F(s)‖² ds = ∫ ‖𝓕 g(ζ)‖² ‖∫ f(y) exp(2πi ζ q(y)) dy‖² dζ`.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticLevelShift.lean

complete

theorem MeasureTheory.lintegral_lintegral_enorm_quadraticLevelShift_sq.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  (A : E →L[ℝ] E) (hA : IsSelfAdjoint A) (hdet : A.det ≠ 0) {g : ℝ → ℂ}
  (hgm : Measurable g)
  (hg1 : MeasureTheory.Integrable g MeasureTheory.volume) {M : ℝ}
  (hgM : ∀ (u : ℝ), ‖g u‖ ≤ M) {f : E → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) :
  ∫⁻ (x₀ : E) (s : ℝ),
      ‖∫ (y : E), g (inner ℝ (y - x₀) (A (y - x₀)) + s) * f y‖ₑ ^ 2 =
    (∫⁻ (ζ : ℝ),
        ‖FourierTransform.fourier g ζ‖ₑ ^ 2 *
          ENNReal.ofReal
            (Real.pi ^ Module.finrank ℝ E /
              (|2 * Real.pi * ζ| ^ Module.finrank ℝ E * |A.det|))) *
      ∫⁻ (y : E), ‖f y‖ₑ ^ 2

theorem MeasureTheory.lintegral_lintegral_enorm_quadraticLevelShift_sq.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (A : E →L[ℝ] E) (hA : IsSelfAdjoint A)
  (hdet : A.det ≠ 0) {g : ℝ → ℂ}
  (hgm : Measurable g)
  (hg1 :
    MeasureTheory.Integrable g
      MeasureTheory.volume)
  {M : ℝ} (hgM : ∀ (u : ℝ), ‖g u‖ ≤ M)
  {f : E → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (h2 :
    MeasureTheory.MemLp f 2
      MeasureTheory.volume) :
  ∫⁻ (x₀ : E) (s : ℝ),
      ‖∫ (y : E),
            g
                (inner ℝ (y - x₀)
                    (A (y - x₀)) +
                  s) *
              f y‖ₑ ^
        2 =
    (∫⁻ (ζ : ℝ),
        ‖FourierTransform.fourier g ζ‖ₑ ^
            2 *
          ENNReal.ofReal
            (Real.pi ^
                Module.finrank ℝ E /
              (|2 * Real.pi * ζ| ^
                  Module.finrank ℝ E *
                |A.det|))) *
      ∫⁻ (y : E), ‖f y‖ₑ ^ 2

**The energy identity of the level-shifted radial family.**  For a self-adjoint invertible `A`
on a space of dimension `m`, a bounded integrable profile `g`, and `f ∈ L¹ ∩ L²`,

`∫∫ ‖∫ g(⟪y - x₀, A (y - x₀)⟫ + s) f(y) dy‖² ds dx₀
  = (∫ ‖𝓕 g(ζ)‖² π^m / (|2πζ|^m |det A|) dζ) · ∫ ‖f‖²`.

The weight `|ζ|^{-m}` is the one of the hyperplane case, and the constant scales like
`|det A|⁻¹`.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticLevelShift.lean

complete

theorem MeasureTheory.lintegral_enorm_fourier_sq_mul_quadraticWeight_pos (m : ℕ)
  {c : ℝ} (hc : 0 < c) {g : ℝ → ℂ}
  (hg1 : MeasureTheory.Integrable g MeasureTheory.volume)
  (hg2 : MeasureTheory.MemLp g 2 MeasureTheory.volume)
  (hg0 : ¬g =ᵐ[MeasureTheory.volume] 0) :
  0 <
    ∫⁻ (ζ : ℝ),
      ‖FourierTransform.fourier g ζ‖ₑ ^ 2 *
        ENNReal.ofReal (Real.pi ^ m / (|2 * Real.pi * ζ| ^ m * c))

theorem MeasureTheory.lintegral_enorm_fourier_sq_mul_quadraticWeight_pos
  (m : ℕ) {c : ℝ} (hc : 0 < c) {g : ℝ → ℂ}
  (hg1 :
    MeasureTheory.Integrable g
      MeasureTheory.volume)
  (hg2 :
    MeasureTheory.MemLp g 2
      MeasureTheory.volume)
  (hg0 : ¬g =ᵐ[MeasureTheory.volume] 0) :
  0 <
    ∫⁻ (ζ : ℝ),
      ‖FourierTransform.fourier g ζ‖ₑ ^
          2 *
        ENNReal.ofReal
          (Real.pi ^ m /
            (|2 * Real.pi * ζ| ^ m * c))

**The constant of the energy identity is positive** for a nonzero profile: if
`∫ ‖𝓕 g(ζ)‖² π^m / (|2πζ|^m c) dζ = 0` then `𝓕 g` vanishes almost everywhere, hence so does `g`
by Plancherel.  No inversion theorem is needed.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticLevelShift.lean

complete

theorem ENNReal.mul_le_sq_add_sq (a b : ENNReal) : a * b ≤ a ^ 2 + b ^ 2

theorem ENNReal.mul_le_sq_add_sq (a b : ENNReal) :
  a * b ≤ a ^ 2 + b ^ 2

`a * b ≤ a ^ 2 + b ^ 2` in `ℝ≥0∞`.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticLevelShift.lean

complete

theorem MeasureTheory.lintegral_comp_neg_eq_self {F : ℝ → ENNReal}
  (hF : Measurable F) : ∫⁻ (ζ : ℝ), F (-ζ) = ∫⁻ (ζ : ℝ), F ζ

theorem MeasureTheory.lintegral_comp_neg_eq_self
  {F : ℝ → ENNReal} (hF : Measurable F) :
  ∫⁻ (ζ : ℝ), F (-ζ) = ∫⁻ (ζ : ℝ), F ζ

A Lebesgue integral over the line is invariant under reflection.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticLevelShift.lean

complete

theorem Real.fourierIntegral_conj (g : ℝ → ℂ) (ζ : ℝ) :
  FourierTransform.fourier (fun t ↦ (starRingEnd ℂ) (g t)) ζ =
    (starRingEnd ℂ) (FourierTransform.fourier g (-ζ))

theorem Real.fourierIntegral_conj (g : ℝ → ℂ)
  (ζ : ℝ) :
  FourierTransform.fourier
      (fun t ↦ (starRingEnd ℂ) (g t)) ζ =
    (starRingEnd ℂ)
      (FourierTransform.fourier g (-ζ))

**The Fourier transform of a conjugate** is the reflected conjugate of the Fourier transform:
`𝓕 (conj g) ζ = conj (𝓕 g (-ζ))`.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticLevelShift.lean

complete

theorem MeasureTheory.integral_integral_quadraticLevelShift_mul_conj.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  (A : E →L[ℝ] E) (hA : IsSelfAdjoint A) (hdet : A.det ≠ 0)
  {g₁ g₂ : ℝ → ℂ} (hg₁m : Measurable g₁)
  (hg₁1 : MeasureTheory.Integrable g₁ MeasureTheory.volume) {M₁ : ℝ}
  (hg₁M : ∀ (u : ℝ), ‖g₁ u‖ ≤ M₁) (hg₂m : Measurable g₂)
  (hg₂1 : MeasureTheory.Integrable g₂ MeasureTheory.volume) {M₂ : ℝ}
  (hg₂M : ∀ (u : ℝ), ‖g₂ u‖ ≤ M₂)
  (hadm :
    ∫⁻ (ζ : ℝ),
        ‖FourierTransform.fourier g₁ ζ‖ₑ *
            ‖FourierTransform.fourier g₂ ζ‖ₑ *
          ENNReal.ofReal
            (Real.pi ^ Module.finrank ℝ E /
              (|2 * Real.pi * ζ| ^ Module.finrank ℝ E * |A.det|)) ≠
      ⊤)
  {f h : E → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume)
  (hh : MeasureTheory.Integrable h MeasureTheory.volume)
  (hh2 : MeasureTheory.MemLp h 2 MeasureTheory.volume) :
  ∫ (x₀ : E) (s : ℝ),
      (∫ (y : E), g₁ (inner ℝ (y - x₀) (A (y - x₀)) + s) * f y) *
        (starRingEnd ℂ)
          (∫ (y : E), g₂ (inner ℝ (y - x₀) (A (y - x₀)) + s) * h y) =
    (∫ (ζ : ℝ),
        FourierTransform.fourier g₁ ζ *
            (starRingEnd ℂ) (FourierTransform.fourier g₂ ζ) *
          ↑(Real.pi ^ Module.finrank ℝ E /
              (|2 * Real.pi * ζ| ^ Module.finrank ℝ E * |A.det|))) *
      ∫ (y : E), f y * (starRingEnd ℂ) (h y)

theorem MeasureTheory.integral_integral_quadraticLevelShift_mul_conj.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (A : E →L[ℝ] E) (hA : IsSelfAdjoint A)
  (hdet : A.det ≠ 0) {g₁ g₂ : ℝ → ℂ}
  (hg₁m : Measurable g₁)
  (hg₁1 :
    MeasureTheory.Integrable g₁
      MeasureTheory.volume)
  {M₁ : ℝ} (hg₁M : ∀ (u : ℝ), ‖g₁ u‖ ≤ M₁)
  (hg₂m : Measurable g₂)
  (hg₂1 :
    MeasureTheory.Integrable g₂
      MeasureTheory.volume)
  {M₂ : ℝ} (hg₂M : ∀ (u : ℝ), ‖g₂ u‖ ≤ M₂)
  (hadm :
    ∫⁻ (ζ : ℝ),
        ‖FourierTransform.fourier g₁ ζ‖ₑ *
            ‖FourierTransform.fourier g₂
                ζ‖ₑ *
          ENNReal.ofReal
            (Real.pi ^
                Module.finrank ℝ E /
              (|2 * Real.pi * ζ| ^
                  Module.finrank ℝ E *
                |A.det|)) ≠
      ⊤)
  {f h : E → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hf2 :
    MeasureTheory.MemLp f 2
      MeasureTheory.volume)
  (hh :
    MeasureTheory.Integrable h
      MeasureTheory.volume)
  (hh2 :
    MeasureTheory.MemLp h 2
      MeasureTheory.volume) :
  ∫ (x₀ : E) (s : ℝ),
      (∫ (y : E),
          g₁
              (inner ℝ (y - x₀)
                  (A (y - x₀)) +
                s) *
            f y) *
        (starRingEnd ℂ)
          (∫ (y : E),
            g₂
                (inner ℝ (y - x₀)
                    (A (y - x₀)) +
                  s) *
              h y) =
    (∫ (ζ : ℝ),
        FourierTransform.fourier g₁ ζ *
            (starRingEnd ℂ)
              (FourierTransform.fourier g₂
                ζ) *
          ↑(Real.pi ^ Module.finrank ℝ E /
              (|2 * Real.pi * ζ| ^
                  Module.finrank ℝ E *
                |A.det|))) *
      ∫ (y : E),
        f y * (starRingEnd ℂ) (h y)

**The polarized energy identity of the level-shifted radial family.**  For a self-adjoint
invertible `A` on a space of dimension `m`, bounded integrable profiles `g₁`, `g₂` whose weighted
cross energy `∫ ‖𝓕 g₁‖ ‖𝓕 g₂‖ π^m / (|2πζ|^m |det A|) dζ` is finite, and `f, h ∈ L¹ ∩ L²`,

`∫ (∫ F₁(x₀, s) conj(F₂(x₀, s)) ds) dx₀
  = (∫ 𝓕 g₁(ζ) conj(𝓕 g₂(ζ)) π^m / (|2πζ|^m |det A|) dζ) · ∫ f conj h`,

where `Fᵢ(x₀, s) = ∫ gᵢ(⟪y - x₀, A (y - x₀)⟫ + s) fᵢ(y) dy` with `f₁ = f`, `f₂ = h`.  Parseval in
the level at each center, Fubini between the center and the frequency, and the polarized chirp
identity at each nonzero frequency; the frequency integrand is dominated by the arithmetic mean of
the two energies, so only the cross energy is assumed finite.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticLevelShift.lean

complete

theorem MeasureTheory.lintegral_enorm_fourier_mul_enorm_fourier_mul_ne_top
  {g₁ g₂ : ℝ → ℂ}
  (hg₁1 : MeasureTheory.Integrable g₁ MeasureTheory.volume)
  {w : ℝ → ENNReal} (hw : Measurable w)
  (h₁ : ∫⁻ (ζ : ℝ), ‖FourierTransform.fourier g₁ ζ‖ₑ ^ 2 * w ζ ≠ ⊤)
  (h₂ : ∫⁻ (ζ : ℝ), ‖FourierTransform.fourier g₂ ζ‖ₑ ^ 2 * w ζ ≠ ⊤) :
  ∫⁻ (ζ : ℝ),
      ‖FourierTransform.fourier g₁ ζ‖ₑ *
          ‖FourierTransform.fourier g₂ ζ‖ₑ *
        w ζ ≠
    ⊤

theorem MeasureTheory.lintegral_enorm_fourier_mul_enorm_fourier_mul_ne_top
  {g₁ g₂ : ℝ → ℂ}
  (hg₁1 :
    MeasureTheory.Integrable g₁
      MeasureTheory.volume)
  {w : ℝ → ENNReal} (hw : Measurable w)
  (h₁ :
    ∫⁻ (ζ : ℝ),
        ‖FourierTransform.fourier g₁ ζ‖ₑ ^
            2 *
          w ζ ≠
      ⊤)
  (h₂ :
    ∫⁻ (ζ : ℝ),
        ‖FourierTransform.fourier g₂ ζ‖ₑ ^
            2 *
          w ζ ≠
      ⊤) :
  ∫⁻ (ζ : ℝ),
      ‖FourierTransform.fourier g₁ ζ‖ₑ *
          ‖FourierTransform.fourier g₂
              ζ‖ₑ *
        w ζ ≠
    ⊤

Two profiles with finite weighted energies have finite weighted cross energy.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticLevelShift.lean

complete

theorem MeasureTheory.aestronglyMeasurable_quadraticLevelShift.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  (A : E →L[ℝ] E) {g : ℝ → ℂ} (hgm : Measurable g) {f : E → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume) :
  MeasureTheory.AEStronglyMeasurable
    (fun p ↦ ∫ (y : E), g (inner ℝ (y - p.1) (A (y - p.1)) + p.2) * f y)
    MeasureTheory.volume

theorem MeasureTheory.aestronglyMeasurable_quadraticLevelShift.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (A : E →L[ℝ] E) {g : ℝ → ℂ}
  (hgm : Measurable g) {f : E → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume) :
  MeasureTheory.AEStronglyMeasurable
    (fun p ↦
      ∫ (y : E),
        g
            (inner ℝ (y - p.1)
                (A (y - p.1)) +
              p.2) *
          f y)
    MeasureTheory.volume

The level-shift pairing, as a function of the center and the level jointly, is measurable.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticLevelShift.lean

complete

theorem MeasureTheory.lintegral_enorm_quadraticLevelShift_sq.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  (A : E →L[ℝ] E) (hA : IsSelfAdjoint A) (hdet : A.det ≠ 0) {g : ℝ → ℂ}
  (hgm : Measurable g)
  (hg1 : MeasureTheory.Integrable g MeasureTheory.volume) {M : ℝ}
  (hgM : ∀ (u : ℝ), ‖g u‖ ≤ M) {f : E → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) :
  ∫⁻ (p : E × ℝ),
      ‖∫ (y : E), g (inner ℝ (y - p.1) (A (y - p.1)) + p.2) * f y‖ₑ ^
        2 =
    (∫⁻ (ζ : ℝ),
        ‖FourierTransform.fourier g ζ‖ₑ ^ 2 *
          ENNReal.ofReal
            (Real.pi ^ Module.finrank ℝ E /
              (|2 * Real.pi * ζ| ^ Module.finrank ℝ E * |A.det|))) *
      ∫⁻ (y : E), ‖f y‖ₑ ^ 2

theorem MeasureTheory.lintegral_enorm_quadraticLevelShift_sq.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (A : E →L[ℝ] E) (hA : IsSelfAdjoint A)
  (hdet : A.det ≠ 0) {g : ℝ → ℂ}
  (hgm : Measurable g)
  (hg1 :
    MeasureTheory.Integrable g
      MeasureTheory.volume)
  {M : ℝ} (hgM : ∀ (u : ℝ), ‖g u‖ ≤ M)
  {f : E → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (h2 :
    MeasureTheory.MemLp f 2
      MeasureTheory.volume) :
  ∫⁻ (p : E × ℝ),
      ‖∫ (y : E),
            g
                (inner ℝ (y - p.1)
                    (A (y - p.1)) +
                  p.2) *
              f y‖ₑ ^
        2 =
    (∫⁻ (ζ : ℝ),
        ‖FourierTransform.fourier g ζ‖ₑ ^
            2 *
          ENNReal.ofReal
            (Real.pi ^
                Module.finrank ℝ E /
              (|2 * Real.pi * ζ| ^
                  Module.finrank ℝ E *
                |A.det|))) *
      ∫⁻ (y : E), ‖f y‖ₑ ^ 2

**The energy identity on the product**: the same as
`MeasureTheory.lintegral_lintegral_enorm_quadraticLevelShift_sq`, with the center and the level
integrated jointly.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticLevelShift.lean

complete

theorem MeasureTheory.memLp_two_quadraticLevelShift.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (A : E →L[ℝ] E)
  (hA : IsSelfAdjoint A) (hdet : A.det ≠ 0) {g : ℝ → ℂ}
  (hgm : Measurable g)
  (hg1 : MeasureTheory.Integrable g MeasureTheory.volume) {M : ℝ}
  (hgM : ∀ (u : ℝ), ‖g u‖ ≤ M)
  (hadm :
    ∫⁻ (ζ : ℝ),
        ‖FourierTransform.fourier g ζ‖ₑ ^ 2 *
          ENNReal.ofReal
            (Real.pi ^ Module.finrank ℝ E /
              (|2 * Real.pi * ζ| ^ Module.finrank ℝ E * |A.det|)) ≠
      ⊤)
  {f : E → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) :
  MeasureTheory.MemLp
    (fun p ↦ ∫ (y : E), g (inner ℝ (y - p.1) (A (y - p.1)) + p.2) * f y)
    2 MeasureTheory.volume

theorem MeasureTheory.memLp_two_quadraticLevelShift.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (A : E →L[ℝ] E) (hA : IsSelfAdjoint A)
  (hdet : A.det ≠ 0) {g : ℝ → ℂ}
  (hgm : Measurable g)
  (hg1 :
    MeasureTheory.Integrable g
      MeasureTheory.volume)
  {M : ℝ} (hgM : ∀ (u : ℝ), ‖g u‖ ≤ M)
  (hadm :
    ∫⁻ (ζ : ℝ),
        ‖FourierTransform.fourier g ζ‖ₑ ^
            2 *
          ENNReal.ofReal
            (Real.pi ^
                Module.finrank ℝ E /
              (|2 * Real.pi * ζ| ^
                  Module.finrank ℝ E *
                |A.det|)) ≠
      ⊤)
  {f : E → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (h2 :
    MeasureTheory.MemLp f 2
      MeasureTheory.volume) :
  MeasureTheory.MemLp
    (fun p ↦
      ∫ (y : E),
        g
            (inner ℝ (y - p.1)
                (A (y - p.1)) +
              p.2) *
          f y)
    2 MeasureTheory.volume

**The level-shift pairing is square-integrable in the center and the level** for an admissible
profile.

theoremdefined in LeanRidgelet/ToMathlib/QuadraticLevelShift.lean

complete

theorem MeasureTheory.integral_quadraticLevelShift_mul_conj.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (A : E →L[ℝ] E)
  (hA : IsSelfAdjoint A) (hdet : A.det ≠ 0) {g₁ g₂ : ℝ → ℂ}
  (hg₁m : Measurable g₁)
  (hg₁1 : MeasureTheory.Integrable g₁ MeasureTheory.volume) {M₁ : ℝ}
  (hg₁M : ∀ (u : ℝ), ‖g₁ u‖ ≤ M₁) (hg₂m : Measurable g₂)
  (hg₂1 : MeasureTheory.Integrable g₂ MeasureTheory.volume) {M₂ : ℝ}
  (hg₂M : ∀ (u : ℝ), ‖g₂ u‖ ≤ M₂)
  (hadm₁ :
    ∫⁻ (ζ : ℝ),
        ‖FourierTransform.fourier g₁ ζ‖ₑ ^ 2 *
          ENNReal.ofReal
            (Real.pi ^ Module.finrank ℝ E /
              (|2 * Real.pi * ζ| ^ Module.finrank ℝ E * |A.det|)) ≠
      ⊤)
  (hadm₂ :
    ∫⁻ (ζ : ℝ),
        ‖FourierTransform.fourier g₂ ζ‖ₑ ^ 2 *
          ENNReal.ofReal
            (Real.pi ^ Module.finrank ℝ E /
              (|2 * Real.pi * ζ| ^ Module.finrank ℝ E * |A.det|)) ≠
      ⊤)
  {f h : E → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume)
  (hh : MeasureTheory.Integrable h MeasureTheory.volume)
  (hh2 : MeasureTheory.MemLp h 2 MeasureTheory.volume) :
  ∫ (p : E × ℝ),
      (∫ (y : E), g₁ (inner ℝ (y - p.1) (A (y - p.1)) + p.2) * f y) *
        (starRingEnd ℂ)
          (∫ (y : E),
            g₂ (inner ℝ (y - p.1) (A (y - p.1)) + p.2) * h y) =
    (∫ (ζ : ℝ),
        FourierTransform.fourier g₁ ζ *
            (starRingEnd ℂ) (FourierTransform.fourier g₂ ζ) *
          ↑(Real.pi ^ Module.finrank ℝ E /
              (|2 * Real.pi * ζ| ^ Module.finrank ℝ E * |A.det|))) *
      ∫ (y : E), f y * (starRingEnd ℂ) (h y)

theorem MeasureTheory.integral_quadraticLevelShift_mul_conj.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (A : E →L[ℝ] E) (hA : IsSelfAdjoint A)
  (hdet : A.det ≠ 0) {g₁ g₂ : ℝ → ℂ}
  (hg₁m : Measurable g₁)
  (hg₁1 :
    MeasureTheory.Integrable g₁
      MeasureTheory.volume)
  {M₁ : ℝ} (hg₁M : ∀ (u : ℝ), ‖g₁ u‖ ≤ M₁)
  (hg₂m : Measurable g₂)
  (hg₂1 :
    MeasureTheory.Integrable g₂
      MeasureTheory.volume)
  {M₂ : ℝ} (hg₂M : ∀ (u : ℝ), ‖g₂ u‖ ≤ M₂)
  (hadm₁ :
    ∫⁻ (ζ : ℝ),
        ‖FourierTransform.fourier g₁ ζ‖ₑ ^
            2 *
          ENNReal.ofReal
            (Real.pi ^
                Module.finrank ℝ E /
              (|2 * Real.pi * ζ| ^
                  Module.finrank ℝ E *
                |A.det|)) ≠
      ⊤)
  (hadm₂ :
    ∫⁻ (ζ : ℝ),
        ‖FourierTransform.fourier g₂ ζ‖ₑ ^
            2 *
          ENNReal.ofReal
            (Real.pi ^
                Module.finrank ℝ E /
              (|2 * Real.pi * ζ| ^
                  Module.finrank ℝ E *
                |A.det|)) ≠
      ⊤)
  {f h : E → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hf2 :
    MeasureTheory.MemLp f 2
      MeasureTheory.volume)
  (hh :
    MeasureTheory.Integrable h
      MeasureTheory.volume)
  (hh2 :
    MeasureTheory.MemLp h 2
      MeasureTheory.volume) :
  ∫ (p : E × ℝ),
      (∫ (y : E),
          g₁
              (inner ℝ (y - p.1)
                  (A (y - p.1)) +
                p.2) *
            f y) *
        (starRingEnd ℂ)
          (∫ (y : E),
            g₂
                (inner ℝ (y - p.1)
                    (A (y - p.1)) +
                  p.2) *
              h y) =
    (∫ (ζ : ℝ),
        FourierTransform.fourier g₁ ζ *
            (starRingEnd ℂ)
              (FourierTransform.fourier g₂
                ζ) *
          ↑(Real.pi ^ Module.finrank ℝ E /
              (|2 * Real.pi * ζ| ^
                  Module.finrank ℝ E *
                |A.det|))) *
      ∫ (y : E),
        f y * (starRingEnd ℂ) (h y)

**The polarized energy identity, in the `L²` inner product of the center and the level.**

Read for the quadratic-form network at a fixed symmetric coefficient, the identity says that the analysis transform over the translation and level parameters is, up to the constant, an isometry into L^2 — the weight |\zeta|^{-m} being the hyperplane one — and that the constant scales like |\det A|^{-1}. Against a parameter measure whose coefficient marginal is the invariant measure of the cone of positive definite operators, the total analysis energy is therefore that measure's total mass times the constant, which is infinite for every nonzero profile; the consequence for the admissibility statement of the track is recorded in its quadratic chapter. The polarized identity is proved directly — Parseval in the level at each center, Fubini between the center and the frequency with the frequency integrand dominated by the arithmetic mean of the two energies, and the polarized chirp identity at each nonzero frequency — rather than by polarizing the energy identity, and it is what the fixed-shape endpoint of the quadratic chapter consumes: read there, it says the composite of analysis against g_1 and synthesis against g_2 is the constant in parentheses times the identity, a Fourier multiplier constant in the frequency because the modulus of the Fourier transform of a chirp is.

Theorem5.2.7

uses 1used by 1✓L∃∀N

Fourier covariance under affine changes of variables. For an invertible real linear map L, pullback by L⁻¹ contributes the determinant and applies Lᵀ to frequency. Translation contributes the corresponding Fourier character. Combining the two gives \mathcal F[f\circ g^{-1}](\xi)=|\det L|\,\mathbf e(-\langle g(0),\xi\rangle)\,\mathcal Ff(L^T\xi). For the unitary affine pullback with coefficient |\det L|^{-1/2}, the remaining frequency-side coefficient is |\det L|^{1/2}. The proof uses the additive-Haar determinant formula and the Bochner integral_map_equiv API; it is valid for arbitrary finite-dimensional real inner-product spaces and does not depend on ridgelets.

Lean code for Theorem5.2.7●6 theorems

theoremdefined in LeanRidgelet/ToMathlib/FourierAffine.lean

complete

theorem MeasureTheory.integral_comp_linearEquiv_symm.{u_1, u_2} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℝ F] (L : V ≃ₗ[ℝ] V) (f : V → F) :
  ∫ (x : V), f (L.symm x) = ↑‖LinearMap.det ↑L‖₊ • ∫ (x : V), f x

theorem MeasureTheory.integral_comp_linearEquiv_symm.{u_1,
    u_2}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  {F : Type u_2} [NormedAddCommGroup F]
  [NormedSpace ℝ F] (L : V ≃ₗ[ℝ] V)
  (f : V → F) :
  ∫ (x : V), f (L.symm x) =
    ↑‖LinearMap.det ↑L‖₊ • ∫ (x : V), f x

Bochner integration after pullback by the inverse of an invertible real linear map. The
statement is unconditional: if either side is non-integrable then both Bochner integrals use the
usual zero convention.

theoremdefined in LeanRidgelet/ToMathlib/FourierAffine.lean

complete

theorem MeasureTheory.fourier_comp_linearEquiv_symm.{u_1, u_2} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℂ F] (L : V ≃ₗ[ℝ] V) (f : V → F)
  (xi : V) :
  FourierTransform.fourier (fun x ↦ f (L.symm x)) xi =
    ↑‖LinearMap.det ↑L‖₊ • FourierTransform.fourier f (L.adjoint xi)

theorem MeasureTheory.fourier_comp_linearEquiv_symm.{u_1,
    u_2}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  {F : Type u_2} [NormedAddCommGroup F]
  [NormedSpace ℂ F] (L : V ≃ₗ[ℝ] V)
  (f : V → F) (xi : V) :
  FourierTransform.fourier
      (fun x ↦ f (L.symm x)) xi =
    ↑‖LinearMap.det ↑L‖₊ •
      FourierTransform.fourier f
        (L.adjoint xi)

Fourier transform of pullback by the inverse of an invertible real linear map.

theoremdefined in LeanRidgelet/ToMathlib/FourierAffine.lean

complete

theorem MeasureTheory.fourier_comp_sub.{u_1, u_2} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℂ F] (f : V → F) (b xi : V) :
  FourierTransform.fourier (fun x ↦ f (x - b)) xi =
    Real.fourierChar (-inner ℝ b xi) • FourierTransform.fourier f xi

theorem MeasureTheory.fourier_comp_sub.{u_1, u_2}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  {F : Type u_2} [NormedAddCommGroup F]
  [NormedSpace ℂ F] (f : V → F)
  (b xi : V) :
  FourierTransform.fourier
      (fun x ↦ f (x - b)) xi =
    Real.fourierChar (-inner ℝ b xi) •
      FourierTransform.fourier f xi

Fourier transform converts translation of the argument into multiplication by a character.

theoremdefined in LeanRidgelet/ToMathlib/FourierAffine.lean

complete

theorem MeasureTheory.affineEquiv_symm_apply.{u_1} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] (g : V ≃ᵃ[ℝ] V)
  (x : V) : g.symm x = g.linear.symm (x - g 0)

theorem MeasureTheory.affineEquiv_symm_apply.{u_1}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] (g : V ≃ᵃ[ℝ] V)
  (x : V) :
  g.symm x = g.linear.symm (x - g 0)

The inverse of an affine equivalence is its inverse linear part applied after subtracting the
translation vector.

theoremdefined in LeanRidgelet/ToMathlib/FourierAffine.lean

complete

theorem MeasureTheory.fourier_comp_affineEquiv_symm.{u_1, u_2} {V : Type u_1}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℂ F] (g : V ≃ᵃ[ℝ] V) (f : V → F)
  (xi : V) :
  FourierTransform.fourier (fun x ↦ f (g.symm x)) xi =
    Real.fourierChar (-inner ℝ (g 0) xi) •
      ↑‖LinearMap.det ↑g.linear‖₊ •
        FourierTransform.fourier f (g.linear.adjoint xi)

theorem MeasureTheory.fourier_comp_affineEquiv_symm.{u_1,
    u_2}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  {F : Type u_2} [NormedAddCommGroup F]
  [NormedSpace ℂ F] (g : V ≃ᵃ[ℝ] V)
  (f : V → F) (xi : V) :
  FourierTransform.fourier
      (fun x ↦ f (g.symm x)) xi =
    Real.fourierChar (-inner ℝ (g 0) xi) •
      ↑‖LinearMap.det ↑g.linear‖₊ •
        FourierTransform.fourier f
          (g.linear.adjoint xi)

Fourier transform of pullback by the inverse of an affine equivalence.

theoremdefined in LeanRidgelet/ToMathlib/FourierAffine.lean

complete

theorem MeasureTheory.fourier_weighted_comp_affineEquiv_symm.{u_1}
  {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V]
  (g : V ≃ᵃ[ℝ] V) (f : V → ℂ) (xi : V) :
  FourierTransform.fourier
      (fun x ↦
        (↑↑(NNReal.sqrt ‖LinearMap.det ↑g.linear‖₊))⁻¹ • f (g.symm x))
      xi =
    Real.fourierChar (-inner ℝ (g 0) xi) •
      ↑↑(NNReal.sqrt ‖LinearMap.det ↑g.linear‖₊) •
        FourierTransform.fourier f (g.linear.adjoint xi)

theorem MeasureTheory.fourier_weighted_comp_affineEquiv_symm.{u_1}
  {V : Type u_1} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  (g : V ≃ᵃ[ℝ] V) (f : V → ℂ) (xi : V) :
  FourierTransform.fourier
      (fun x ↦
        (↑↑(NNReal.sqrt
                  ‖LinearMap.det
                      ↑g.linear‖₊))⁻¹ •
          f (g.symm x))
      xi =
    Real.fourierChar (-inner ℝ (g 0) xi) •
      ↑↑(NNReal.sqrt
              ‖LinearMap.det
                  ↑g.linear‖₊) •
        FourierTransform.fourier f
          (g.linear.adjoint xi)

Fourier covariance of the determinant-weighted affine pullback used in the unitary `L²`
representation. The Jacobian factor on the Fourier side is the square root rather than its
inverse.

Theorem5.2.8

uses 0used by 1✓L∃∀N

The second moment of the Fourier transform is the second derivative at the origin. For a smooth compactly supported g:\mathbb R\to\mathbb C, \int_{\mathbb R}(2\pi w)^2\mathcal Fg(w)\,\mathrm dw=-g''(0), that is \int_{\mathbb R}\lambda^2\hat g(\lambda)\,\mathrm d\lambda=-2\pi g''(0) for the angular transform \hat g(\lambda)=\int e^{-i\lambda t}g(t)\,\mathrm dt=\mathcal Fg(\lambda/2\pi). Two applications of Mathlib's \mathcal F(g')=2\pi iw\,\mathcal Fg turn the integrand into -\mathcal F(g''), whose integral is g''(0) by Fourier inversion at the origin; the integrability of \mathcal F(g'') that inversion needs comes from g'' being a Schwartz function.

Lean code for Theorem5.2.8●5 theorems

theoremdefined in LeanRidgelet/ToMathlib/FourierSecondMoment.lean

complete

theorem Real.integral_exp_neg_I_mul_mul_eq_fourier (g : ℝ → ℂ) (lam : ℝ) :
  ∫ (t : ℝ), Complex.exp (-(Complex.I * ↑lam * ↑t)) * g t =
    FourierTransform.fourier g (lam / (2 * Real.pi))

theorem Real.integral_exp_neg_I_mul_mul_eq_fourier
  (g : ℝ → ℂ) (lam : ℝ) :
  ∫ (t : ℝ),
      Complex.exp
          (-(Complex.I * ↑lam * ↑t)) *
        g t =
    FourierTransform.fourier g
      (lam / (2 * Real.pi))

The angular Fourier transform `∫ e^{-iλt} g(t) dt` is Mathlib's `𝓕g` at the rescaled frequency
`λ/2π`.

theoremdefined in LeanRidgelet/ToMathlib/FourierSecondMoment.lean

complete

theorem Real.integral_fourier_eq_apply_zero {g : ℝ → ℂ} (hg : Continuous g)
  (hint : MeasureTheory.Integrable g MeasureTheory.volume)
  (hint' :
    MeasureTheory.Integrable (FourierTransform.fourier g)
      MeasureTheory.volume) :
  ∫ (w : ℝ), FourierTransform.fourier g w = g 0

theorem Real.integral_fourier_eq_apply_zero
  {g : ℝ → ℂ} (hg : Continuous g)
  (hint :
    MeasureTheory.Integrable g
      MeasureTheory.volume)
  (hint' :
    MeasureTheory.Integrable
      (FourierTransform.fourier g)
      MeasureTheory.volume) :
  ∫ (w : ℝ),
      FourierTransform.fourier g w =
    g 0

Fourier inversion at the origin, `∫ 𝓕g(w) dw = g(0)`, for a continuous integrable `g` with
integrable Fourier transform.

theoremdefined in LeanRidgelet/ToMathlib/FourierSecondMoment.lean

complete

theorem Real.integrable_fourier_of_hasCompactSupport {g : ℝ → ℂ}
  (hg : ContDiff ℝ (↑⊤) g) (hsupp : HasCompactSupport g) :
  MeasureTheory.Integrable (FourierTransform.fourier g)
    MeasureTheory.volume

theorem Real.integrable_fourier_of_hasCompactSupport
  {g : ℝ → ℂ} (hg : ContDiff ℝ (↑⊤) g)
  (hsupp : HasCompactSupport g) :
  MeasureTheory.Integrable
    (FourierTransform.fourier g)
    MeasureTheory.volume

The Fourier transform of a smooth compactly supported function is integrable: such a function
is a Schwartz function, and the Fourier transform of a Schwartz function is Schwartz.

theoremdefined in LeanRidgelet/ToMathlib/FourierSecondMoment.lean

complete

theorem Real.integral_two_pi_mul_sq_mul_fourier {g : ℝ → ℂ}
  (hg : ContDiff ℝ (↑⊤) g) (hsupp : HasCompactSupport g) :
  ∫ (w : ℝ), ↑(2 * Real.pi * w) ^ 2 * FourierTransform.fourier g w =
    -deriv (deriv g) 0

theorem Real.integral_two_pi_mul_sq_mul_fourier
  {g : ℝ → ℂ} (hg : ContDiff ℝ (↑⊤) g)
  (hsupp : HasCompactSupport g) :
  ∫ (w : ℝ),
      ↑(2 * Real.pi * w) ^ 2 *
        FourierTransform.fourier g w =
    -deriv (deriv g) 0

**The second moment of the Fourier transform**: for a smooth compactly supported `g : ℝ → ℂ`,
`∫ (2πw)² 𝓕g(w) dw = -g''(0)`. Two applications of `𝓕(g') = 2πiw 𝓕g` turn the integrand into
`-𝓕(g'')`, and Fourier inversion at the origin evaluates its integral.

theoremdefined in LeanRidgelet/ToMathlib/FourierSecondMoment.lean

complete

theorem Real.integral_sq_mul_integral_exp_neg_I_mul_mul {g : ℝ → ℂ}
  (hg : ContDiff ℝ (↑⊤) g) (hsupp : HasCompactSupport g) :
  ∫ (lam : ℝ),
      ↑lam ^ 2 *
        ∫ (t : ℝ), Complex.exp (-(Complex.I * ↑lam * ↑t)) * g t =
    -(2 * ↑Real.pi) * deriv (deriv g) 0

theorem Real.integral_sq_mul_integral_exp_neg_I_mul_mul
  {g : ℝ → ℂ} (hg : ContDiff ℝ (↑⊤) g)
  (hsupp : HasCompactSupport g) :
  ∫ (lam : ℝ),
      ↑lam ^ 2 *
        ∫ (t : ℝ),
          Complex.exp
              (-(Complex.I * ↑lam * ↑t)) *
            g t =
    -(2 * ↑Real.pi) * deriv (deriv g) 0

**The second moment in the angular normalization**: for a smooth compactly supported
`g : ℝ → ℂ` and `ĝ(λ) = ∫ e^{-iλt} g(t) dt`,

`∫_ℝ λ² ĝ(λ) dλ = -2π g''(0)`.

The factor `2π` is the Jacobian of the frequency rescaling `λ = 2πw` between the angular and the
Mathlib normalizations.

This is the one-dimensional Fourier input of the inversion formula for the spherical transform on odd-dimensional hyperbolic space, where the Plancherel density is a polynomial in the frequency — on \mathbb H^3 a multiple of \lambda^2 — and inversion reduces to this identity applied to the Abel transform. The factor 2\pi between the two forms is the Jacobian of the frequency rescaling, as everywhere in this project.

Theorem5.2.9

uses 0used by 1✓L∃∀N

Smoothness of a parametric integral over a compact space. Mathlib differentiates under the integral sign once (hasDerivAt_integral_of_dominated_loc_of_deriv_le), against a dominating function to be supplied. When the variable of integration ranges over a compact space with a finite measure and the integrand is jointly C^n — as g : ℝ × E → F composed with a continuous φ : X → E — the dominating function is a constant produced by compactness, and induction on n gives that r\mapsto\int g(r,\varphi(x))\,\mathrm d\nu(x) is C^n, for every finite n and for n=\infty.

Lean code for Theorem5.2.9●5 theorems

theoremdefined in LeanRidgelet/ToMathlib/ContDiffParametricIntegral.lean

complete

theorem MeasureTheory.Continuous.integrable_of_compactSpace'.{u_1, u_3}
  {X : Type u_1} {F : Type u_3} [TopologicalSpace X] [CompactSpace X]
  [MeasurableSpace X] [OpensMeasurableSpace X] [NormedAddCommGroup F]
  (ν : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure ν]
  {h : X → F} (hh : Continuous h) : MeasureTheory.Integrable h ν

theorem MeasureTheory.Continuous.integrable_of_compactSpace'.{u_1,
    u_3}
  {X : Type u_1} {F : Type u_3}
  [TopologicalSpace X] [CompactSpace X]
  [MeasurableSpace X]
  [OpensMeasurableSpace X]
  [NormedAddCommGroup F]
  (ν : MeasureTheory.Measure X)
  [MeasureTheory.IsFiniteMeasure ν]
  {h : X → F} (hh : Continuous h) :
  MeasureTheory.Integrable h ν

On a compact space with a finite measure a continuous function is integrable.

theoremdefined in LeanRidgelet/ToMathlib/ContDiffParametricIntegral.lean

complete

theorem MeasureTheory.continuous_integral_of_compactSpace.{u_1, u_2, u_3}
  {X : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace X]
  [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X]
  [SecondCountableTopology X] [NormedAddCommGroup E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] (ν : MeasureTheory.Measure X)
  [MeasureTheory.IsFiniteMeasure ν] {φ : X → E} (hφ : Continuous φ)
  {g : ℝ × E → F} (hg : Continuous g) :
  Continuous fun r ↦ ∫ (x : X), g (r, φ x) ∂ν

theorem MeasureTheory.continuous_integral_of_compactSpace.{u_1,
    u_2, u_3}
  {X : Type u_1} {E : Type u_2}
  {F : Type u_3} [TopologicalSpace X]
  [CompactSpace X] [MeasurableSpace X]
  [OpensMeasurableSpace X]
  [SecondCountableTopology X]
  [NormedAddCommGroup E]
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  (ν : MeasureTheory.Measure X)
  [MeasureTheory.IsFiniteMeasure ν]
  {φ : X → E} (hφ : Continuous φ)
  {g : ℝ × E → F} (hg : Continuous g) :
  Continuous fun r ↦
    ∫ (x : X), g (r, φ x) ∂ν

Continuity of a parametric integral over a compact space with a finite measure, for a jointly
continuous integrand: the dominating function is the maximum of the integrand on
`closedBall r₀ 1 × φ(X)`.

theoremdefined in LeanRidgelet/ToMathlib/ContDiffParametricIntegral.lean

complete

theorem MeasureTheory.hasDerivAt_integral_of_compactSpace.{u_1, u_2, u_3}
  {X : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace X]
  [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X]
  [SecondCountableTopology X] [NormedAddCommGroup E] [NormedSpace ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] (ν : MeasureTheory.Measure X)
  [MeasureTheory.IsFiniteMeasure ν] {φ : X → E} (hφ : Continuous φ)
  {g : ℝ × E → F} (hg : ContDiff ℝ 1 g) (r₀ : ℝ) :
  HasDerivAt (fun r ↦ ∫ (x : X), g (r, φ x) ∂ν)
    (∫ (x : X), (fderiv ℝ g (r₀, φ x)) (1, 0) ∂ν) r₀

theorem MeasureTheory.hasDerivAt_integral_of_compactSpace.{u_1,
    u_2, u_3}
  {X : Type u_1} {E : Type u_2}
  {F : Type u_3} [TopologicalSpace X]
  [CompactSpace X] [MeasurableSpace X]
  [OpensMeasurableSpace X]
  [SecondCountableTopology X]
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  (ν : MeasureTheory.Measure X)
  [MeasureTheory.IsFiniteMeasure ν]
  {φ : X → E} (hφ : Continuous φ)
  {g : ℝ × E → F} (hg : ContDiff ℝ 1 g)
  (r₀ : ℝ) :
  HasDerivAt
    (fun r ↦ ∫ (x : X), g (r, φ x) ∂ν)
    (∫ (x : X),
      (fderiv ℝ g (r₀, φ x)) (1, 0) ∂ν)
    r₀

**Differentiation under the integral sign over a compact space.** For a jointly `C^1`
integrand the parametric integral is differentiable, with derivative the integral of the partial
derivative in the parameter.

theoremdefined in LeanRidgelet/ToMathlib/ContDiffParametricIntegral.lean

complete

theorem MeasureTheory.contDiff_integral_of_compactSpace.{u_1, u_2, u_3}
  {X : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace X]
  [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X]
  [SecondCountableTopology X] [NormedAddCommGroup E] [NormedSpace ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] (ν : MeasureTheory.Measure X)
  [MeasureTheory.IsFiniteMeasure ν] {φ : X → E} (hφ : Continuous φ)
  {n : ℕ} {g : ℝ × E → F} (hg : ContDiff ℝ (↑n) g) :
  ContDiff ℝ ↑n fun r ↦ ∫ (x : X), g (r, φ x) ∂ν

theorem MeasureTheory.contDiff_integral_of_compactSpace.{u_1,
    u_2, u_3}
  {X : Type u_1} {E : Type u_2}
  {F : Type u_3} [TopologicalSpace X]
  [CompactSpace X] [MeasurableSpace X]
  [OpensMeasurableSpace X]
  [SecondCountableTopology X]
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  (ν : MeasureTheory.Measure X)
  [MeasureTheory.IsFiniteMeasure ν]
  {φ : X → E} (hφ : Continuous φ) {n : ℕ}
  {g : ℝ × E → F}
  (hg : ContDiff ℝ (↑n) g) :
  ContDiff ℝ ↑n fun r ↦
    ∫ (x : X), g (r, φ x) ∂ν

**Smoothness of a parametric integral over a compact space.** For a jointly `C^n` integrand
`g : ℝ × E → F`, a continuous `φ : X → E` on a compact space and a finite measure `ν` on `X`, the
parametric integral `r ↦ ∫ g(r, φ x) dν(x)` is `C^n`.

theoremdefined in LeanRidgelet/ToMathlib/ContDiffParametricIntegral.lean

complete

theorem MeasureTheory.contDiff_infty_integral_of_compactSpace.{u_1, u_2, u_3}
  {X : Type u_1} {E : Type u_2} {F : Type u_3} [TopologicalSpace X]
  [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X]
  [SecondCountableTopology X] [NormedAddCommGroup E] [NormedSpace ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] (ν : MeasureTheory.Measure X)
  [MeasureTheory.IsFiniteMeasure ν] {φ : X → E} (hφ : Continuous φ)
  {g : ℝ × E → F} (hg : ContDiff ℝ (↑⊤) g) :
  ContDiff ℝ ↑⊤ fun r ↦ ∫ (x : X), g (r, φ x) ∂ν

theorem MeasureTheory.contDiff_infty_integral_of_compactSpace.{u_1,
    u_2, u_3}
  {X : Type u_1} {E : Type u_2}
  {F : Type u_3} [TopologicalSpace X]
  [CompactSpace X] [MeasurableSpace X]
  [OpensMeasurableSpace X]
  [SecondCountableTopology X]
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  (ν : MeasureTheory.Measure X)
  [MeasureTheory.IsFiniteMeasure ν]
  {φ : X → E} (hφ : Continuous φ)
  {g : ℝ × E → F}
  (hg : ContDiff ℝ (↑⊤) g) :
  ContDiff ℝ ↑⊤ fun r ↦
    ∫ (x : X), g (r, φ x) ∂ν

The `C^∞` case of `MeasureTheory.contDiff_integral_of_compactSpace`.

The typical instance is the spherical average r\mapsto\int_{\mathbb S^{m-1}}f(ru)\,\mathrm du of a smooth function, which is where the smoothness of a test function enters the inversion formula on hyperbolic space: it makes the Abel transform of the radialization a smooth compactly supported function.

Theorem5.2.10

uses 0

Used by 2

Reverse dependency previews

Preview

Lemma 2.2.9

Loading preview

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

✓L∃∀N

Almost-everywhere Fourier inversion. Mathlib's inversion theorem (MeasureTheory.Integrable.fourierInv_fourier_eq) recovers an integrable function with integrable Fourier transform at its continuity points; the almost-everywhere counterpart with no continuity hypothesis is absent. It is proved here: for f integrable on a finite-dimensional real inner product space with 𝓕 f integrable, \mathcal F^{-1}[\mathcal F f]=f almost everywhere. The proof pairs both sides against Schwartz functions — a Fubini swap computes the pairing of \mathcal F^{-1}\mathcal F f against \varphi as the pairing of \mathcal F f against \mathcal F^{-1}\varphi, the multiplication formula (VectorFourier.integral_fourierIntegral_smul_eq_flip) moves the transform back to f, and the Schwartz inversion closes the circle — and concludes with ae_eq_of_integral_contDiff_smul_eq.

Lean code for Theorem5.2.10●1 theorem

theoremdefined in LeanRidgelet/ToMathlib/FourierInversion.lean

complete

theorem MeasureTheory.Integrable.fourierInv_fourier_ae_eq.{u_1, u_2}
  {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V]
  [BorelSpace V] [NormedAddCommGroup E] [NormedSpace ℂ E]
  [CompleteSpace E] {f : V → E}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (h'f :
    MeasureTheory.Integrable (FourierTransform.fourier f)
      MeasureTheory.volume) :
  FourierTransformInv.fourierInv
      (FourierTransform.fourier f) =ᵐ[MeasureTheory.volume]
    f

theorem MeasureTheory.Integrable.fourierInv_fourier_ae_eq.{u_1,
    u_2}
  {V : Type u_1} {E : Type u_2}
  [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  [NormedAddCommGroup E] [NormedSpace ℂ E]
  [CompleteSpace E] {f : V → E}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (h'f :
    MeasureTheory.Integrable
      (FourierTransform.fourier f)
      MeasureTheory.volume) :
  FourierTransformInv.fourierInv
      (FourierTransform.fourier
        f) =ᵐ[MeasureTheory.volume]
    f

**Almost-everywhere Fourier inversion**: if `f` is integrable and its Fourier transform is
integrable, then `𝓕⁻ (𝓕 f) = f` almost everywhere.