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 3

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

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.5●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.6

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.6●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.