Lean Ridgelet Blueprint

2.2. L1 theory: formalization details🔗

The machinery behind the main results of the previous chapter, organized by Lean dependency rather than by publication order. Each section corresponds to one file of LeanRidgelet/L1/; the three files whose results are already stated in full in the overview chapter — L1.Balancing, L1.StructureTheorem and L1.Radon — have no section of their own here. The general-purpose analytic input — the Radon transform, Young's inequality, the Hilbert transform, polar coordinates, weighted L¹ smoothing, the L² duality criterion — is stated in Mathlib generality in the upstream-candidates chapter and only specialized here.

L1.Defs, L1.FourierExpression: the two identities the theory runs on

Theorem2.2.1
Statement uses 3
Statement dependency previews
Preview
Definition 2.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

Fourier slice theorem in the article convention. For f\in L^1(\mathbb R^m) and every unit direction \boldsymbol{u}, the slice identity \widehat f(\omega\boldsymbol{u})=\widehat{\mathscr Rf(\boldsymbol{u},\cdot)}(\omega) holds in the article Fourier convention, bridging the m-dimensional and one-dimensional transforms. The article quotes the slice theorem and the Fubini corollary \int\mathscr Rf(\boldsymbol{u},p)\,dp=\int f without proof; both are proved, the latter in the upstream chapter, for every unit direction rather than almost every.

Lean code for Theorem2.2.1●1 theorem
  • theoremdefined in LeanRidgelet/L1/Defs.lean
    complete
    theorem LeanRidgelet.angularFourier_slice_radonTransform {m : ℕ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (u : LeanRidgelet.InputSpace m) (hu : ‖u‖ = 1) (ω : ℝ) :
  LeanRidgelet.Fourier.angularFourierIntegralInner f (ω • u) =
    LeanRidgelet.angularFourier1D (MeasureTheory.radonTransform f u) ω
    theorem LeanRidgelet.angularFourier_slice_radonTransform
  {m : ℕ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (u : LeanRidgelet.InputSpace m)
  (hu : ‖u‖ = 1) (ω : ℝ) :
  LeanRidgelet.Fourier.angularFourierIntegralInner
      f (ω • u) =
    LeanRidgelet.angularFourier1D
      (MeasureTheory.radonTransform f u) ω
    **Fourier slice theorem** (Section 2.4 of the manuscript) in the angular Fourier
convention: the `m`-dimensional angular Fourier transform of `f ∈ L¹(ℝ^m)`, restricted to the
ray through a unit vector `u`, is the one-dimensional angular Fourier transform of the Radon
transform: `f̂(ω • u) = (R[f](u, ·))^(ω)`. The Mathlib-convention version for a general
finite-dimensional inner product space is `MeasureTheory.fourier_slice_radonTransform`.
Theorem2.2.2
Statement uses 2
Statement dependency previews
Preview
Definition 2.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
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

Fourier expression of the ridgelet transform (eq:fstridge). For f\in L^1(\mathbb R^m), \psi\in L^1(\mathbb R), every weight \boldsymbol{a} and bias frequency \zeta, \widehat{\mathscr R_\psi f(\boldsymbol{a},\cdot)}(\zeta)=\widehat f(\zeta\boldsymbol{a})\,\overline{\widehat\psi(\zeta)}\,\|\boldsymbol{a}\|^s, where the hat on the left is the one-dimensional article Fourier transform in the bias. In the bias-frequency domain the ridgelet transform is the Fourier slice data \widehat f(\zeta\boldsymbol{a}) weighted by the conjugate activation spectrum. This is the bridge between the L1 transform and the unitary Fourier--dilation coordinates T of the L2 theory, and the engine behind thm:parseval and thm:L2. The proof uses the measure-preserving preactivation shear (\boldsymbol{a},z)\mapsto(\boldsymbol{a},\langle\boldsymbol{a},x\rangle-z) and a one-dimensional reflected translation. The first three declarations are the accompanying L¹ and L² bias-section estimates.

Lean code for Theorem2.2.2●4 theorems
  • theoremdefined in LeanRidgelet/L1/FourierExpression.lean
    complete
    theorem LeanRidgelet.integrable_ridgelet_bias_kernel {m : ℕ} {ψ : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hψ : MeasureTheory.Integrable ψ MeasureTheory.volume)
  (a : LeanRidgelet.InputSpace m) :
  MeasureTheory.Integrable
    (fun q ↦ f q.2 * (starRingEnd ℂ) (ψ (inner ℝ a q.2 - q.1)))
    (MeasureTheory.volume.prod MeasureTheory.volume)
    theorem LeanRidgelet.integrable_ridgelet_bias_kernel
  {m : ℕ} {ψ : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hψ :
    MeasureTheory.Integrable ψ
      MeasureTheory.volume)
  (a : LeanRidgelet.InputSpace m) :
  MeasureTheory.Integrable
    (fun q ↦
      f q.2 *
        (starRingEnd ℂ)
          (ψ (inner ℝ a q.2 - q.1)))
    (MeasureTheory.volume.prod
      MeasureTheory.volume)
    Product-space integrability of the ridgelet bias kernel
`(b, x) ↦ f x ⋅ conj (ψ (⟪a,x⟫ - b))`, through the measure-preserving preactivation shear.
  • theoremdefined in LeanRidgelet/L1/FourierExpression.lean
    complete
    theorem LeanRidgelet.integrable_euclideanRidgeletTransform_bias (m : ℕ) (s : ℝ)
  {ψ : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hψ : MeasureTheory.Integrable ψ MeasureTheory.volume)
  (a : LeanRidgelet.InputSpace m) :
  MeasureTheory.Integrable
    (fun b ↦ LeanRidgelet.euclideanRidgeletTransform m s ψ f (a, b))
    MeasureTheory.volume
    theorem LeanRidgelet.integrable_euclideanRidgeletTransform_bias
  (m : ℕ) (s : ℝ) {ψ : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hψ :
    MeasureTheory.Integrable ψ
      MeasureTheory.volume)
  (a : LeanRidgelet.InputSpace m) :
  MeasureTheory.Integrable
    (fun b ↦
      LeanRidgelet.euclideanRidgeletTransform
        m s ψ f (a, b))
    MeasureTheory.volume
    For `f ∈ L¹(ℝ^m)` and `ψ ∈ L¹(ℝ)`, the ridgelet transform is integrable in the bias
variable at every fixed weight `a`; the `L¹` half of the fiberwise `L²` theory behind
`thm:parseval` and `thm:L2`.
  • theoremdefined in LeanRidgelet/L1/FourierExpression.lean
    complete
    theorem LeanRidgelet.memLp_two_euclideanRidgeletTransform_bias (m : ℕ)
  [NeZero m] (s : ℝ) {ψ : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  {C : ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hψ : MeasureTheory.Integrable ψ MeasureTheory.volume)
  (hψc : Continuous ψ) (hψb : ∀ (z : ℝ), ‖ψ z‖ ≤ C)
  (a : LeanRidgelet.InputSpace m) :
  MeasureTheory.MemLp
    (fun b ↦ LeanRidgelet.euclideanRidgeletTransform m s ψ f (a, b)) 2
    MeasureTheory.volume
    theorem LeanRidgelet.memLp_two_euclideanRidgeletTransform_bias
  (m : ℕ) [NeZero m] (s : ℝ) {ψ : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  {C : ℝ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hψ :
    MeasureTheory.Integrable ψ
      MeasureTheory.volume)
  (hψc : Continuous ψ)
  (hψb : ∀ (z : ℝ), ‖ψ z‖ ≤ C)
  (a : LeanRidgelet.InputSpace m) :
  MeasureTheory.MemLp
    (fun b ↦
      LeanRidgelet.euclideanRidgeletTransform
        m s ψ f (a, b))
    2 MeasureTheory.volume
    For `f ∈ L¹(ℝ^m)` and a bounded continuous `ψ ∈ L¹(ℝ)`, the ridgelet transform is
square-integrable in the bias variable at every fixed weight `a`.
  • theoremdefined in LeanRidgelet/L1/FourierExpression.lean
    complete
    theorem LeanRidgelet.angularFourier1D_euclideanRidgeletTransform (m : ℕ) (s : ℝ)
  {ψ : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hψ : MeasureTheory.Integrable ψ MeasureTheory.volume)
  (a : LeanRidgelet.InputSpace m) (ζ : ℝ) :
  LeanRidgelet.angularFourier1D
      (fun b ↦ LeanRidgelet.euclideanRidgeletTransform m s ψ f (a, b))
      ζ =
    LeanRidgelet.Fourier.angularFourierIntegralInner f (ζ • a) *
        (starRingEnd ℂ) (LeanRidgelet.angularFourier1D ψ ζ) *
      ↑(‖a‖ ^ s)
    theorem LeanRidgelet.angularFourier1D_euclideanRidgeletTransform
  (m : ℕ) (s : ℝ) {ψ : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hψ :
    MeasureTheory.Integrable ψ
      MeasureTheory.volume)
  (a : LeanRidgelet.InputSpace m)
  (ζ : ℝ) :
  LeanRidgelet.angularFourier1D
      (fun b ↦
        LeanRidgelet.euclideanRidgeletTransform
          m s ψ f (a, b))
      ζ =
    LeanRidgelet.Fourier.angularFourierIntegralInner
          f (ζ • a) *
        (starRingEnd ℂ)
          (LeanRidgelet.angularFourier1D ψ
            ζ) *
      ↑(‖a‖ ^ s)
    The Fourier expression of the ridgelet transform in the bias variable (`eq:fstridge`): for
`f ∈ L¹(ℝ^m)` and `ψ ∈ L¹(ℝ)`, at every weight `a` and bias frequency `ζ`,
`(R_ψ f (a, ·))^(ζ) = f̂(ζ a) ⋅ conj (ψ̂ ζ) ⋅ ‖a‖^s`.

This identity is the key link of plan item M7 (B) between the L1 theory and the L2 theory: in
the bias-frequency domain the ridgelet transform is the Fourier slice data `f̂(ζ a)` weighted by
the conjugate activation spectrum, which is exactly the shape of the unitary Fourier--dilation
coordinates `T` of arXiv:2106.04770v2, and it is the engine behind `thm:parseval` and
`thm:L2`.

L1.Lizorkin: the quotient at function level

Lemma2.2.3
Statement uses 2
Statement dependency previews
Preview
Definition 2.1.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

Moments of a spectrum supported away from the origin. All moments \int\zeta^n\widehat\varphi(\zeta)\,d\zeta of the Fourier transform of a Schwartz function \varphi with 0\notin\operatorname{tsupport}\varphi vanish, hence so does the pairing against any polynomial. Since moments are the derivatives of the Fourier transform at the origin (mathlib_lizorkin_space), this is the analytic heart of the invisibility of polynomials, and gives l1_lizorkin_quotient_invariance.

Lean code for Lemma2.2.3●2 theorems
  • theoremdefined in LeanRidgelet/L1/Lizorkin.lean
    complete
    theorem LeanRidgelet.integral_pow_mul_angularFourier1D_eq_zero
  (φ : SchwartzMap ℝ ℂ) (hφ : tsupport ⇑φ ⊆ {0}ᶜ) (n : ℕ) :
  ∫ (ζ : ℝ), ↑ζ ^ n * LeanRidgelet.angularFourier1D (⇑φ) ζ = 0
    theorem LeanRidgelet.integral_pow_mul_angularFourier1D_eq_zero
  (φ : SchwartzMap ℝ ℂ)
  (hφ : tsupport ⇑φ ⊆ {0}ᶜ) (n : ℕ) :
  ∫ (ζ : ℝ),
      ↑ζ ^ n *
        LeanRidgelet.angularFourier1D (⇑φ)
          ζ =
    0
    Moments of the angular Fourier transform of a Schwartz function supported away from the
origin all vanish: `∫ ζ^n φ̂(ζ) dζ = 0`. This is the analytic heart of the invisibility of
polynomials in the Lizorkin quotient.
  • theoremdefined in LeanRidgelet/L1/Lizorkin.lean
    complete
    theorem LeanRidgelet.integral_polynomial_mul_angularFourier1D_eq_zero
  (Q : Polynomial ℂ) (φ : SchwartzMap ℝ ℂ) (hφ : tsupport ⇑φ ⊆ {0}ᶜ) :
  ∫ (z : ℝ),
      Polynomial.eval (↑z) Q * LeanRidgelet.angularFourier1D (⇑φ) z =
    0
    theorem LeanRidgelet.integral_polynomial_mul_angularFourier1D_eq_zero
  (Q : Polynomial ℂ) (φ : SchwartzMap ℝ ℂ)
  (hφ : tsupport ⇑φ ⊆ {0}ᶜ) :
  ∫ (z : ℝ),
      Polynomial.eval (↑z) Q *
        LeanRidgelet.angularFourier1D (⇑φ)
          z =
    0
    Integrating a polynomial against the angular Fourier transform of a Schwartz function
supported away from the origin gives zero.

L1.TruncatedPower: the Gel'fand--Shilov pairing

Lemma2.2.4
Statement uses 2
Statement dependency previews
Preview
Definition 2.1.8
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

The pairing identity for the truncated powers. The identity \int_0^\infty z^k\widehat\varphi(z)\,dz=\int k!/(i\zeta)^{k+1}\varphi(\zeta)\,d\zeta for test functions supported away from the origin is proved by induction on k. The base case computes the half-line integral of an angular Fourier transform through finite truncations, Fubini's theorem and the Riemann--Lebesgue lemma (second declaration); the inductive step trades one power of z for one derivative of the test function through the angular derivative rule \widehat{\varphi'}(\zeta)=i\zeta\widehat\varphi(\zeta) (first declaration) and integrates by parts on the real line.

Lean code for Lemma2.2.4●3 theorems
  • theoremdefined in LeanRidgelet/L1/TruncatedPower.lean
    complete
    theorem LeanRidgelet.angularFourier1D_deriv (φ : SchwartzMap ℝ ℂ) :
  LeanRidgelet.angularFourier1D (deriv ⇑φ) = fun ζ ↦
    Complex.I * ↑ζ * LeanRidgelet.angularFourier1D (⇑φ) ζ
    theorem LeanRidgelet.angularFourier1D_deriv
  (φ : SchwartzMap ℝ ℂ) :
  LeanRidgelet.angularFourier1D
      (deriv ⇑φ) =
    fun ζ ↦
    Complex.I * ↑ζ *
      LeanRidgelet.angularFourier1D (⇑φ) ζ
    The angular-convention derivative rule for Schwartz functions: `(φ')^ (ζ) = i ζ φ̂ (ζ)`.
  • theoremdefined in LeanRidgelet/L1/TruncatedPower.lean
    complete
    theorem LeanRidgelet.setIntegral_Ioi_angularFourier1D (φ : SchwartzMap ℝ ℂ)
  (hφ : tsupport ⇑φ ⊆ {0}ᶜ) :
  ∫ (z : ℝ) in Set.Ioi 0, LeanRidgelet.angularFourier1D (⇑φ) z =
    ∫ (ζ : ℝ), (Complex.I * ↑ζ)⁻¹ * φ ζ
    theorem LeanRidgelet.setIntegral_Ioi_angularFourier1D
  (φ : SchwartzMap ℝ ℂ)
  (hφ : tsupport ⇑φ ⊆ {0}ᶜ) :
  ∫ (z : ℝ) in Set.Ioi 0,
      LeanRidgelet.angularFourier1D (⇑φ)
        z =
    ∫ (ζ : ℝ), (Complex.I * ↑ζ)⁻¹ * φ ζ
    Half-line integral of the angular Fourier transform of a Schwartz function supported away
from the origin: `∫_{0}^{∞} φ̂(z) dz = ∫ (iζ)⁻¹ φ(ζ) dζ`. This is the step-function
(`k = 0`) case of the Gel'fand--Shilov pairing.
  • theoremdefined in LeanRidgelet/L1/TruncatedPower.lean
    complete
    theorem LeanRidgelet.truncatedPowerFourier_pairing (k : ℕ) (φ : SchwartzMap ℝ ℂ)
  (hφ : tsupport ⇑φ ⊆ {0}ᶜ) :
  ∫ (ζ : ℝ), LeanRidgelet.truncatedPowerFourier k ζ * φ ζ =
    ∫ (z : ℝ) in Set.Ioi 0,
      ↑z ^ k * LeanRidgelet.angularFourier1D (⇑φ) z
    theorem LeanRidgelet.truncatedPowerFourier_pairing
  (k : ℕ) (φ : SchwartzMap ℝ ℂ)
  (hφ : tsupport ⇑φ ⊆ {0}ᶜ) :
  ∫ (ζ : ℝ),
      LeanRidgelet.truncatedPowerFourier k
          ζ *
        φ ζ =
    ∫ (z : ℝ) in Set.Ioi 0,
      ↑z ^ k *
        LeanRidgelet.angularFourier1D (⇑φ)
          z
    The Gel'fand--Shilov pairing for truncated powers: for a Schwartz test function supported
away from the origin, `∫ k!/(iζ)^{k+1} φ(ζ) dζ = ∫_{0}^{∞} z^k φ̂(z) dz`.

L1.PairingExtension: absolute convergence and step T4

Lemma2.2.5
Statement uses 2
Statement dependency previews
Preview
Definition 2.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Lemma 2.2.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Absolute-convergence layer for the reconstruction. For an activation with \|\eta(z)\|\le C_\eta(1+|z|)^k and a ridgelet function with finite k-th moment, the convolution kernel w=\overline{\widetilde\psi}*\eta converges absolutely at every point with growth \|w(z)\|\le C_\eta\,(\int(1+|s|)^k\|\psi(s)\|ds)\,(1+|z|)^k (first and second declarations), and for a signal with finite k-th moment the bias pairing of the ridgelet transform factors through it (eq:convdz in Euclidean coordinates, fourth declaration): \int_{\mathbb R}\mathscr R_\psi f(\boldsymbol{a},b)\,\eta(t-b)\,db=\|\boldsymbol{a}\|\int_{\mathbb R^m}f(\boldsymbol{y})\,w(t-\langle\boldsymbol{a},\boldsymbol{y}\rangle)\,d\boldsymbol{y}. Vanishing moments of \psi up to k are inherited by every shifted conjugate section r\mapsto\overline{\psi(r-c)} (third declaration, stated in Mathlib generality in the upstream chapter), the mechanism hiding the polynomial part of the activation.

Lean code for Lemma2.2.5●4 theorems
  • theoremdefined in LeanRidgelet/L1/PairingExtension.lean
    complete
    theorem LeanRidgelet.integrable_reflectedConjConvolution_integrand (k : ℕ)
  {ψ η : ℝ → ℂ} {Cη : ℝ}
  (hψm : MeasureTheory.AEStronglyMeasurable ψ MeasureTheory.volume)
  (hηm : MeasureTheory.AEStronglyMeasurable η MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hηk : ∀ (z : ℝ), ‖η z‖ ≤ Cη * (1 + |z|) ^ k) (z : ℝ) :
  MeasureTheory.Integrable
    (fun t ↦ (starRingEnd ℂ) (ψ (-t)) * η (z - t)) MeasureTheory.volume
    theorem LeanRidgelet.integrable_reflectedConjConvolution_integrand
  (k : ℕ) {ψ η : ℝ → ℂ} {Cη : ℝ}
  (hψm :
    MeasureTheory.AEStronglyMeasurable ψ
      MeasureTheory.volume)
  (hηm :
    MeasureTheory.AEStronglyMeasurable η
      MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable
      (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hηk :
    ∀ (z : ℝ), ‖η z‖ ≤ Cη * (1 + |z|) ^ k)
  (z : ℝ) :
  MeasureTheory.Integrable
    (fun t ↦
      (starRingEnd ℂ) (ψ (-t)) *
        η (z - t))
    MeasureTheory.volume
    Under a `k`-th moment bound on `ψ` and polynomial growth of degree `k` of `η`, the
defining integrand of the convolution `conj (ψ~) ⋆ η` is integrable at every point.
  • theoremdefined in LeanRidgelet/L1/PairingExtension.lean
    complete
    theorem LeanRidgelet.norm_reflectedConjConvolution_le (k : ℕ) {ψ η : ℝ → ℂ}
  {Cη : ℝ}
  (hψk :
    MeasureTheory.Integrable (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hηk : ∀ (z : ℝ), ‖η z‖ ≤ Cη * (1 + |z|) ^ k) (z : ℝ) :
  ‖LeanRidgelet.reflectedConjConvolution ψ η z‖ ≤
    (Cη * ∫ (s : ℝ), (1 + |s|) ^ k * ‖ψ s‖) * (1 + |z|) ^ k
    theorem LeanRidgelet.norm_reflectedConjConvolution_le
  (k : ℕ) {ψ η : ℝ → ℂ} {Cη : ℝ}
  (hψk :
    MeasureTheory.Integrable
      (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hηk :
    ∀ (z : ℝ), ‖η z‖ ≤ Cη * (1 + |z|) ^ k)
  (z : ℝ) :
  ‖LeanRidgelet.reflectedConjConvolution ψ
        η z‖ ≤
    (Cη *
        ∫ (s : ℝ),
          (1 + |s|) ^ k * ‖ψ s‖) *
      (1 + |z|) ^ k
    Under matched moment and growth hypotheses, the convolution `w = conj (ψ~) ⋆ η` obeys the
growth bound `‖w z‖ ≤ Cη ⋅ (∫ (1+|s|)^k ‖ψ s‖ ds) ⋅ (1+|z|)^k` at every point.
  • theoremdefined in LeanRidgelet/ToMathlib/PolynomialGrowth.lean
    complete
    theorem MeasureTheory.integral_pow_mul_conj_comp_sub_eq_zero {ψ : ℝ → ℂ} {k : ℕ}
  (hψm : MeasureTheory.AEStronglyMeasurable ψ MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hψvm : ∀ j ≤ k, ∫ (s : ℝ), ↑s ^ j * ψ s = 0) {j : ℕ} (hj : j ≤ k)
  (c : ℝ) : ∫ (r : ℝ), ↑r ^ j * (starRingEnd ℂ) (ψ (r - c)) = 0
    theorem MeasureTheory.integral_pow_mul_conj_comp_sub_eq_zero
  {ψ : ℝ → ℂ} {k : ℕ}
  (hψm :
    MeasureTheory.AEStronglyMeasurable ψ
      MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable
      (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hψvm :
    ∀ j ≤ k, ∫ (s : ℝ), ↑s ^ j * ψ s = 0)
  {j : ℕ} (hj : j ≤ k) (c : ℝ) :
  ∫ (r : ℝ),
      ↑r ^ j *
        (starRingEnd ℂ) (ψ (r - c)) =
    0
    Vanishing moments are inherited by shifted conjugate sections: if `ψ` has finite `k`-th
moment and vanishing moments up to `k`, then `∫ r^j conj (ψ (r - c)) dr = 0` for every
`j ≤ k` and every shift `c`. This is the mechanism by which the polynomial part of the
function — the kernel of the Lizorkin quotient — becomes invisible to a pairing against a
function with vanishing moments.
  • theoremdefined in LeanRidgelet/L1/PairingExtension.lean
    complete
    theorem LeanRidgelet.integral_euclideanRidgeletTransform_mul_activation
  (m k : ℕ) {ψ η : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ} {Cη : ℝ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hψm : MeasureTheory.AEStronglyMeasurable ψ MeasureTheory.volume)
  (hηm : MeasureTheory.AEStronglyMeasurable η MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hηk : ∀ (z : ℝ), ‖η z‖ ≤ Cη * (1 + |z|) ^ k)
  (a : LeanRidgelet.InputSpace m) (t : ℝ) :
  ∫ (b : ℝ),
      LeanRidgelet.euclideanRidgeletTransform m 1 ψ f (a, b) *
        η (t - b) =
    ↑‖a‖ *
      ∫ (y : LeanRidgelet.InputSpace m),
        f y *
          LeanRidgelet.reflectedConjConvolution ψ η (t - inner ℝ a y)
    theorem LeanRidgelet.integral_euclideanRidgeletTransform_mul_activation
  (m k : ℕ) {ψ η : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  {Cη : ℝ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable
      (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hψm :
    MeasureTheory.AEStronglyMeasurable ψ
      MeasureTheory.volume)
  (hηm :
    MeasureTheory.AEStronglyMeasurable η
      MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable
      (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hηk :
    ∀ (z : ℝ), ‖η z‖ ≤ Cη * (1 + |z|) ^ k)
  (a : LeanRidgelet.InputSpace m)
  (t : ℝ) :
  ∫ (b : ℝ),
      LeanRidgelet.euclideanRidgeletTransform
          m 1 ψ f (a, b) *
        η (t - b) =
    ↑‖a‖ *
      ∫ (y : LeanRidgelet.InputSpace m),
        f y *
          LeanRidgelet.reflectedConjConvolution
            ψ η (t - inner ℝ a y)
    The bias pairing of the ridgelet transform against a polynomially growing activation
factors through the convolution kernel `w = conj (ψ~) ⋆ η` (`eq:convdz` in Euclidean
coordinates): `∫ b, R_ψ f (a, b) ⋅ η (t - b) db = ‖a‖ ⋅ ∫ y, f y ⋅ w (t - ⟨a, y⟩) dy`,
absolutely convergent under matched `k`-th moments of `ψ` and `f`.
Lemma2.2.6
Statement uses 3
Statement dependency previews
Preview
Definition 2.1.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 2.1.17
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Pairing extension for Fourier data away from the origin (step T4). For an activation of growth degree k with Fourier data F_\eta and a weighted-L¹ function \Xi with vanishing moments up to k, \int\eta(z)\,\Xi(z)\,dz=\frac1{2\pi}\int_{\zeta\ne0}F_\eta(\zeta)\,\widehat\Xi(-\zeta)\,d\zeta, provided the right-hand side converges absolutely. The polynomial part of \eta is invisible on both sides — on the right because the integral omits the origin, on the left by the vanishing moments — realizing the dual pairing of the Lizorkin quotient at function level. The proof feeds the Schwartz test functions \varphi_{n,\ell}=c_n\cdot(\kappa_\ell*\chi) — with \chi(\zeta)=\widehat\Xi(-\zeta), a compactly supported mollifier \kappa_\ell, and a smooth cutoff c_n=b(\zeta/n)-b(n\zeta) vanishing near the origin — to the defining pairing; the transform identity \widehat{\varphi_{n,\ell}}(z)=\int\Xi(r)\widehat\kappa_\ell(r)\widehat c_n(z-r)\,dr holds by two absolutely convergent Fubini computations. As \ell\to\infty both sides converge by dominated convergence; as n\to\infty, the splitting \widehat c_n(s)=n\widehat b(ns)-n^{-1}\widehat b(s/n) sends the taper term to 2\pi\int\eta\,\Xi by the weighted approximate identity and kills the low-cut term by the vanishing-moment cancellation, both proved in the upstream chapter (mathlib_weighted_l1_smoothing).

Lean code for Lemma2.2.6●1 theorem
  • theoremdefined in LeanRidgelet/L1/PairingExtension.lean
    complete
    theorem LeanRidgelet.hasFourierAwayFromOrigin_pairing_extension (k : ℕ)
  {η Fη : ℝ → ℂ} (hη : LeanRidgelet.HasFourierAwayFromOrigin η Fη)
  {Cη : ℝ} (hηk : ∀ (z : ℝ), ‖η z‖ ≤ Cη * (1 + |z|) ^ k) {Ξ : ℝ → ℂ}
  (hΞm : MeasureTheory.AEStronglyMeasurable Ξ MeasureTheory.volume)
  (hΞk :
    MeasureTheory.Integrable (fun r ↦ (1 + |r|) ^ k * ‖Ξ r‖)
      MeasureTheory.volume)
  (hΞvm : ∀ j ≤ k, ∫ (r : ℝ), ↑r ^ j * Ξ r = 0)
  (hFΞ :
    MeasureTheory.IntegrableOn
      (fun ζ ↦ Fη ζ * LeanRidgelet.angularFourier1D Ξ (-ζ)) {0}ᶜ
      MeasureTheory.volume) :
  ∫ (z : ℝ), η z * Ξ z =
    ↑(2 * Real.pi)⁻¹ *
      ∫ (ζ : ℝ) in {0}ᶜ, Fη ζ * LeanRidgelet.angularFourier1D Ξ (-ζ)
    theorem LeanRidgelet.hasFourierAwayFromOrigin_pairing_extension
  (k : ℕ) {η Fη : ℝ → ℂ}
  (hη :
    LeanRidgelet.HasFourierAwayFromOrigin
      η Fη)
  {Cη : ℝ}
  (hηk :
    ∀ (z : ℝ), ‖η z‖ ≤ Cη * (1 + |z|) ^ k)
  {Ξ : ℝ → ℂ}
  (hΞm :
    MeasureTheory.AEStronglyMeasurable Ξ
      MeasureTheory.volume)
  (hΞk :
    MeasureTheory.Integrable
      (fun r ↦ (1 + |r|) ^ k * ‖Ξ r‖)
      MeasureTheory.volume)
  (hΞvm :
    ∀ j ≤ k, ∫ (r : ℝ), ↑r ^ j * Ξ r = 0)
  (hFΞ :
    MeasureTheory.IntegrableOn
      (fun ζ ↦
        Fη ζ *
          LeanRidgelet.angularFourier1D Ξ
            (-ζ))
      {0}ᶜ MeasureTheory.volume) :
  ∫ (z : ℝ), η z * Ξ z =
    ↑(2 * Real.pi)⁻¹ *
      ∫ (ζ : ℝ) in {0}ᶜ,
        Fη ζ *
          LeanRidgelet.angularFourier1D Ξ
            (-ζ)
    **Pairing extension for Fourier data away from the origin** (step T4 of the
reconstruction plan): for an activation `η` of polynomial growth degree `k` with Fourier data
`Fη` away from the origin, and a weighted-`L¹` function `Ξ` with vanishing moments up to `k`,
the pairing `∫ η Ξ` is computed by `Fη` against the spectral data of `Ξ`:
`∫ η(z) Ξ(z) dz = (2π)⁻¹ ∫_{ζ≠0} Fη(ζ) Ξ̂(-ζ) dζ`, provided the right-hand side converges
absolutely.

The point masses at the origin of the distributional Fourier transform of `η` — its
polynomial part — are invisible on both sides: on the right because the integral omits the
origin, on the left because the vanishing moments of `Ξ` annihilate polynomials. This is the
function-level realization of the dual pairing of the Lizorkin quotient `𝒮'(ℝ)/𝒫`.

Proof: the defining pairing of `HasFourierAwayFromOrigin` is applied to the Schwartz test
functions `φ_{n,ℓ} = c_n ⋅ (κ_ℓ ⋆ χ)` where `χ(ζ) = Ξ̂(-ζ)`, `κ_ℓ` is a compactly supported
mollifier, and `c_n = b(ζ/n) - b(nζ)` a smooth cutoff vanishing near the origin and tapering
at `|ζ| ~ n`; the transform identity
`angularFourier1D φ_{n,ℓ} (z) = ∫ Ξ(r) κ̂_ℓ(r) ĉ_n(z-r) dr` holds by two absolutely
convergent Fubini computations. As `ℓ → ∞` the frequency side converges by dominated
convergence with majorant `|Fη ⋅ χ|` (compactly supported away from the origin), the time
side with majorant built from `κ̂_ℓ ≤ 1`. As `n → ∞`, `ĉ_n(s) = n b̂(ns) - n⁻¹ b̂(s/n)`
splits the time side into a taper term, which converges to `2π ∫ η Ξ` by the weighted
approximate identity (`MeasureTheory.tendsto_integral_weight_norm_smoothing_sub`, with
kernel `(2π)⁻¹ b̂` of unit integral), and a low-cut term, which vanishes by the
vanishing-moment cancellation
(`MeasureTheory.tendsto_integral_mul_smoothing_of_vanishing_moments`).

L1.ReconstructionSection, L1.Reconstruction: steps T1--T3 and T5--T6

Lemma2.2.7
Statement uses 3
Statement dependency previews
Preview
Definition 2.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

The reconstruction section and its spectral data (steps T1--T3). The truncated reconstruction is the pairing of the activation against the section \Xi_{x,\varepsilon,\delta}(r)=\int_{\varepsilon\le\|a\|\le\delta}\int f(y)\,\overline{\psi(r-\langle a,x-y\rangle)}\,dy\,da: \mathscr R^\dagger_\eta[\mathscr R_\psi f](x;\varepsilon,\delta)=\int\eta(r)\,\Xi_{x,\varepsilon,\delta}(r)\,dr, absolutely convergent under matched k-th moments (step T1; the proof substitutes b\leftarrow\langle a,x\rangle-r fibrewise and swaps the scale and pairing integrals through a triple-kernel layer built from the parametrized skew shears). The section is measurable, lies in the (1+|r|)^k-weighted L^1, and inherits the vanishing moments of \psi: \int r^j\,\Xi_{x,\varepsilon,\delta}(r)\,dr=0 for j\le k (step T3 — the integrated form of the shifted-conjugate moment lemma, placing \Xi in the domain of the pairing extension). Its Fourier data is computed by the spectral factor H_{x,\varepsilon,\delta}(\zeta)=\int_{\varepsilon\le\|a\|\le\delta}\widehat f(\zeta a)e^{i\zeta\langle a,x\rangle}da: \widehat\Xi(\zeta)=\overline{\widehat\psi(-\zeta)}\,H(-\zeta),\qquad \|H(\zeta)\|\le\min\bigl(\|f\|_1\,\mathrm{vol}(A_{\varepsilon,\delta}),\ |\zeta|^{-m}\|\widehat f\|_1\bigr), the two bounds — uniform near the origin, dilation-decaying at infinity — that make the admissibility pairing of step T5 absolutely convergent.

Lean code for Lemma2.2.7●9 declarations
  • defdefined in LeanRidgelet/L1/ReconstructionSection.lean
    complete
    def LeanRidgelet.truncatedReconstructionSection (m : ℕ) (ψ : ℝ → ℂ)
  (f : LeanRidgelet.InputSpace m → ℂ) (x : LeanRidgelet.InputSpace m)
  (ε δ : ℝ) : ℝ → ℂ
    def LeanRidgelet.truncatedReconstructionSection
  (m : ℕ) (ψ : ℝ → ℂ)
  (f : LeanRidgelet.InputSpace m → ℂ)
  (x : LeanRidgelet.InputSpace m)
  (ε δ : ℝ) : ℝ → ℂ
    Implementation after :=
    :=
  fun r => ∫ a in scaleAnnulus m ε δ, ∫ y, f y * conj (ψ (r - inner ℝ a (x - y)))
    The reconstruction section `Ξ_{x,ε,δ}(r)` (step T1 of the reconstruction plan): the
ridgelet-side data of the truncated reconstruction, paired against the activation in the
variable `r`.
  • theoremdefined in LeanRidgelet/L1/ReconstructionSection.lean
    complete
    theorem LeanRidgelet.truncatedDualRidgeletTransform_eq_section_pairing (m k : ℕ)
  {ψ η : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ} {Cη : ℝ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hψm : MeasureTheory.AEStronglyMeasurable ψ MeasureTheory.volume)
  (hηm : MeasureTheory.AEStronglyMeasurable η MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hηk : ∀ (z : ℝ), ‖η z‖ ≤ Cη * (1 + |z|) ^ k)
  (x : LeanRidgelet.InputSpace m) {ε δ : ℝ} (hε : 0 < ε) :
  LeanRidgelet.truncatedDualRidgeletTransform m 1 η
      (LeanRidgelet.euclideanRidgeletTransform m 1 ψ f) ε δ x =
    ∫ (r : ℝ),
      η r * LeanRidgelet.truncatedReconstructionSection m ψ f x ε δ r
    theorem LeanRidgelet.truncatedDualRidgeletTransform_eq_section_pairing
  (m k : ℕ) {ψ η : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  {Cη : ℝ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable
      (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hψm :
    MeasureTheory.AEStronglyMeasurable ψ
      MeasureTheory.volume)
  (hηm :
    MeasureTheory.AEStronglyMeasurable η
      MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable
      (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hηk :
    ∀ (z : ℝ), ‖η z‖ ≤ Cη * (1 + |z|) ^ k)
  (x : LeanRidgelet.InputSpace m)
  {ε δ : ℝ} (hε : 0 < ε) :
  LeanRidgelet.truncatedDualRidgeletTransform
      m 1 η
      (LeanRidgelet.euclideanRidgeletTransform
        m 1 ψ f)
      ε δ x =
    ∫ (r : ℝ),
      η r *
        LeanRidgelet.truncatedReconstructionSection
          m ψ f x ε δ r
    **Step T1 of the reconstruction plan**: the truncated reconstruction is the pairing of the
activation against the reconstruction section,
`R†_η[R_ψ f](x; ε, δ) = ∫ η(r) Ξ_{x,ε,δ}(r) dr`, absolutely convergent under matched `k`-th
moments. The proof substitutes `b ← ⟨a,x⟩ - r` fiberwise and swaps the scale and pairing
integrals through a triple-kernel integrability layer built from the parametrized skew shears
of `LeanRidgelet.ToMathlib.ProdShear`.
  • theoremdefined in LeanRidgelet/L1/ReconstructionSection.lean
    complete
    theorem LeanRidgelet.aestronglyMeasurable_truncatedReconstructionSection (m : ℕ)
  {ψ : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hψm : MeasureTheory.AEStronglyMeasurable ψ MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m) (ε δ : ℝ) :
  MeasureTheory.AEStronglyMeasurable
    (LeanRidgelet.truncatedReconstructionSection m ψ f x ε δ)
    MeasureTheory.volume
    theorem LeanRidgelet.aestronglyMeasurable_truncatedReconstructionSection
  (m : ℕ) {ψ : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hψm :
    MeasureTheory.AEStronglyMeasurable ψ
      MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m)
  (ε δ : ℝ) :
  MeasureTheory.AEStronglyMeasurable
    (LeanRidgelet.truncatedReconstructionSection
      m ψ f x ε δ)
    MeasureTheory.volume
    The reconstruction section is a.e. strongly measurable (step T2).
  • theoremdefined in LeanRidgelet/L1/ReconstructionSection.lean
    complete
    theorem LeanRidgelet.integrable_weight_truncatedReconstructionSection (m k : ℕ)
  {ψ : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hψm : MeasureTheory.AEStronglyMeasurable ψ MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m) (ε δ : ℝ) :
  MeasureTheory.Integrable
    (fun r ↦
      (1 + |r|) ^ k *
        ‖LeanRidgelet.truncatedReconstructionSection m ψ f x ε δ r‖)
    MeasureTheory.volume
    theorem LeanRidgelet.integrable_weight_truncatedReconstructionSection
  (m k : ℕ) {ψ : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable
      (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hψm :
    MeasureTheory.AEStronglyMeasurable ψ
      MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable
      (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m)
  (ε δ : ℝ) :
  MeasureTheory.Integrable
    (fun r ↦
      (1 + |r|) ^ k *
        ‖LeanRidgelet.truncatedReconstructionSection
            m ψ f x ε δ r‖)
    MeasureTheory.volume
    The reconstruction section lies in the polynomially weighted `L¹` (step T2).
  • theoremdefined in LeanRidgelet/L1/ReconstructionSection.lean
    complete
    theorem LeanRidgelet.integral_pow_mul_truncatedReconstructionSection_eq_zero
  (m k : ℕ) {ψ : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hψm : MeasureTheory.AEStronglyMeasurable ψ MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hψvm : ∀ j ≤ k, ∫ (s : ℝ), ↑s ^ j * ψ s = 0)
  (x : LeanRidgelet.InputSpace m) (ε δ : ℝ) {j : ℕ} (hj : j ≤ k) :
  ∫ (r : ℝ),
      ↑r ^ j *
        LeanRidgelet.truncatedReconstructionSection m ψ f x ε δ r =
    0
    theorem LeanRidgelet.integral_pow_mul_truncatedReconstructionSection_eq_zero
  (m k : ℕ) {ψ : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable
      (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hψm :
    MeasureTheory.AEStronglyMeasurable ψ
      MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable
      (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hψvm :
    ∀ j ≤ k, ∫ (s : ℝ), ↑s ^ j * ψ s = 0)
  (x : LeanRidgelet.InputSpace m)
  (ε δ : ℝ) {j : ℕ} (hj : j ≤ k) :
  ∫ (r : ℝ),
      ↑r ^ j *
        LeanRidgelet.truncatedReconstructionSection
          m ψ f x ε δ r =
    0
    **Step T3 of the reconstruction plan**: the reconstruction section inherits the vanishing
moments of the ridgelet function, `∫ r^j Ξ_{x,ε,δ}(r) dr = 0` for every `j ≤ k`. This is the
integrated form of `integral_pow_mul_conj_comp_sub_eq_zero`: after a Fubini swap through the
weighted master kernel, every fiber `∫ r^j conj (ψ (r - c)) dr` vanishes. Together with the
weighted-`L¹` membership this places `Ξ` in the domain of the pairing extension
`hasFourierAwayFromOrigin_pairing_extension`.
  • defdefined in LeanRidgelet/L1/ReconstructionSection.lean
    complete
    def LeanRidgelet.truncatedSpectralFactor (m : ℕ)
  (f : LeanRidgelet.InputSpace m → ℂ) (x : LeanRidgelet.InputSpace m)
  (ε δ : ℝ) : ℝ → ℂ
    def LeanRidgelet.truncatedSpectralFactor
  (m : ℕ)
  (f : LeanRidgelet.InputSpace m → ℂ)
  (x : LeanRidgelet.InputSpace m)
  (ε δ : ℝ) : ℝ → ℂ
    Implementation after :=
    :=
  fun ζ => ∫ a in scaleAnnulus m ε δ,
    Fourier.angularFourierIntegralInner f (ζ • a) *
      Complex.exp (Complex.I * ((ζ * inner ℝ a x : ℝ) : ℂ))
    The spectral factor `H_{x,ε,δ}(ζ) = ∫_{ε≤‖a‖≤δ} f̂(ζa) e^{iζ⟨a,x⟩} da` of the
truncated reconstruction (step T2).
  • theoremdefined in LeanRidgelet/L1/ReconstructionSection.lean
    complete
    theorem LeanRidgelet.angularFourier1D_truncatedReconstructionSection (m k : ℕ)
  {ψ : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hψm : MeasureTheory.AEStronglyMeasurable ψ MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m) (ε δ ζ : ℝ) :
  LeanRidgelet.angularFourier1D
      (LeanRidgelet.truncatedReconstructionSection m ψ f x ε δ) ζ =
    (starRingEnd ℂ) (LeanRidgelet.angularFourier1D ψ (-ζ)) *
      LeanRidgelet.truncatedSpectralFactor m f x ε δ (-ζ)
    theorem LeanRidgelet.angularFourier1D_truncatedReconstructionSection
  (m k : ℕ) {ψ : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable
      (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hψm :
    MeasureTheory.AEStronglyMeasurable ψ
      MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable
      (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m)
  (ε δ ζ : ℝ) :
  LeanRidgelet.angularFourier1D
      (LeanRidgelet.truncatedReconstructionSection
        m ψ f x ε δ)
      ζ =
    (starRingEnd ℂ)
        (LeanRidgelet.angularFourier1D ψ
          (-ζ)) *
      LeanRidgelet.truncatedSpectralFactor
        m f x ε δ (-ζ)
    Fourier representation of the reconstruction section (step T2):
`Ξ̂(ζ) = conj (ψ̂(-ζ)) ⋅ H(-ζ)`.
  • theoremdefined in LeanRidgelet/L1/ReconstructionSection.lean
    complete
    theorem LeanRidgelet.norm_truncatedSpectralFactor_le (m : ℕ)
  (f : LeanRidgelet.InputSpace m → ℂ) (x : LeanRidgelet.InputSpace m)
  (ε δ ζ : ℝ) :
  ‖LeanRidgelet.truncatedSpectralFactor m f x ε δ ζ‖ ≤
    (∫ (y : LeanRidgelet.InputSpace m), ‖f y‖) *
      (MeasureTheory.volume (LeanRidgelet.scaleAnnulus m ε δ)).toReal
    theorem LeanRidgelet.norm_truncatedSpectralFactor_le
  (m : ℕ)
  (f : LeanRidgelet.InputSpace m → ℂ)
  (x : LeanRidgelet.InputSpace m)
  (ε δ ζ : ℝ) :
  ‖LeanRidgelet.truncatedSpectralFactor m
        f x ε δ ζ‖ ≤
    (∫ (y : LeanRidgelet.InputSpace m),
        ‖f y‖) *
      (MeasureTheory.volume
          (LeanRidgelet.scaleAnnulus m ε
            δ)).toReal
    Uniform bound of the spectral factor by the signal mass (step T2).
  • theoremdefined in LeanRidgelet/L1/ReconstructionSection.lean
    complete
    theorem LeanRidgelet.norm_truncatedSpectralFactor_le_of_ne (m : ℕ)
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hfhat :
    MeasureTheory.Integrable
      (LeanRidgelet.Fourier.angularFourierIntegralInner f)
      MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m) (ε δ : ℝ) {ζ : ℝ} (hζ : ζ ≠ 0) :
  ‖LeanRidgelet.truncatedSpectralFactor m f x ε δ ζ‖ ≤
    |ζ|⁻¹ ^ m *
      ∫ (ξ : LeanRidgelet.InputSpace m),
        ‖LeanRidgelet.Fourier.angularFourierIntegralInner f ξ‖
    theorem LeanRidgelet.norm_truncatedSpectralFactor_le_of_ne
  (m : ℕ)
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hfhat :
    MeasureTheory.Integrable
      (LeanRidgelet.Fourier.angularFourierIntegralInner
        f)
      MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m)
  (ε δ : ℝ) {ζ : ℝ} (hζ : ζ ≠ 0) :
  ‖LeanRidgelet.truncatedSpectralFactor m
        f x ε δ ζ‖ ≤
    |ζ|⁻¹ ^ m *
      ∫ (ξ : LeanRidgelet.InputSpace m),
        ‖LeanRidgelet.Fourier.angularFourierIntegralInner
            f ξ‖
    Dilation bound of the spectral factor by the spectral mass (step T2):
`‖H(ζ)‖ ≤ |ζ|⁻ᵐ ‖f̂‖₁` for `ζ ≠ 0`.
Lemma2.2.8
Statement uses 2
Statement dependency previews
Preview
Lemma 2.2.6
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

The spectral pairing of the truncated reconstruction (step T5). The spectral window G_{x,\varepsilon,\delta}(\zeta)=\int_{|\zeta|\varepsilon\le\|\xi\|\le|\zeta|\delta}\widehat f(\xi)e^{i\langle\xi,x\rangle}d\xi is the |\zeta|^m-rescaled spectral factor, G(\zeta)=|\zeta|^mH(\zeta), by the dilation \xi=\zeta a. The dilation bound \|H(\zeta)\|\le|\zeta|^{-m}\|\widehat f\|_1 dominates the pairing integrand of the extension theorem by the admissibility density u(\zeta)=\overline{\widehat\psi(\zeta)}F_\eta(\zeta)/|\zeta|^m, giving the absolute convergence \|F_\eta(\zeta)\widehat\Xi(-\zeta)\|\le\|u(\zeta)\|\,\|\widehat f\|_1 demanded by the pairing extension — the point where the integrability half of admissibility enters. Combining T1--T5: \mathscr R^\dagger_\eta[\mathscr R_\psi f](x;\varepsilon,\delta)=\frac1{2\pi}\int_{\zeta\ne0}u(\zeta)\,G_{x,\varepsilon,\delta}(\zeta)\,d\zeta.

Lean code for Lemma2.2.8●6 declarations
  • defdefined in LeanRidgelet/L1/Reconstruction.lean
    complete
    def LeanRidgelet.truncatedSpectralWindow (m : ℕ)
  (f : LeanRidgelet.InputSpace m → ℂ) (x : LeanRidgelet.InputSpace m)
  (ε δ ζ : ℝ) : ℂ
    def LeanRidgelet.truncatedSpectralWindow
  (m : ℕ)
  (f : LeanRidgelet.InputSpace m → ℂ)
  (x : LeanRidgelet.InputSpace m)
  (ε δ ζ : ℝ) : ℂ
    Implementation after :=
    :=
  ∫ ξ in scaleAnnulus m (|ζ| * ε) (|ζ| * δ),
    Fourier.angularFourierIntegralInner f ξ *
      Complex.exp (Complex.I * ((inner ℝ ξ x : ℝ) : ℂ))
    The spectral window `G_{x,ε,δ}(ζ) = ∫_{|ζ|ε ≤ ‖ξ‖ ≤ |ζ|δ} f̂(ξ) e^{i⟨ξ,x⟩} dξ`
(step T5): the inverse Fourier integral of the signal truncated to the dilated annulus.
  • theoremdefined in LeanRidgelet/L1/Reconstruction.lean
    complete
    theorem LeanRidgelet.truncatedSpectralWindow_eq (m : ℕ)
  (f : LeanRidgelet.InputSpace m → ℂ) (x : LeanRidgelet.InputSpace m)
  (ε δ : ℝ) {ζ : ℝ} (hζ : ζ ≠ 0) :
  LeanRidgelet.truncatedSpectralWindow m f x ε δ ζ =
    ↑(|ζ| ^ m) * LeanRidgelet.truncatedSpectralFactor m f x ε δ ζ
    theorem LeanRidgelet.truncatedSpectralWindow_eq
  (m : ℕ)
  (f : LeanRidgelet.InputSpace m → ℂ)
  (x : LeanRidgelet.InputSpace m)
  (ε δ : ℝ) {ζ : ℝ} (hζ : ζ ≠ 0) :
  LeanRidgelet.truncatedSpectralWindow m f
      x ε δ ζ =
    ↑(|ζ| ^ m) *
      LeanRidgelet.truncatedSpectralFactor
        m f x ε δ ζ
    Dilation identity (step T5): the spectral window is the `|ζ|^m`-rescaled spectral factor,
`G_{x,ε,δ}(ζ) = |ζ|^m ⋅ H_{x,ε,δ}(ζ)`, by the change of variables `ξ = ζ • a`.
  • theoremdefined in LeanRidgelet/L1/Reconstruction.lean
    complete
    theorem LeanRidgelet.integrable_truncatedReconstructionSection (m k : ℕ)
  {ψ : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hψm : MeasureTheory.AEStronglyMeasurable ψ MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m) (ε δ : ℝ) :
  MeasureTheory.Integrable
    (LeanRidgelet.truncatedReconstructionSection m ψ f x ε δ)
    MeasureTheory.volume
    theorem LeanRidgelet.integrable_truncatedReconstructionSection
  (m k : ℕ) {ψ : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable
      (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hψm :
    MeasureTheory.AEStronglyMeasurable ψ
      MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable
      (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m)
  (ε δ : ℝ) :
  MeasureTheory.Integrable
    (LeanRidgelet.truncatedReconstructionSection
      m ψ f x ε δ)
    MeasureTheory.volume
    The reconstruction section is integrable (step T2).
  • theoremdefined in LeanRidgelet/L1/Reconstruction.lean
    complete
    theorem LeanRidgelet.integrableOn_fourierData_truncatedReconstructionSection
  (m k : ℕ) {ψ Fη : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hψm : MeasureTheory.AEStronglyMeasurable ψ MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hfhat :
    MeasureTheory.Integrable
      (LeanRidgelet.Fourier.angularFourierIntegralInner f)
      MeasureTheory.volume)
  (hFηm :
    MeasureTheory.AEStronglyMeasurable Fη
      (MeasureTheory.volume.restrict {0}ᶜ))
  (hKint :
    MeasureTheory.IntegrableOn
      (fun ζ ↦
        (starRingEnd ℂ) (LeanRidgelet.angularFourier1D ψ ζ) * Fη ζ /
          ↑(|ζ| ^ m))
      {0}ᶜ MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m) (ε δ : ℝ) :
  MeasureTheory.IntegrableOn
    (fun ζ ↦
      Fη ζ *
        LeanRidgelet.angularFourier1D
          (LeanRidgelet.truncatedReconstructionSection m ψ f x ε δ)
          (-ζ))
    {0}ᶜ MeasureTheory.volume
    theorem LeanRidgelet.integrableOn_fourierData_truncatedReconstructionSection
  (m k : ℕ) {ψ Fη : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable
      (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hψm :
    MeasureTheory.AEStronglyMeasurable ψ
      MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable
      (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hfhat :
    MeasureTheory.Integrable
      (LeanRidgelet.Fourier.angularFourierIntegralInner
        f)
      MeasureTheory.volume)
  (hFηm :
    MeasureTheory.AEStronglyMeasurable Fη
      (MeasureTheory.volume.restrict
        {0}ᶜ))
  (hKint :
    MeasureTheory.IntegrableOn
      (fun ζ ↦
        (starRingEnd ℂ)
              (LeanRidgelet.angularFourier1D
                ψ ζ) *
            Fη ζ /
          ↑(|ζ| ^ m))
      {0}ᶜ MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m)
  (ε δ : ℝ) :
  MeasureTheory.IntegrableOn
    (fun ζ ↦
      Fη ζ *
        LeanRidgelet.angularFourier1D
          (LeanRidgelet.truncatedReconstructionSection
            m ψ f x ε δ)
          (-ζ))
    {0}ᶜ MeasureTheory.volume
    Absolute convergence of the spectral pairing (step T5): the admissibility density
`u(ζ) = conj(ψ̂ ζ) Fη ζ / |ζ|^m` and the dilation bound on the spectral factor dominate the
pairing integrand of the extension theorem, `‖Fη(ζ) Ξ̂(-ζ)‖ ≤ ‖u(ζ)‖ ⋅ ‖f̂‖₁`.
  • theoremdefined in LeanRidgelet/L1/Reconstruction.lean
    complete
    theorem LeanRidgelet.setIntegral_fourierData_truncatedReconstructionSection
  (m k : ℕ) {ψ Fη : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hψm : MeasureTheory.AEStronglyMeasurable ψ MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m) (ε δ : ℝ) :
  ∫ (ζ : ℝ) in {0}ᶜ,
      Fη ζ *
        LeanRidgelet.angularFourier1D
          (LeanRidgelet.truncatedReconstructionSection m ψ f x ε δ)
          (-ζ) =
    ∫ (ζ : ℝ) in {0}ᶜ,
      (starRingEnd ℂ) (LeanRidgelet.angularFourier1D ψ ζ) * Fη ζ /
          ↑(|ζ| ^ m) *
        LeanRidgelet.truncatedSpectralWindow m f x ε δ ζ
    theorem LeanRidgelet.setIntegral_fourierData_truncatedReconstructionSection
  (m k : ℕ) {ψ Fη : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable
      (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hψm :
    MeasureTheory.AEStronglyMeasurable ψ
      MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable
      (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m)
  (ε δ : ℝ) :
  ∫ (ζ : ℝ) in {0}ᶜ,
      Fη ζ *
        LeanRidgelet.angularFourier1D
          (LeanRidgelet.truncatedReconstructionSection
            m ψ f x ε δ)
          (-ζ) =
    ∫ (ζ : ℝ) in {0}ᶜ,
      (starRingEnd ℂ)
              (LeanRidgelet.angularFourier1D
                ψ ζ) *
            Fη ζ /
          ↑(|ζ| ^ m) *
        LeanRidgelet.truncatedSpectralWindow
          m f x ε δ ζ
    The spectral pairing identity (step T5): against the Fourier data of the activation, the
reconstruction section pairs into the admissibility density and the spectral window,
`∫_{ζ≠0} Fη(ζ) Ξ̂(-ζ) dζ = ∫_{ζ≠0} u(ζ) G_{x,ε,δ}(ζ) dζ`.
  • theoremdefined in LeanRidgelet/L1/Reconstruction.lean
    complete
    theorem LeanRidgelet.truncatedDualRidgeletTransform_eq_spectral_pairing
  (m k : ℕ) {ψ η Fη : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  {Cη : ℝ} (hη : LeanRidgelet.HasFourierAwayFromOrigin η Fη)
  (hηk : ∀ (z : ℝ), ‖η z‖ ≤ Cη * (1 + |z|) ^ k)
  (hψm : MeasureTheory.AEStronglyMeasurable ψ MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hψvm : ∀ j ≤ k, ∫ (s : ℝ), ↑s ^ j * ψ s = 0)
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hfhat :
    MeasureTheory.Integrable
      (LeanRidgelet.Fourier.angularFourierIntegralInner f)
      MeasureTheory.volume)
  (hKint :
    MeasureTheory.IntegrableOn
      (fun ζ ↦
        (starRingEnd ℂ) (LeanRidgelet.angularFourier1D ψ ζ) * Fη ζ /
          ↑(|ζ| ^ m))
      {0}ᶜ MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m) {ε δ : ℝ} (hε : 0 < ε) :
  LeanRidgelet.truncatedDualRidgeletTransform m 1 η
      (LeanRidgelet.euclideanRidgeletTransform m 1 ψ f) ε δ x =
    ↑(2 * Real.pi)⁻¹ *
      ∫ (ζ : ℝ) in {0}ᶜ,
        (starRingEnd ℂ) (LeanRidgelet.angularFourier1D ψ ζ) * Fη ζ /
            ↑(|ζ| ^ m) *
          LeanRidgelet.truncatedSpectralWindow m f x ε δ ζ
    theorem LeanRidgelet.truncatedDualRidgeletTransform_eq_spectral_pairing
  (m k : ℕ) {ψ η Fη : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  {Cη : ℝ}
  (hη :
    LeanRidgelet.HasFourierAwayFromOrigin
      η Fη)
  (hηk :
    ∀ (z : ℝ), ‖η z‖ ≤ Cη * (1 + |z|) ^ k)
  (hψm :
    MeasureTheory.AEStronglyMeasurable ψ
      MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable
      (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hψvm :
    ∀ j ≤ k, ∫ (s : ℝ), ↑s ^ j * ψ s = 0)
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable
      (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hfhat :
    MeasureTheory.Integrable
      (LeanRidgelet.Fourier.angularFourierIntegralInner
        f)
      MeasureTheory.volume)
  (hKint :
    MeasureTheory.IntegrableOn
      (fun ζ ↦
        (starRingEnd ℂ)
              (LeanRidgelet.angularFourier1D
                ψ ζ) *
            Fη ζ /
          ↑(|ζ| ^ m))
      {0}ᶜ MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m)
  {ε δ : ℝ} (hε : 0 < ε) :
  LeanRidgelet.truncatedDualRidgeletTransform
      m 1 η
      (LeanRidgelet.euclideanRidgeletTransform
        m 1 ψ f)
      ε δ x =
    ↑(2 * Real.pi)⁻¹ *
      ∫ (ζ : ℝ) in {0}ᶜ,
        (starRingEnd ℂ)
                (LeanRidgelet.angularFourier1D
                  ψ ζ) *
              Fη ζ /
            ↑(|ζ| ^ m) *
          LeanRidgelet.truncatedSpectralWindow
            m f x ε δ ζ
    **Steps T1–T5 combined**: under matched growth and moments and an absolutely convergent
admissibility density, the truncated reconstruction is the spectral pairing
`R†_η[R_ψ f](x; ε, δ) = (2π)⁻¹ ∫_{ζ≠0} u(ζ) G_{x,ε,δ}(ζ) dζ` of the admissibility density
`u(ζ) = conj(ψ̂ ζ) Fη ζ / |ζ|^m` against the spectral window.
Lemma2.2.9
Statement uses 3
Statement dependency previews
Preview
Theorem 1.2.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

The truncation limit (step T6). At every nonzero frequency the spectral window converges to the full inverse spectral integral along the truncation filter \varepsilon\to0^+, \delta\to\infty (dominated convergence over the dilated annuli, majorant \|\widehat f\|_1; the origin is null for m\ge1). A second dominated convergence with majorant \|u\|\,\|\widehat f\|_1 — uniform in the truncation — passes the limit through the spectral pairing: \mathscr R^\dagger_\eta[\mathscr R_\psi f](x;\varepsilon,\delta)\longrightarrow K_{\psi,\eta}\,(2\pi)^{-m}\int\widehat f(\xi)e^{i\langle\xi,x\rangle}d\xi, and the inverse spectral integral equals (2\pi)^mf(x) almost everywhere (by almost-everywhere Fourier inversion) and at continuity points (by Mathlib's inversion theorem), through the angular bridge of the foundations chapter. This proves l1_reconstruction.

Lean code for Lemma2.2.9●10 theorems
  • theoremdefined in LeanRidgelet/L1/Reconstruction.lean
    complete
    theorem LeanRidgelet.norm_truncatedSpectralWindow_le (m : ℕ)
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hfhat :
    MeasureTheory.Integrable
      (LeanRidgelet.Fourier.angularFourierIntegralInner f)
      MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m) (ε δ ζ : ℝ) :
  ‖LeanRidgelet.truncatedSpectralWindow m f x ε δ ζ‖ ≤
    ∫ (ξ : LeanRidgelet.InputSpace m),
      ‖LeanRidgelet.Fourier.angularFourierIntegralInner f ξ‖
    theorem LeanRidgelet.norm_truncatedSpectralWindow_le
  (m : ℕ)
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hfhat :
    MeasureTheory.Integrable
      (LeanRidgelet.Fourier.angularFourierIntegralInner
        f)
      MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m)
  (ε δ ζ : ℝ) :
  ‖LeanRidgelet.truncatedSpectralWindow m
        f x ε δ ζ‖ ≤
    ∫ (ξ : LeanRidgelet.InputSpace m),
      ‖LeanRidgelet.Fourier.angularFourierIntegralInner
          f ξ‖
    Uniform bound of the spectral window by the spectral mass (step T6):
`‖G_{x,ε,δ}(ζ)‖ ≤ ‖f̂‖₁` for all scales and truncations.
  • theoremdefined in LeanRidgelet/L1/Reconstruction.lean
    complete
    theorem LeanRidgelet.continuous_truncatedSpectralFactor (m : ℕ)
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m) (ε δ : ℝ) :
  Continuous (LeanRidgelet.truncatedSpectralFactor m f x ε δ)
    theorem LeanRidgelet.continuous_truncatedSpectralFactor
  (m : ℕ)
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m)
  (ε δ : ℝ) :
  Continuous
    (LeanRidgelet.truncatedSpectralFactor
      m f x ε δ)
    The spectral factor is continuous in the frequency (step T6).
  • theoremdefined in LeanRidgelet/L1/Reconstruction.lean
    complete
    theorem LeanRidgelet.tendsto_truncatedSpectralWindow (m : ℕ) [NeZero m]
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hfhat :
    MeasureTheory.Integrable
      (LeanRidgelet.Fourier.angularFourierIntegralInner f)
      MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m) {ζ : ℝ} (hζ : ζ ≠ 0) :
  Filter.Tendsto
    (fun q ↦ LeanRidgelet.truncatedSpectralWindow m f x q.1 q.2 ζ)
    LeanRidgelet.ridgeletTruncationFilter
    (nhds
      (∫ (ξ : LeanRidgelet.InputSpace m),
        LeanRidgelet.Fourier.angularFourierIntegralInner f ξ *
          Complex.exp (Complex.I * ↑(inner ℝ ξ x))))
    theorem LeanRidgelet.tendsto_truncatedSpectralWindow
  (m : ℕ) [NeZero m]
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hfhat :
    MeasureTheory.Integrable
      (LeanRidgelet.Fourier.angularFourierIntegralInner
        f)
      MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m) {ζ : ℝ}
  (hζ : ζ ≠ 0) :
  Filter.Tendsto
    (fun q ↦
      LeanRidgelet.truncatedSpectralWindow
        m f x q.1 q.2 ζ)
    LeanRidgelet.ridgeletTruncationFilter
    (nhds
      (∫ (ξ : LeanRidgelet.InputSpace m),
        LeanRidgelet.Fourier.angularFourierIntegralInner
            f ξ *
          Complex.exp
            (Complex.I * ↑(inner ℝ ξ x))))
    Pointwise truncation limit of the spectral window (step T6): at every nonzero frequency
the window converges to the full inverse spectral integral along the truncation filter.
  • theoremdefined in LeanRidgelet/L1/Reconstruction.lean
    complete
    theorem LeanRidgelet.tendsto_truncatedDualRidgeletTransform (m k : ℕ) [NeZero m]
  {ψ η Fη : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ} {Cη : ℝ}
  (hη : LeanRidgelet.HasFourierAwayFromOrigin η Fη)
  (hηk : ∀ (z : ℝ), ‖η z‖ ≤ Cη * (1 + |z|) ^ k)
  (hψm : MeasureTheory.AEStronglyMeasurable ψ MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hψvm : ∀ j ≤ k, ∫ (s : ℝ), ↑s ^ j * ψ s = 0)
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hfhat :
    MeasureTheory.Integrable
      (LeanRidgelet.Fourier.angularFourierIntegralInner f)
      MeasureTheory.volume)
  (hKint :
    MeasureTheory.IntegrableOn
      (fun ζ ↦
        (starRingEnd ℂ) (LeanRidgelet.angularFourier1D ψ ζ) * Fη ζ /
          ↑(|ζ| ^ m))
      {0}ᶜ MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m) :
  Filter.Tendsto
    (fun q ↦
      LeanRidgelet.truncatedDualRidgeletTransform m 1 η
        (LeanRidgelet.euclideanRidgeletTransform m 1 ψ f) q.1 q.2 x)
    LeanRidgelet.ridgeletTruncationFilter
    (nhds
      (LeanRidgelet.admissibilityConstant m ψ Fη *
          (↑((2 * Real.pi) ^ m))⁻¹ *
        ∫ (ξ : LeanRidgelet.InputSpace m),
          LeanRidgelet.Fourier.angularFourierIntegralInner f ξ *
            Complex.exp (Complex.I * ↑(inner ℝ ξ x))))
    theorem LeanRidgelet.tendsto_truncatedDualRidgeletTransform
  (m k : ℕ) [NeZero m] {ψ η Fη : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  {Cη : ℝ}
  (hη :
    LeanRidgelet.HasFourierAwayFromOrigin
      η Fη)
  (hηk :
    ∀ (z : ℝ), ‖η z‖ ≤ Cη * (1 + |z|) ^ k)
  (hψm :
    MeasureTheory.AEStronglyMeasurable ψ
      MeasureTheory.volume)
  (hψk :
    MeasureTheory.Integrable
      (fun s ↦ (1 + |s|) ^ k * ‖ψ s‖)
      MeasureTheory.volume)
  (hψvm :
    ∀ j ≤ k, ∫ (s : ℝ), ↑s ^ j * ψ s = 0)
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hfk :
    MeasureTheory.Integrable
      (fun y ↦ (1 + ‖y‖) ^ k * ‖f y‖)
      MeasureTheory.volume)
  (hfhat :
    MeasureTheory.Integrable
      (LeanRidgelet.Fourier.angularFourierIntegralInner
        f)
      MeasureTheory.volume)
  (hKint :
    MeasureTheory.IntegrableOn
      (fun ζ ↦
        (starRingEnd ℂ)
              (LeanRidgelet.angularFourier1D
                ψ ζ) *
            Fη ζ /
          ↑(|ζ| ^ m))
      {0}ᶜ MeasureTheory.volume)
  (x : LeanRidgelet.InputSpace m) :
  Filter.Tendsto
    (fun q ↦
      LeanRidgelet.truncatedDualRidgeletTransform
        m 1 η
        (LeanRidgelet.euclideanRidgeletTransform
          m 1 ψ f)
        q.1 q.2 x)
    LeanRidgelet.ridgeletTruncationFilter
    (nhds
      (LeanRidgelet.admissibilityConstant
            m ψ Fη *
          (↑((2 * Real.pi) ^ m))⁻¹ *
        ∫ (ξ : LeanRidgelet.InputSpace m),
          LeanRidgelet.Fourier.angularFourierIntegralInner
              f ξ *
            Complex.exp
              (Complex.I *
                ↑(inner ℝ ξ x))))
    **Step T6, truncation limit**: the truncated reconstruction converges along the
truncation filter to the admissibility constant times the normalized inverse spectral
integral.
  • theoremdefined in LeanRidgelet/L1/TruncatedLimit.lean
    complete
    theorem LeanRidgelet.measurableSet_truncationAnnulus (m : ℕ) (ε δ : ℝ) :
  MeasurableSet {p | ε ≤ ‖p.1‖ ∧ ‖p.1‖ ≤ δ}
    theorem LeanRidgelet.measurableSet_truncationAnnulus
  (m : ℕ) (ε δ : ℝ) :
  MeasurableSet
    {p | ε ≤ ‖p.1‖ ∧ ‖p.1‖ ≤ δ}
    The scale annulus `ε ≤ ‖a‖ ≤ δ` of the parameter space `𝕐^{m+1}` is measurable: it is the
preimage of `Set.Icc ε δ` under the continuous map `p ↦ ‖p.1‖`.
  • theoremdefined in LeanRidgelet/L1/TruncatedLimit.lean
    complete
    theorem LeanRidgelet.ae_parameter_fst_ne_zero (m : ℕ) [NeZero m] :
  ∀ᵐ (p : LeanRidgelet.RidgeletParameterSpace m), p.1 ≠ 0
    theorem LeanRidgelet.ae_parameter_fst_ne_zero
  (m : ℕ) [NeZero m] :
  ∀ᵐ (p :
    LeanRidgelet.RidgeletParameterSpace
      m),
    p.1 ≠ 0
    Almost every parameter has a nonzero weight component: the slice `a = 0` of the parameter
space is a null set as soon as the input space is nontrivial. This is what makes the scale
annulus exhaust `𝕐^{m+1}` up to a null set.
  • theoremdefined in LeanRidgelet/L1/TruncatedLimit.lean
    complete
    theorem LeanRidgelet.truncatedDualRidgeletTransform_eq_integral_indicator
  (m : ℕ) (s : ℝ) (η : ℝ → ℂ)
  (T : LeanRidgelet.RidgeletParameterSpace m → ℂ) (ε δ : ℝ)
  (x : LeanRidgelet.InputSpace m) :
  LeanRidgelet.truncatedDualRidgeletTransform m s η T ε δ x =
    ∫ (p : LeanRidgelet.RidgeletParameterSpace m),
      {p | ε ≤ ‖p.1‖ ∧ ‖p.1‖ ≤ δ}.indicator
        (fun p ↦ T p * η (inner ℝ p.1 x - p.2) * (↑(‖p.1‖ ^ s))⁻¹) p
    theorem LeanRidgelet.truncatedDualRidgeletTransform_eq_integral_indicator
  (m : ℕ) (s : ℝ) (η : ℝ → ℂ)
  (T :
    LeanRidgelet.RidgeletParameterSpace
        m →
      ℂ)
  (ε δ : ℝ)
  (x : LeanRidgelet.InputSpace m) :
  LeanRidgelet.truncatedDualRidgeletTransform
      m s η T ε δ x =
    ∫ (p :
      LeanRidgelet.RidgeletParameterSpace
        m),
      {p |
            ε ≤ ‖p.1‖ ∧
              ‖p.1‖ ≤ δ}.indicator
        (fun p ↦
          T p * η (inner ℝ p.1 x - p.2) *
            (↑(‖p.1‖ ^ s))⁻¹)
        p
    The truncated dual ridgelet transform is the integral over the whole parameter space of the
dual ridgelet integrand against the indicator of the scale annulus.
  • theoremdefined in LeanRidgelet/L1/TruncatedLimit.lean
    complete
    theorem LeanRidgelet.tendsto_truncatedDualRidgeletTransform_of_integrable
  (m : ℕ) [NeZero m] (s : ℝ) (η : ℝ → ℂ)
  (T : LeanRidgelet.RidgeletParameterSpace m → ℂ)
  (x : LeanRidgelet.InputSpace m)
  (hint :
    MeasureTheory.Integrable
      (fun p ↦ T p * η (inner ℝ p.1 x - p.2) * (↑(‖p.1‖ ^ s))⁻¹)
      MeasureTheory.volume) :
  Filter.Tendsto
    (fun q ↦
      LeanRidgelet.truncatedDualRidgeletTransform m s η T q.1 q.2 x)
    LeanRidgelet.ridgeletTruncationFilter
    (nhds (LeanRidgelet.euclideanDualRidgeletTransform m s η T x))
    theorem LeanRidgelet.tendsto_truncatedDualRidgeletTransform_of_integrable
  (m : ℕ) [NeZero m] (s : ℝ) (η : ℝ → ℂ)
  (T :
    LeanRidgelet.RidgeletParameterSpace
        m →
      ℂ)
  (x : LeanRidgelet.InputSpace m)
  (hint :
    MeasureTheory.Integrable
      (fun p ↦
        T p * η (inner ℝ p.1 x - p.2) *
          (↑(‖p.1‖ ^ s))⁻¹)
      MeasureTheory.volume) :
  Filter.Tendsto
    (fun q ↦
      LeanRidgelet.truncatedDualRidgeletTransform
        m s η T q.1 q.2 x)
    LeanRidgelet.ridgeletTruncationFilter
    (nhds
      (LeanRidgelet.euclideanDualRidgeletTransform
        m s η T x))
    **The truncation limit of the dual ridgelet transform.** If the full dual ridgelet integrand
`p ↦ T p * η (⟪a, x⟫ - b) * ‖a‖^{-s}` is `volume`-integrable on the parameter space, then the
truncated dual ridgelet transform converges to the untruncated one along the truncation filter
`ridgeletTruncationFilter = (𝓝[>] 0) ×ˢ atTop`, i.e. as `ε → 0⁺` and `δ → ∞` jointly.

Read the honesty warning in the module docstring before using this: the integrability hypothesis
is not available for the admissible pairs constructed in `LeanRidgelet.L1.BumpRidgelet`, so this
does not upgrade the `L¹` reconstruction endpoints to untruncated statements.
  • theoremdefined in LeanRidgelet/L1/Reconstruction.lean
    complete
    theorem LeanRidgelet.ae_integral_angularFourier_mul_exp (m : ℕ)
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hfhat :
    MeasureTheory.Integrable
      (LeanRidgelet.Fourier.angularFourierIntegralInner f)
      MeasureTheory.volume) :
  ∀ᵐ (x : LeanRidgelet.InputSpace m),
    ∫ (ξ : LeanRidgelet.InputSpace m),
        LeanRidgelet.Fourier.angularFourierIntegralInner f ξ *
          Complex.exp (Complex.I * ↑(inner ℝ ξ x)) =
      ↑((2 * Real.pi) ^ m) * f x
    theorem LeanRidgelet.ae_integral_angularFourier_mul_exp
  (m : ℕ)
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hfhat :
    MeasureTheory.Integrable
      (LeanRidgelet.Fourier.angularFourierIntegralInner
        f)
      MeasureTheory.volume) :
  ∀ᵐ (x : LeanRidgelet.InputSpace m),
    ∫ (ξ : LeanRidgelet.InputSpace m),
        LeanRidgelet.Fourier.angularFourierIntegralInner
            f ξ *
          Complex.exp
            (Complex.I * ↑(inner ℝ ξ x)) =
      ↑((2 * Real.pi) ^ m) * f x
    The truncation limit is the inverse Fourier integral, almost everywhere: for `f ∈ L¹`
with `f̂ ∈ L¹`, `∫ f̂(ξ) e^{i⟨ξ,x⟩} dξ = (2π)^m f(x)` at almost every `x`.
  • theoremdefined in LeanRidgelet/L1/Reconstruction.lean
    complete
    theorem LeanRidgelet.integral_angularFourier_mul_exp_of_continuousAt (m : ℕ)
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hfhat :
    MeasureTheory.Integrable
      (LeanRidgelet.Fourier.angularFourierIntegralInner f)
      MeasureTheory.volume)
  {x : LeanRidgelet.InputSpace m} (hx : ContinuousAt f x) :
  ∫ (ξ : LeanRidgelet.InputSpace m),
      LeanRidgelet.Fourier.angularFourierIntegralInner f ξ *
        Complex.exp (Complex.I * ↑(inner ℝ ξ x)) =
    ↑((2 * Real.pi) ^ m) * f x
    theorem LeanRidgelet.integral_angularFourier_mul_exp_of_continuousAt
  (m : ℕ)
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hfhat :
    MeasureTheory.Integrable
      (LeanRidgelet.Fourier.angularFourierIntegralInner
        f)
      MeasureTheory.volume)
  {x : LeanRidgelet.InputSpace m}
  (hx : ContinuousAt f x) :
  ∫ (ξ : LeanRidgelet.InputSpace m),
      LeanRidgelet.Fourier.angularFourierIntegralInner
          f ξ *
        Complex.exp
          (Complex.I * ↑(inner ℝ ξ x)) =
    ↑((2 * Real.pi) ^ m) * f x
    The truncation limit is the inverse Fourier integral at continuity points.

A second truncation limit is available for the dual transform alone, without the spectral route: if the full dual integrand is integrable for the parameter Lebesgue measure, the truncated dual transform converges to the untruncated one along the same filter, by dominated convergence with the integrand itself as majorant. The filter is a genuine product, so it is countably generated and the dominated-convergence theorem applies to it directly; the input dimension must be nonzero, since otherwise every annulus is empty and the truncated transform vanishes while the untruncated one does not. This lemma does not discharge the reconstruction hypothesis of the endpoints above: for the admissible pairs the construction chapter produces, the ridgelet transform is only square-integrable against the weighted parameter measure, which does not give the integrability this lemma needs.

L1.LambdaOperator: the multiplier property

Theorem2.2.10
Statement uses 4
Statement dependency previews
Preview
Definition 2.1.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Theorem 2.1.15
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The Lambda operator as a Fourier multiplier (plan item A-3). On Schwartz functions the standard Lambda-operator power \Lambda^m acts as the Fourier multiplier |2\pi\xi|^m, i.e. the article's |\omega|^m in the angular convention \omega=2\pi\xi: \Lambda^m\varphi(z)=\int|2\pi\xi|^m\,\mathcal F\varphi(\xi)\,e^{2\pi iz\xi}\,d\xi. The even case is Fourier inversion together with the derivative rule \mathcal F[\partial^m\varphi]=(2\pi i\xi)^m\mathcal F\varphi and the identity (-1)^{m/2}(2\pi i\xi)^m=|2\pi\xi|^m; the odd case additionally uses the Fourier symbol -i\,\mathrm{sign}\,\xi of the principal-value Hilbert transform (upstream-candidate mathlib_hilbert_symbol) and the identity (-1)^{\lfloor m/2\rfloor}(-i\,\mathrm{sign}\,\xi)(2\pi i\xi)^m=|2\pi\xi|^m. The angular form (fifth declaration) exhibits \Lambda^m\varphi as the inverse angular Fourier transform of the integrable multiplier |\zeta|^m\widehat\varphi, and a general lemma — the inverse angular Fourier transform of an integrable function carries that function as its Fourier data away from the origin (sixth declaration) — yields the Fourier data of \Lambda^m\varphi (seventh), which is what the spectral form of thm:eq.ac needs. The sixth declaration is also the function-level substitute for the duality \mathcal O_M\cong\mathcal O_C' in the necessity half of l1_structure_theorem, its witness being bounded and continuous rather than slowly increasing and smooth. Integrability of the filtered function. For even m it is Schwartz (eighth declaration); for odd m it is \pm\mathscr H\varphi^{(m)}, whose integral vanishes because it is a derivative (ninth declaration), so the L^1 estimate of mathlib_hilbert_symbol applies and \Lambda^m\varphi\in L^1 for every m\ge1 (tenth declaration). Angular Fourier inversion then upgrades the Fourier data to the honest Fourier integral at every frequency (eleventh declaration), which is what l1_construction_admissible needs. This chain is also the analytic prerequisite of Radon's inversion formula for even m.

Lean code for Theorem2.2.10●11 declarations
  • theoremdefined in LeanRidgelet/L1/LambdaOperator.lean
    complete
    theorem LeanRidgelet.lambda_symbol_even {m : ℕ} (hm : Even m) (ξ : ℝ) :
  (-1) ^ (m / 2) * (2 * ↑Real.pi * Complex.I * ↑ξ) ^ m =
    ↑(|2 * Real.pi * ξ| ^ m)
    theorem LeanRidgelet.lambda_symbol_even {m : ℕ}
  (hm : Even m) (ξ : ℝ) :
  (-1) ^ (m / 2) *
      (2 * ↑Real.pi * Complex.I * ↑ξ) ^
        m =
    ↑(|2 * Real.pi * ξ| ^ m)
    The even-order symbol identity behind the multiplier property of `Λ^m`.
  • theoremdefined in LeanRidgelet/L1/LambdaOperator.lean
    complete
    theorem LeanRidgelet.lambda_symbol_odd {m : ℕ} (hm : ¬Even m) (ξ : ℝ) :
  (-1) ^ (m / 2) * (-Complex.I * ↑ξ.sign) *
      (2 * ↑Real.pi * Complex.I * ↑ξ) ^ m =
    ↑(|2 * Real.pi * ξ| ^ m)
    theorem LeanRidgelet.lambda_symbol_odd {m : ℕ}
  (hm : ¬Even m) (ξ : ℝ) :
  (-1) ^ (m / 2) *
        (-Complex.I * ↑ξ.sign) *
      (2 * ↑Real.pi * Complex.I * ↑ξ) ^
        m =
    ↑(|2 * Real.pi * ξ| ^ m)
    The odd-order symbol identity behind the multiplier property of `Λ^m`.
  • theoremdefined in LeanRidgelet/L1/LambdaOperator.lean
    complete
    theorem LeanRidgelet.lambdaOperatorPow_eq_fourier_multiplier (m : ℕ)
  (φ : SchwartzMap ℝ ℂ) (z : ℝ) :
  LeanRidgelet.lambdaOperatorPow m (⇑φ) z =
    ∫ (ξ : ℝ),
      ↑(|2 * Real.pi * ξ| ^ m) * FourierTransform.fourier (⇑φ) ξ *
        Complex.exp (↑(2 * Real.pi * (z * ξ)) * Complex.I)
    theorem LeanRidgelet.lambdaOperatorPow_eq_fourier_multiplier
  (m : ℕ) (φ : SchwartzMap ℝ ℂ) (z : ℝ) :
  LeanRidgelet.lambdaOperatorPow m (⇑φ)
      z =
    ∫ (ξ : ℝ),
      ↑(|2 * Real.pi * ξ| ^ m) *
          FourierTransform.fourier (⇑φ)
            ξ *
        Complex.exp
          (↑(2 * Real.pi * (z * ξ)) *
            Complex.I)
    **Step A-3, the Fourier multiplier property of the Lambda operator**: on Schwartz functions
`Λ^m` acts as the Fourier multiplier `|2πξ|^m` — the manuscript's `|ω|^m` in the angular
convention `ω = 2πξ`.
  • defdefined in LeanRidgelet/L1/LambdaOperator.lean
    complete
    def LeanRidgelet.angularSchwartz (φ : SchwartzMap ℝ ℂ) : SchwartzMap ℝ ℂ
    def LeanRidgelet.angularSchwartz
  (φ : SchwartzMap ℝ ℂ) : SchwartzMap ℝ ℂ
    Implementation after :=
    :=
  SchwartzMap.compCLMOfAntilipschitz (𝕜 := ℝ)
    (hasTemperateGrowth_const_mul (2 * Real.pi)⁻¹)
    (antilipschitzWith_const_mul (by positivity : ((2 * Real.pi)⁻¹ : ℝ) ≠ 0)) (𝓕 φ)
    The angular Fourier transform of a Schwartz function, as a Schwartz function.
  • theoremdefined in LeanRidgelet/L1/LambdaOperator.lean
    complete
    theorem LeanRidgelet.lambdaOperatorPow_eq_angular (m : ℕ) (φ : SchwartzMap ℝ ℂ)
  (z : ℝ) :
  LeanRidgelet.lambdaOperatorPow m (⇑φ) z =
    (2 * Real.pi)⁻¹ •
      ∫ (ζ : ℝ),
        ↑(|ζ| ^ m) * LeanRidgelet.angularFourier1D (⇑φ) ζ *
          Complex.exp (Complex.I * ↑(z * ζ))
    theorem LeanRidgelet.lambdaOperatorPow_eq_angular
  (m : ℕ) (φ : SchwartzMap ℝ ℂ) (z : ℝ) :
  LeanRidgelet.lambdaOperatorPow m (⇑φ)
      z =
    (2 * Real.pi)⁻¹ •
      ∫ (ζ : ℝ),
        ↑(|ζ| ^ m) *
            LeanRidgelet.angularFourier1D
              (⇑φ) ζ *
          Complex.exp
            (Complex.I * ↑(z * ζ))
    The angular inverse-Fourier representation of the Lambda operator on Schwartz functions:
the angular-convention form of `lambdaOperatorPow_eq_fourier_multiplier`.
  • theoremdefined in LeanRidgelet/L1/LambdaOperator.lean
    complete
    theorem LeanRidgelet.hasFourierAwayFromOrigin_angularFourierInv {A : ℝ → ℂ}
  (hA : MeasureTheory.Integrable A MeasureTheory.volume) :
  LeanRidgelet.HasFourierAwayFromOrigin
    (fun z ↦
      (2 * Real.pi)⁻¹ •
        ∫ (ζ : ℝ), A ζ * Complex.exp (Complex.I * ↑(z * ζ)))
    A
    theorem LeanRidgelet.hasFourierAwayFromOrigin_angularFourierInv
  {A : ℝ → ℂ}
  (hA :
    MeasureTheory.Integrable A
      MeasureTheory.volume) :
  LeanRidgelet.HasFourierAwayFromOrigin
    (fun z ↦
      (2 * Real.pi)⁻¹ •
        ∫ (ζ : ℝ),
          A ζ *
            Complex.exp
              (Complex.I * ↑(z * ζ)))
    A
    **The inverse angular Fourier transform of an integrable function carries that function as
its Fourier data away from the origin.** At function level this is the substitute for the
Fourier duality `𝒪_M ≅ 𝒪'_C` by which the manuscript produces the solution `u` of the
backprojection equation of `thm:eq.ac`: the witness is bounded and continuous rather than
slowly increasing and smooth, which is all the Fourier data pairing needs.
  • theoremdefined in LeanRidgelet/L1/LambdaOperator.lean
    complete
    theorem LeanRidgelet.hasFourierAwayFromOrigin_lambdaOperatorPow (m : ℕ)
  (φ : SchwartzMap ℝ ℂ) :
  LeanRidgelet.HasFourierAwayFromOrigin
    (LeanRidgelet.lambdaOperatorPow m ⇑φ) fun ζ ↦
    ↑(|ζ| ^ m) * LeanRidgelet.angularFourier1D (⇑φ) ζ
    theorem LeanRidgelet.hasFourierAwayFromOrigin_lambdaOperatorPow
  (m : ℕ) (φ : SchwartzMap ℝ ℂ) :
  LeanRidgelet.HasFourierAwayFromOrigin
    (LeanRidgelet.lambdaOperatorPow m ⇑φ)
    fun ζ ↦
    ↑(|ζ| ^ m) *
      LeanRidgelet.angularFourier1D (⇑φ) ζ
    **The Fourier data of the Lambda operator away from the origin**: on Schwartz functions the
Fourier data of `Λ^m φ` is the multiplier `|ζ|^m φ̂(ζ)`. This is the spectral form of the
backprojection equation of the structure theorem `thm:eq.ac`.
  • theoremdefined in LeanRidgelet/L1/LambdaOperator.lean
    complete
    theorem LeanRidgelet.integrable_lambdaOperatorPow_of_even {m : ℕ} (hm : Even m)
  (φ : SchwartzMap ℝ ℂ) :
  MeasureTheory.Integrable (LeanRidgelet.lambdaOperatorPow m ⇑φ)
    MeasureTheory.volume
    theorem LeanRidgelet.integrable_lambdaOperatorPow_of_even
  {m : ℕ} (hm : Even m)
  (φ : SchwartzMap ℝ ℂ) :
  MeasureTheory.Integrable
    (LeanRidgelet.lambdaOperatorPow m ⇑φ)
    MeasureTheory.volume
    **For even `m` the filtered Schwartz function is again Schwartz**, hence integrable:
`Λ^m φ = (-1)^{m/2} φ^{(m)}`. For odd `m` the Hilbert transform intervenes and integrability is
a genuine decay estimate; see `LeanRidgelet.L1.BumpRidgelet` for the remaining gap.
  • theoremdefined in LeanRidgelet/L1/LambdaOperator.lean
    complete
    theorem LeanRidgelet.integral_iteratedDeriv_schwartz_eq_zero {m : ℕ}
  (hm : m ≠ 0) (φ : SchwartzMap ℝ ℂ) :
  ∫ (z : ℝ), iteratedDeriv m (⇑φ) z = 0
    theorem LeanRidgelet.integral_iteratedDeriv_schwartz_eq_zero
  {m : ℕ} (hm : m ≠ 0)
  (φ : SchwartzMap ℝ ℂ) :
  ∫ (z : ℝ), iteratedDeriv m (⇑φ) z = 0
    The integral of an iterated derivative of a Schwartz function vanishes.
  • theoremdefined in LeanRidgelet/L1/LambdaOperator.lean
    complete
    theorem LeanRidgelet.integrable_lambdaOperatorPow (m : ℕ) [NeZero m]
  (φ : SchwartzMap ℝ ℂ) :
  MeasureTheory.Integrable (LeanRidgelet.lambdaOperatorPow m ⇑φ)
    MeasureTheory.volume
    theorem LeanRidgelet.integrable_lambdaOperatorPow
  (m : ℕ) [NeZero m]
  (φ : SchwartzMap ℝ ℂ) :
  MeasureTheory.Integrable
    (LeanRidgelet.lambdaOperatorPow m ⇑φ)
    MeasureTheory.volume
    **`Λ^m` maps Schwartz functions into `L¹` for every `m ≥ 1`.** For even `m` the filtered
function is again Schwartz; for odd `m` it is the Hilbert transform of `φ^{(m)}`, whose integral
vanishes because it is a derivative, so the decay improves from `O(1/x)` to `O(1/x²)` and
`MeasureTheory.integrable_pvHilbertTransform_of_integral_eq_zero` applies.
  • theoremdefined in LeanRidgelet/L1/LambdaOperator.lean
    complete
    theorem LeanRidgelet.angularFourier1D_lambdaOperatorPow (m : ℕ)
  (φ : SchwartzMap ℝ ℂ)
  (hint :
    MeasureTheory.Integrable (LeanRidgelet.lambdaOperatorPow m ⇑φ)
      MeasureTheory.volume)
  (ζ : ℝ) :
  LeanRidgelet.angularFourier1D (LeanRidgelet.lambdaOperatorPow m ⇑φ)
      ζ =
    ↑(|ζ| ^ m) * LeanRidgelet.angularFourier1D (⇑φ) ζ
    theorem LeanRidgelet.angularFourier1D_lambdaOperatorPow
  (m : ℕ) (φ : SchwartzMap ℝ ℂ)
  (hint :
    MeasureTheory.Integrable
      (LeanRidgelet.lambdaOperatorPow m
        ⇑φ)
      MeasureTheory.volume)
  (ζ : ℝ) :
  LeanRidgelet.angularFourier1D
      (LeanRidgelet.lambdaOperatorPow m
        ⇑φ)
      ζ =
    ↑(|ζ| ^ m) *
      LeanRidgelet.angularFourier1D (⇑φ) ζ
    **The classical multiplier identity for the Lambda operator.** Once `Λ^m φ` is integrable —
automatic for even `m`, where `Λ^m φ = ± φ^{(m)}` — its honest angular Fourier integral is the
multiplier `|ζ|^m φ̂(ζ)` at *every* frequency, not only as Fourier data away from the origin.
This is what `cor:const.ap` needs, since the admissibility constant is defined through the
Fourier integral of the ridgelet function.

L1.FourierData: uniqueness and the convolution theorem away from the origin

Lemma2.2.11
Statement uses 4
Statement dependency previews
Preview
Definition 2.1.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

Uniqueness of Fourier data, and the convolution theorem away from the origin. Two representatives of the Fourier transform of the same function away from the origin agree almost everywhere on \mathbb R\setminus\{0\}: a smooth bump compactly supported there is a legitimate test function, so the fundamental lemma of the calculus of variations applies on that open set (third declaration; the second supplies the integrability that makes the defining pairing an honest Bochner integral). If \eta carries the Fourier data F_\eta and \psi is Schwartz, then \overline{\widetilde\psi}\ast\eta carries the Fourier data \overline{\widehat\psi}F_\eta (last declaration). The proof pairs against a test function \theta supported away from the origin, moves \overline{\widehat\psi} onto \theta — the product \theta\,\overline{\widehat\psi} is again Schwartz and again supported away from the origin — and uses the identity \widehat{\theta\,\overline{\widehat\psi}}(s)=\int\overline{\psi(s-z)}\,\widehat\theta(z)\,dz (fourth declaration; the factor (2\pi)^{-1} of the product-convolution theorem cancels against the factor 2\pi of the double transform). Fubini's theorem then exchanges the two iterated integrals: the dominating function factorizes after 1+|z-t|\le(1+|z|)(1+|t|), and the shear (z,t)\mapsto(z,z-t) of mathlib_prod_shear carries one iterated order to the other. Together with l1_lambda_multiplier this is what turns the backprojection equation of thm:eq.ac into its spectral form; the fourth declaration records that Fourier data depends only on its values away from the origin, which is what lets the two forms be compared.

Lean code for Lemma2.2.11●6 theorems
  • theoremdefined in LeanRidgelet/L1/Defs.lean
    complete
    theorem LeanRidgelet.angularFourier1D_apply (g : ℝ → ℂ) (ζ : ℝ) :
  LeanRidgelet.angularFourier1D g ζ =
    ∫ (z : ℝ), Complex.exp (-Complex.I * ↑(z * ζ)) * g z
    theorem LeanRidgelet.angularFourier1D_apply
  (g : ℝ → ℂ) (ζ : ℝ) :
  LeanRidgelet.angularFourier1D g ζ =
    ∫ (z : ℝ),
      Complex.exp
          (-Complex.I * ↑(z * ζ)) *
        g z
    The defining integral of `angularFourier1D` with the real inner product expanded.
  • theoremdefined in LeanRidgelet/L1/FourierData.lean
    complete
    theorem LeanRidgelet.integrable_mul_of_tsupport_subset_compl_singleton
  {F φ : ℝ → ℂ}
  (hF : MeasureTheory.LocallyIntegrableOn F {0}ᶜ MeasureTheory.volume)
  (hφcont : Continuous φ) (hφcs : HasCompactSupport φ)
  (hφts : tsupport φ ⊆ {0}ᶜ) :
  MeasureTheory.Integrable (fun ζ ↦ F ζ * φ ζ) MeasureTheory.volume
    theorem LeanRidgelet.integrable_mul_of_tsupport_subset_compl_singleton
  {F φ : ℝ → ℂ}
  (hF :
    MeasureTheory.LocallyIntegrableOn F
      {0}ᶜ MeasureTheory.volume)
  (hφcont : Continuous φ)
  (hφcs : HasCompactSupport φ)
  (hφts : tsupport φ ⊆ {0}ᶜ) :
  MeasureTheory.Integrable
    (fun ζ ↦ F ζ * φ ζ)
    MeasureTheory.volume
    A locally integrable function on `ℝ \ {0}` is integrable against every Schwartz function
whose (compact) support avoids the origin. This is the integrability that makes the defining
pairing of `HasFourierAwayFromOrigin` an honest Bochner integral for compactly supported test
functions.
  • theoremdefined in LeanRidgelet/L1/FourierData.lean
    complete
    theorem LeanRidgelet.hasFourierAwayFromOrigin_ae_eq {η F₁ F₂ : ℝ → ℂ}
  (h₁ : LeanRidgelet.HasFourierAwayFromOrigin η F₁)
  (h₂ : LeanRidgelet.HasFourierAwayFromOrigin η F₂) :
  F₁ =ᵐ[MeasureTheory.volume.restrict {0}ᶜ] F₂
    theorem LeanRidgelet.hasFourierAwayFromOrigin_ae_eq
  {η F₁ F₂ : ℝ → ℂ}
  (h₁ :
    LeanRidgelet.HasFourierAwayFromOrigin
      η F₁)
  (h₂ :
    LeanRidgelet.HasFourierAwayFromOrigin
      η F₂) :
  F₁ =ᵐ[MeasureTheory.volume.restrict
      {0}ᶜ]
    F₂
    **Uniqueness of Fourier data away from the origin.** A function has at most one Fourier
transform away from the origin, up to a null set of `ℝ \ {0}`. Together with
`LeanRidgelet.l1_hasFourierAwayFromOrigin_add_polynomial` this says that `η ↦ Fη` realizes the
Lizorkin quotient `𝒮'(ℝ)/𝒫 ≅ 𝒮₀'(ℝ)` faithfully at function level.
  • theoremdefined in LeanRidgelet/L1/FourierData.lean
    complete
    theorem LeanRidgelet.HasFourierAwayFromOrigin.congr_data {η F₁ F₂ : ℝ → ℂ}
  (h : LeanRidgelet.HasFourierAwayFromOrigin η F₁)
  (hF : Set.EqOn F₁ F₂ {0}ᶜ) :
  LeanRidgelet.HasFourierAwayFromOrigin η F₂
    theorem LeanRidgelet.HasFourierAwayFromOrigin.congr_data
  {η F₁ F₂ : ℝ → ℂ}
  (h :
    LeanRidgelet.HasFourierAwayFromOrigin
      η F₁)
  (hF : Set.EqOn F₁ F₂ {0}ᶜ) :
  LeanRidgelet.HasFourierAwayFromOrigin η
    F₂
    Fourier data away from the origin depends only on the values of the representative away
from the origin.
  • theoremdefined in LeanRidgelet/L1/FourierData.lean
    complete
    theorem LeanRidgelet.angularFourier1D_mul_conj_angularFourier1D
  (ψ θ : SchwartzMap ℝ ℂ) (s : ℝ) :
  LeanRidgelet.angularFourier1D
      (fun ζ ↦
        θ ζ * (starRingEnd ℂ) (LeanRidgelet.angularFourier1D (⇑ψ) ζ))
      s =
    ∫ (z : ℝ),
      (starRingEnd ℂ) (ψ (s - z)) * LeanRidgelet.angularFourier1D (⇑θ) z
    theorem LeanRidgelet.angularFourier1D_mul_conj_angularFourier1D
  (ψ θ : SchwartzMap ℝ ℂ) (s : ℝ) :
  LeanRidgelet.angularFourier1D
      (fun ζ ↦
        θ ζ *
          (starRingEnd ℂ)
            (LeanRidgelet.angularFourier1D
              (⇑ψ) ζ))
      s =
    ∫ (z : ℝ),
      (starRingEnd ℂ) (ψ (s - z)) *
        LeanRidgelet.angularFourier1D (⇑θ)
          z
    The angular Fourier transform of the product of a Schwartz test function `θ` with the
conjugate transform `conj (ψ̂)` of a Schwartz function: `(θ ⬝ conj (ψ̂))^(s) =
∫ conj (ψ (s - z)) θ̂(z) dz`. In the manuscript's convention the product-convolution theorem
carries the factor `(2π)⁻¹`, which here cancels against the factor `2π` of the double transform
`angularFourier1D² = 2π ⬝ (reflection)`.
  • theoremdefined in LeanRidgelet/L1/FourierData.lean
    complete
    theorem LeanRidgelet.hasFourierAwayFromOrigin_reflectedConjConvolution
  (ψ : SchwartzMap ℝ ℂ) {v Fv : ℝ → ℂ}
  (hv : LeanRidgelet.HasFourierAwayFromOrigin v Fv) :
  LeanRidgelet.HasFourierAwayFromOrigin
    (LeanRidgelet.reflectedConjConvolution (⇑ψ) v) fun ζ ↦
    (starRingEnd ℂ) (LeanRidgelet.angularFourier1D (⇑ψ) ζ) * Fv ζ
    theorem LeanRidgelet.hasFourierAwayFromOrigin_reflectedConjConvolution
  (ψ : SchwartzMap ℝ ℂ) {v Fv : ℝ → ℂ}
  (hv :
    LeanRidgelet.HasFourierAwayFromOrigin
      v Fv) :
  LeanRidgelet.HasFourierAwayFromOrigin
    (LeanRidgelet.reflectedConjConvolution
      (⇑ψ) v)
    fun ζ ↦
    (starRingEnd ℂ)
        (LeanRidgelet.angularFourier1D
          (⇑ψ) ζ) *
      Fv ζ
    **The convolution theorem away from the origin.** If the activation `v` carries the Fourier
data `Fv` away from the origin then the convolution `conj (ψ~) ⋆ v` with a Schwartz ridgelet
function carries the Fourier data `conj (ψ̂) Fv`. This is what turns the physical backprojection
equation of `thm:eq.ac` into its spectral form.

L1.Plancherel, L1.ReconstructionL2: the L² layer

Lemma2.2.12
Statement uses 2
Statement dependency previews
Preview
Theorem 2.2.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 2.1.20
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Strong measurability and the lintegral form of Plancherel's identity. The ridgelet transform is strongly measurable on parameter space, for the Lebesgue and the weighted measure and for every homogeneity index. Plancherel's identity is proved first in lintegral form — eq:fstridge factors the fibre, the fibrewise L¹ ∩ L² Plancherel identity in the angular convention evaluates it, the weight \|a\|^{-2} cancels against \|a\|^2, Tonelli's theorem and the dilation change of variables \xi=\zeta a reduce it to the m-dimensional Plancherel identity, and K_{\psi,\psi}=1 closes it. Square-integrability \mathscr R_\psi f\in L^2(\mathbb Y^{m+1}) follows, and drives both l1_parseval_plancherel and the bounded extension l1_L2_extension.

Lean code for Lemma2.2.12●4 theorems
  • theoremdefined in LeanRidgelet/L1/Plancherel.lean
    complete
    theorem LeanRidgelet.aestronglyMeasurable_euclideanRidgeletTransform (m : ℕ)
  (s : ℝ) {ψ : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hψc : Continuous ψ) :
  MeasureTheory.AEStronglyMeasurable
    (LeanRidgelet.euclideanRidgeletTransform m s ψ f)
    MeasureTheory.volume
    theorem LeanRidgelet.aestronglyMeasurable_euclideanRidgeletTransform
  (m : ℕ) (s : ℝ) {ψ : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hψc : Continuous ψ) :
  MeasureTheory.AEStronglyMeasurable
    (LeanRidgelet.euclideanRidgeletTransform
      m s ψ f)
    MeasureTheory.volume
    The ridgelet transform of an integrable function against a continuous ridgelet function is
strongly measurable on the parameter space (with Lebesgue measure).
  • theoremdefined in LeanRidgelet/L1/Plancherel.lean
    complete
    theorem LeanRidgelet.aestronglyMeasurable_euclideanRidgeletTransform_parameterMeasure
  (m : ℕ) (s : ℝ) {ψ : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hψc : Continuous ψ) :
  MeasureTheory.AEStronglyMeasurable
    (LeanRidgelet.euclideanRidgeletTransform m s ψ f)
    (LeanRidgelet.ridgeletParameterMeasure m)
    theorem LeanRidgelet.aestronglyMeasurable_euclideanRidgeletTransform_parameterMeasure
  (m : ℕ) (s : ℝ) {ψ : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hψc : Continuous ψ) :
  MeasureTheory.AEStronglyMeasurable
    (LeanRidgelet.euclideanRidgeletTransform
      m s ψ f)
    (LeanRidgelet.ridgeletParameterMeasure
      m)
    The ridgelet transform of an integrable function against a continuous ridgelet function is
strongly measurable with respect to the weighted parameter measure `‖a‖⁻² da db`.
  • theoremdefined in LeanRidgelet/L1/Plancherel.lean
    complete
    theorem LeanRidgelet.lintegral_enorm_euclideanRidgeletTransform_sq (m : ℕ)
  [NeZero m] {ψ : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  (hself : LeanRidgelet.IsSelfAdmissible m ψ)
  (hK :
    LeanRidgelet.admissibilityConstant m ψ
        (LeanRidgelet.angularFourier1D ψ) =
      1)
  (hψc : Continuous ψ) (hψb : ∃ C, ∀ (z : ℝ), ‖ψ z‖ ≤ C)
  (hf1 : MeasureTheory.Integrable f MeasureTheory.volume)
  (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) :
  ∫⁻ (q : LeanRidgelet.RidgeletParameterSpace m),
      ‖LeanRidgelet.euclideanRidgeletTransform m 1 ψ f q‖ₑ ^
        2 ∂LeanRidgelet.ridgeletParameterMeasure m =
    ∫⁻ (x : LeanRidgelet.InputSpace m), ‖f x‖ₑ ^ 2
    theorem LeanRidgelet.lintegral_enorm_euclideanRidgeletTransform_sq
  (m : ℕ) [NeZero m] {ψ : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hself :
    LeanRidgelet.IsSelfAdmissible m ψ)
  (hK :
    LeanRidgelet.admissibilityConstant m ψ
        (LeanRidgelet.angularFourier1D
          ψ) =
      1)
  (hψc : Continuous ψ)
  (hψb : ∃ C, ∀ (z : ℝ), ‖ψ z‖ ≤ C)
  (hf1 :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hf2 :
    MeasureTheory.MemLp f 2
      MeasureTheory.volume) :
  ∫⁻ (q :
      LeanRidgelet.RidgeletParameterSpace
        m),
      ‖LeanRidgelet.euclideanRidgeletTransform
            m 1 ψ f q‖ₑ ^
        2 ∂LeanRidgelet.ridgeletParameterMeasure
        m =
    ∫⁻ (x : LeanRidgelet.InputSpace m),
      ‖f x‖ₑ ^ 2
    Plancherel's identity for the ridgelet transform (`thm:parseval`), `lintegral` form: for a
self-admissible `ψ` normalized by `K_{ψ,ψ} = 1` and `f ∈ L¹ ∩ L²(ℝ^m)`,
`∫⁻ ‖R_ψ f‖ₑ² d(‖a‖⁻² da db) = ∫⁻ ‖f‖ₑ²`. This form drives the square-integrability of the
transform and its bounded `L²` extension `l1_ridgeletTransform_L2_extension`.
  • theoremdefined in LeanRidgelet/L1/Plancherel.lean
    complete
    theorem LeanRidgelet.memLp_two_euclideanRidgeletTransform (m : ℕ) [NeZero m]
  {ψ : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  (hself : LeanRidgelet.IsSelfAdmissible m ψ)
  (hK :
    LeanRidgelet.admissibilityConstant m ψ
        (LeanRidgelet.angularFourier1D ψ) =
      1)
  (hψc : Continuous ψ) (hψb : ∃ C, ∀ (z : ℝ), ‖ψ z‖ ≤ C)
  (hf1 : MeasureTheory.Integrable f MeasureTheory.volume)
  (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) :
  MeasureTheory.MemLp (LeanRidgelet.euclideanRidgeletTransform m 1 ψ f)
    2 (LeanRidgelet.ridgeletParameterMeasure m)
    theorem LeanRidgelet.memLp_two_euclideanRidgeletTransform
  (m : ℕ) [NeZero m] {ψ : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hself :
    LeanRidgelet.IsSelfAdmissible m ψ)
  (hK :
    LeanRidgelet.admissibilityConstant m ψ
        (LeanRidgelet.angularFourier1D
          ψ) =
      1)
  (hψc : Continuous ψ)
  (hψb : ∃ C, ∀ (z : ℝ), ‖ψ z‖ ≤ C)
  (hf1 :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hf2 :
    MeasureTheory.MemLp f 2
      MeasureTheory.volume) :
  MeasureTheory.MemLp
    (LeanRidgelet.euclideanRidgeletTransform
      m 1 ψ f)
    2
    (LeanRidgelet.ridgeletParameterMeasure
      m)
    On `L¹ ∩ L²(ℝ^m)`, the ridgelet transform of a self-admissible normalized ridgelet function
is square-integrable on the parameter space: `R_ψ f ∈ L²(𝕐^{m+1})`.
Lemma2.2.13
Statement uses 3
Statement dependency previews
Preview
Theorem 2.1.13
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

The three quantitative steps of thm:formula.L2. (i) Truncated duality: the identity thm:dual, applied to the data 1_A\mathscr R_\psi f truncated to the annulus A=\{\varepsilon\le\|a\|\le\delta\} — whose weighted form is integrable because \|\mathscr R_\psi f(a,\cdot)\|_1\le\|f\|_1\|\psi\|_1\|a\| — identifies \langle\mathscr R^\dagger_\eta[\mathscr R_\psi f](\cdot;\varepsilon,\delta),g\rangle with \langle\mathscr R_\psi f,\mathscr R_\eta g\rangle_{L^2(A)}. (ii) Error bound: subtracting Parseval's relation, the error pairs with g as -\langle\mathscr R_\psi f,\mathscr R_\eta g\rangle_{L^2(A^c)}, which Cauchy--Schwarz and the Plancherel identity for \eta bound by \|\mathscr R_\psi f\|_{L^2(A^c)}\|g\|_2; since the truncated reconstruction is bounded and measurable, the upstream L² duality criterion — testing against the truncations of the error to an exhausting sequence of balls — converts this into \|\mathscr R^\dagger_\eta[\mathscr R_\psi f](\cdot;\varepsilon,\delta)-f\|_2\le\|\mathscr R_\psi f\|_{L^2(A^c)}, with no a priori L²-membership of the truncated reconstruction. (iii) Vanishing tail: dominated convergence along the truncation filter sends \|\mathscr R_\psi f\|_{L^2(A^c)} to zero, because the annulus exhausts \mathbb Y^{m+1} up to the null set of vanishing weights.

Lean code for Lemma2.2.13●7 theorems
  • theoremdefined in LeanRidgelet/L1/ReconstructionL2.lean
    complete
    theorem LeanRidgelet.integral_norm_euclideanRidgeletTransform_bias_le (m : ℕ)
  (s : ℝ) {ψ : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hψ : MeasureTheory.Integrable ψ MeasureTheory.volume)
  (a : LeanRidgelet.InputSpace m) :
  ∫ (b : ℝ), ‖LeanRidgelet.euclideanRidgeletTransform m s ψ f (a, b)‖ ≤
    ((∫ (x : LeanRidgelet.InputSpace m), ‖f x‖) * ∫ (z : ℝ), ‖ψ z‖) *
      ‖a‖ ^ s
    theorem LeanRidgelet.integral_norm_euclideanRidgeletTransform_bias_le
  (m : ℕ) (s : ℝ) {ψ : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hψ :
    MeasureTheory.Integrable ψ
      MeasureTheory.volume)
  (a : LeanRidgelet.InputSpace m) :
  ∫ (b : ℝ),
      ‖LeanRidgelet.euclideanRidgeletTransform
          m s ψ f (a, b)‖ ≤
    ((∫ (x : LeanRidgelet.InputSpace m),
          ‖f x‖) *
        ∫ (z : ℝ), ‖ψ z‖) *
      ‖a‖ ^ s
    The `L¹` norm of the ridgelet transform in the bias variable is bounded by
`‖f‖₁ ‖ψ‖₁ ‖a‖^s`.
  • theoremdefined in LeanRidgelet/L1/ReconstructionL2.lean
    complete
    theorem LeanRidgelet.integrable_weight_indicator_euclideanRidgeletTransform
  (m : ℕ) {ψ : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hψ : MeasureTheory.Integrable ψ MeasureTheory.volume)
  (hψc : Continuous ψ) {ε δ : ℝ} (hε : 0 < ε) :
  MeasureTheory.Integrable
    (fun q ↦
      {p | ε ≤ ‖p.1‖ ∧ ‖p.1‖ ≤ δ}.indicator
          (LeanRidgelet.euclideanRidgeletTransform m 1 ψ f) q *
        (↑‖q.1‖)⁻¹)
    MeasureTheory.volume
    theorem LeanRidgelet.integrable_weight_indicator_euclideanRidgeletTransform
  (m : ℕ) {ψ : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hψ :
    MeasureTheory.Integrable ψ
      MeasureTheory.volume)
  (hψc : Continuous ψ) {ε δ : ℝ}
  (hε : 0 < ε) :
  MeasureTheory.Integrable
    (fun q ↦
      {p |
              ε ≤ ‖p.1‖ ∧
                ‖p.1‖ ≤ δ}.indicator
          (LeanRidgelet.euclideanRidgeletTransform
            m 1 ψ f)
          q *
        (↑‖q.1‖)⁻¹)
    MeasureTheory.volume
    With a positive inner truncation radius the truncated ridgelet data has an integrable
weighted form, the hypothesis of the duality identity `l1_dualRidgeletTransform_pairing`.
  • theoremdefined in LeanRidgelet/L1/ReconstructionL2.lean
    complete
    theorem LeanRidgelet.norm_truncatedDualRidgeletTransform_le (m : ℕ) {η : ℝ → ℂ}
  {Cη : ℝ} {T : LeanRidgelet.RidgeletParameterSpace m → ℂ} {ε δ : ℝ}
  (hTm : MeasureTheory.AEStronglyMeasurable T MeasureTheory.volume)
  (hT :
    MeasureTheory.Integrable (fun q ↦ T q * (↑‖q.1‖)⁻¹)
      MeasureTheory.volume)
  (hηc : Continuous η) (hηb : ∀ (z : ℝ), ‖η z‖ ≤ Cη)
  (x : LeanRidgelet.InputSpace m) :
  ‖LeanRidgelet.truncatedDualRidgeletTransform m 1 η T ε δ x‖ ≤
    Cη *
      ∫ (q : LeanRidgelet.RidgeletParameterSpace m), ‖T q * (↑‖q.1‖)⁻¹‖
    theorem LeanRidgelet.norm_truncatedDualRidgeletTransform_le
  (m : ℕ) {η : ℝ → ℂ} {Cη : ℝ}
  {T :
    LeanRidgelet.RidgeletParameterSpace
        m →
      ℂ}
  {ε δ : ℝ}
  (hTm :
    MeasureTheory.AEStronglyMeasurable T
      MeasureTheory.volume)
  (hT :
    MeasureTheory.Integrable
      (fun q ↦ T q * (↑‖q.1‖)⁻¹)
      MeasureTheory.volume)
  (hηc : Continuous η)
  (hηb : ∀ (z : ℝ), ‖η z‖ ≤ Cη)
  (x : LeanRidgelet.InputSpace m) :
  ‖LeanRidgelet.truncatedDualRidgeletTransform
        m 1 η T ε δ x‖ ≤
    Cη *
      ∫ (q :
        LeanRidgelet.RidgeletParameterSpace
          m),
        ‖T q * (↑‖q.1‖)⁻¹‖
    The truncated dual ridgelet transform of weighted-integrable data against a bounded
activation is uniformly bounded in the input variable.
  • theoremdefined in LeanRidgelet/L1/ReconstructionL2.lean
    complete
    theorem LeanRidgelet.aestronglyMeasurable_truncatedDualRidgeletTransform (m : ℕ)
  {η : ℝ → ℂ} {T : LeanRidgelet.RidgeletParameterSpace m → ℂ} {ε δ : ℝ}
  (hTm : MeasureTheory.AEStronglyMeasurable T MeasureTheory.volume)
  (hηc : Continuous η) :
  MeasureTheory.AEStronglyMeasurable
    (LeanRidgelet.truncatedDualRidgeletTransform m 1 η T ε δ)
    MeasureTheory.volume
    theorem LeanRidgelet.aestronglyMeasurable_truncatedDualRidgeletTransform
  (m : ℕ) {η : ℝ → ℂ}
  {T :
    LeanRidgelet.RidgeletParameterSpace
        m →
      ℂ}
  {ε δ : ℝ}
  (hTm :
    MeasureTheory.AEStronglyMeasurable T
      MeasureTheory.volume)
  (hηc : Continuous η) :
  MeasureTheory.AEStronglyMeasurable
    (LeanRidgelet.truncatedDualRidgeletTransform
      m 1 η T ε δ)
    MeasureTheory.volume
    The truncated dual ridgelet transform of measurable data against a continuous activation is
almost-everywhere strongly measurable in the input variable.
  • theoremdefined in LeanRidgelet/L1/ReconstructionL2.lean
    complete
    theorem LeanRidgelet.setIntegral_annulus_ridgeletTransform_mul_conj (m : ℕ)
  [NeZero m] {ψ η : ℝ → ℂ} {f g : LeanRidgelet.InputSpace m → ℂ}
  {ε δ : ℝ} (hε : 0 < ε)
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hψ : MeasureTheory.Integrable ψ MeasureTheory.volume)
  (hψc : Continuous ψ)
  (hg : MeasureTheory.Integrable g MeasureTheory.volume)
  (hηc : Continuous η) (hηb : ∃ C, ∀ (z : ℝ), ‖η z‖ ≤ C) :
  ∫ (q : LeanRidgelet.RidgeletParameterSpace m) in
      {p | ε ≤ ‖p.1‖ ∧ ‖p.1‖ ≤ δ},
      LeanRidgelet.euclideanRidgeletTransform m 1 ψ f q *
        (starRingEnd ℂ)
          (LeanRidgelet.euclideanRidgeletTransform m 1 η g
            q) ∂LeanRidgelet.ridgeletParameterMeasure m =
    ∫ (x : LeanRidgelet.InputSpace m),
      LeanRidgelet.truncatedDualRidgeletTransform m 1 η
          (LeanRidgelet.euclideanRidgeletTransform m 1 ψ f) ε δ x *
        (starRingEnd ℂ) (g x)
    theorem LeanRidgelet.setIntegral_annulus_ridgeletTransform_mul_conj
  (m : ℕ) [NeZero m] {ψ η : ℝ → ℂ}
  {f g : LeanRidgelet.InputSpace m → ℂ}
  {ε δ : ℝ} (hε : 0 < ε)
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hψ :
    MeasureTheory.Integrable ψ
      MeasureTheory.volume)
  (hψc : Continuous ψ)
  (hg :
    MeasureTheory.Integrable g
      MeasureTheory.volume)
  (hηc : Continuous η)
  (hηb : ∃ C, ∀ (z : ℝ), ‖η z‖ ≤ C) :
  ∫ (q :
      LeanRidgelet.RidgeletParameterSpace
        m) in
      {p | ε ≤ ‖p.1‖ ∧ ‖p.1‖ ≤ δ},
      LeanRidgelet.euclideanRidgeletTransform
          m 1 ψ f q *
        (starRingEnd ℂ)
          (LeanRidgelet.euclideanRidgeletTransform
            m 1 η g
            q) ∂LeanRidgelet.ridgeletParameterMeasure
        m =
    ∫ (x : LeanRidgelet.InputSpace m),
      LeanRidgelet.truncatedDualRidgeletTransform
          m 1 η
          (LeanRidgelet.euclideanRidgeletTransform
            m 1 ψ f)
          ε δ x *
        (starRingEnd ℂ) (g x)
    **The truncated duality identity**: the pairing of the ridgelet transform of `f` against the
ridgelet transform of `g` over the scale annulus `ε ≤ ‖a‖ ≤ δ` is the pairing of the truncated
reconstruction of `f` against `g`.
  • theoremdefined in LeanRidgelet/L1/ReconstructionL2.lean
    complete
    theorem LeanRidgelet.eLpNorm_truncatedDualRidgeletTransform_sub_le (m : ℕ)
  [NeZero m] {ψ η : ℝ → ℂ} {f : LeanRidgelet.InputSpace m → ℂ}
  (hψself : LeanRidgelet.IsSelfAdmissible m ψ)
  (hKψ :
    LeanRidgelet.admissibilityConstant m ψ
        (LeanRidgelet.angularFourier1D ψ) =
      1)
  (hηself : LeanRidgelet.IsSelfAdmissible m η)
  (hKη :
    LeanRidgelet.admissibilityConstant m η
        (LeanRidgelet.angularFourier1D η) =
      1)
  (hK :
    LeanRidgelet.admissibilityConstant m ψ
        (LeanRidgelet.angularFourier1D η) =
      1)
  (hψc : Continuous ψ) (hψb : ∃ C, ∀ (z : ℝ), ‖ψ z‖ ≤ C)
  (hηc : Continuous η) (hηb : ∃ C, ∀ (z : ℝ), ‖η z‖ ≤ C)
  (hf1 : MeasureTheory.Integrable f MeasureTheory.volume)
  (hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) {ε δ : ℝ}
  (hε : 0 < ε) :
  MeasureTheory.eLpNorm
      (fun x ↦
        LeanRidgelet.truncatedDualRidgeletTransform m 1 η
            (LeanRidgelet.euclideanRidgeletTransform m 1 ψ f) ε δ x -
          f x)
      2 MeasureTheory.volume ≤
    ENNReal.ofReal
      √(∫ (q : LeanRidgelet.RidgeletParameterSpace m) in
          {p | ε ≤ ‖p.1‖ ∧ ‖p.1‖ ≤ δ}ᶜ,
          ‖LeanRidgelet.euclideanRidgeletTransform m 1 ψ f q‖ ^
            2 ∂LeanRidgelet.ridgeletParameterMeasure m)
    theorem LeanRidgelet.eLpNorm_truncatedDualRidgeletTransform_sub_le
  (m : ℕ) [NeZero m] {ψ η : ℝ → ℂ}
  {f : LeanRidgelet.InputSpace m → ℂ}
  (hψself :
    LeanRidgelet.IsSelfAdmissible m ψ)
  (hKψ :
    LeanRidgelet.admissibilityConstant m ψ
        (LeanRidgelet.angularFourier1D
          ψ) =
      1)
  (hηself :
    LeanRidgelet.IsSelfAdmissible m η)
  (hKη :
    LeanRidgelet.admissibilityConstant m η
        (LeanRidgelet.angularFourier1D
          η) =
      1)
  (hK :
    LeanRidgelet.admissibilityConstant m ψ
        (LeanRidgelet.angularFourier1D
          η) =
      1)
  (hψc : Continuous ψ)
  (hψb : ∃ C, ∀ (z : ℝ), ‖ψ z‖ ≤ C)
  (hηc : Continuous η)
  (hηb : ∃ C, ∀ (z : ℝ), ‖η z‖ ≤ C)
  (hf1 :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hf2 :
    MeasureTheory.MemLp f 2
      MeasureTheory.volume)
  {ε δ : ℝ} (hε : 0 < ε) :
  MeasureTheory.eLpNorm
      (fun x ↦
        LeanRidgelet.truncatedDualRidgeletTransform
            m 1 η
            (LeanRidgelet.euclideanRidgeletTransform
              m 1 ψ f)
            ε δ x -
          f x)
      2 MeasureTheory.volume ≤
    ENNReal.ofReal
      √(∫ (q :
          LeanRidgelet.RidgeletParameterSpace
            m) in
          {p | ε ≤ ‖p.1‖ ∧ ‖p.1‖ ≤ δ}ᶜ,
          ‖LeanRidgelet.euclideanRidgeletTransform
                m 1 ψ f q‖ ^
            2 ∂LeanRidgelet.ridgeletParameterMeasure
            m)
    **Reconstruction error bound in `L²`**: for normalized self-admissible `ψ` and `η` paired
with `K_{ψ,η} = 1`, the truncated reconstruction error is bounded by the energy of the ridgelet
transform outside the scale annulus.
  • theoremdefined in LeanRidgelet/L1/ReconstructionL2.lean
    complete
    theorem LeanRidgelet.tendsto_setIntegral_compl_annulus_norm_sq (m : ℕ)
  [NeZero m] {G : LeanRidgelet.RidgeletParameterSpace m → ℂ}
  (hG :
    MeasureTheory.Integrable (fun p ↦ ‖G p‖ ^ 2)
      (LeanRidgelet.ridgeletParameterMeasure m)) :
  Filter.Tendsto
    (fun q ↦
      ∫ (p : LeanRidgelet.RidgeletParameterSpace m) in
        {p | q.1 ≤ ‖p.1‖ ∧ ‖p.1‖ ≤ q.2}ᶜ,
        ‖G p‖ ^ 2 ∂LeanRidgelet.ridgeletParameterMeasure m)
    LeanRidgelet.ridgeletTruncationFilter (nhds 0)
    theorem LeanRidgelet.tendsto_setIntegral_compl_annulus_norm_sq
  (m : ℕ) [NeZero m]
  {G :
    LeanRidgelet.RidgeletParameterSpace
        m →
      ℂ}
  (hG :
    MeasureTheory.Integrable
      (fun p ↦ ‖G p‖ ^ 2)
      (LeanRidgelet.ridgeletParameterMeasure
        m)) :
  Filter.Tendsto
    (fun q ↦
      ∫ (p :
        LeanRidgelet.RidgeletParameterSpace
          m) in
        {p | q.1 ≤ ‖p.1‖ ∧ ‖p.1‖ ≤ q.2}ᶜ,
        ‖G p‖ ^
          2 ∂LeanRidgelet.ridgeletParameterMeasure
          m)
    LeanRidgelet.ridgeletTruncationFilter
    (nhds 0)
    The energy of a square-integrable parameter function outside the scale annulus tends to zero
along the truncation filter: the annulus exhausts the parameter space up to the null set of
vanishing weights.

L1.BumpRidgelet: the explicit witness

Lemma2.2.14
Statement uses 2
Statement dependency previews
Preview
Definition 2.1.8
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

Construction of the explicit admissible ridgelet function. Take a smooth bump supported in (5\pi/2,7\pi/2), positive at its centre 3\pi, as the spectrum, and let \psi be its inverse Fourier transform; it is Schwartz, hence integrable with all weighted moments finite. Against the Fourier data k!/(i\zeta)^{k+1} of the truncated power the admissibility integrand becomes a fixed nonzero constant times the nonnegative continuous compactly supported density \zeta\mapsto\widehat\psi(\zeta)/(\zeta^{k+1}|\zeta|^m) on the positive half-line, so it is integrable and its integral is strictly positive; hence K_{\psi,z_+^k}\ne0. All moments of \psi vanish because its spectrum vanishes near the origin. The last declaration records the ReLU growth bound \|z_+\|\le1+|z| used when the pair is fed into the reconstruction formula.

Lean code for Lemma2.2.14●8 declarations
  • defdefined in LeanRidgelet/L1/BumpRidgelet.lean
    complete
    def LeanRidgelet.spectrumBump : SchwartzMap ℝ ℂ
    def LeanRidgelet.spectrumBump :
  SchwartzMap ℝ ℂ
    Implementation after :=
    :=
  HasCompactSupport.toSchwartzMap
    (f := fun ξ : ℝ => ((spectrumBumpFn ξ : ℝ) : ℂ))
    (spectrumBumpFn.hasCompactSupport.comp_left Complex.ofReal_zero)
    (Complex.ofRealCLM.contDiff.comp spectrumBumpFn.contDiff)
    The frequency bump as a complex-valued Schwartz function.
  • defdefined in LeanRidgelet/L1/BumpRidgelet.lean
    complete
    def LeanRidgelet.bumpRidgeletSchwartz : SchwartzMap ℝ ℂ
    def LeanRidgelet.bumpRidgeletSchwartz :
  SchwartzMap ℝ ℂ
    Implementation after :=
    := 𝓕⁻ spectrumBump
    The explicit ridgelet function of the universality theorem: the inverse Fourier transform of
the frequency bump. Its spectrum is smooth, compactly supported and supported away from the
origin, which makes it admissible against every truncated power and gives it vanishing moments
of every order.
  • defdefined in LeanRidgelet/L1/BumpRidgelet.lean
    complete
    def LeanRidgelet.bumpAdmissibilityDensity (m k : ℕ) : ℝ → ℝ
    def LeanRidgelet.bumpAdmissibilityDensity
  (m k : ℕ) : ℝ → ℝ
    Implementation after :=
    :=
  fun ζ => spectrumBumpFn ((2 * Real.pi)⁻¹ * ζ) / (ζ ^ (k + 1) * |ζ| ^ m)
    The real density of the admissibility integral of the pair `(bumpRidgelet, z₊^k)`.
  • theoremdefined in LeanRidgelet/L1/BumpRidgelet.lean
    complete
    theorem LeanRidgelet.admissibilityIntegrand_bumpRidgelet (m k : ℕ) (ζ : ℝ) :
  (starRingEnd ℂ)
          (LeanRidgelet.angularFourier1D LeanRidgelet.bumpRidgelet ζ) *
        LeanRidgelet.truncatedPowerFourier k ζ /
      ↑(|ζ| ^ m) =
    ↑k.factorial / Complex.I ^ (k + 1) *
      ↑(LeanRidgelet.bumpAdmissibilityDensity m k ζ)
    theorem LeanRidgelet.admissibilityIntegrand_bumpRidgelet
  (m k : ℕ) (ζ : ℝ) :
  (starRingEnd ℂ)
          (LeanRidgelet.angularFourier1D
            LeanRidgelet.bumpRidgelet ζ) *
        LeanRidgelet.truncatedPowerFourier
          k ζ /
      ↑(|ζ| ^ m) =
    ↑k.factorial / Complex.I ^ (k + 1) *
      ↑(LeanRidgelet.bumpAdmissibilityDensity
          m k ζ)
    The admissibility integrand of the pair `(bumpRidgelet, z₊^k)` is a fixed nonzero constant
times the real density `bumpAdmissibilityDensity`.
  • theoremdefined in LeanRidgelet/L1/BumpRidgelet.lean
    complete
    theorem LeanRidgelet.integral_bumpAdmissibilityDensity_pos (m k : ℕ) :
  0 < ∫ (ζ : ℝ), LeanRidgelet.bumpAdmissibilityDensity m k ζ
    theorem LeanRidgelet.integral_bumpAdmissibilityDensity_pos
  (m k : ℕ) :
  0 <
    ∫ (ζ : ℝ),
      LeanRidgelet.bumpAdmissibilityDensity
        m k ζ
  • theoremdefined in LeanRidgelet/L1/BumpRidgelet.lean
    complete
    theorem LeanRidgelet.admissibilityConstant_bumpRidgelet_ne_zero (m k : ℕ) :
  LeanRidgelet.admissibilityConstant m LeanRidgelet.bumpRidgelet
      (LeanRidgelet.truncatedPowerFourier k) ≠
    0
    theorem LeanRidgelet.admissibilityConstant_bumpRidgelet_ne_zero
  (m k : ℕ) :
  LeanRidgelet.admissibilityConstant m
      LeanRidgelet.bumpRidgelet
      (LeanRidgelet.truncatedPowerFourier
        k) ≠
    0
  • theoremdefined in LeanRidgelet/L1/BumpRidgelet.lean
    complete
    theorem LeanRidgelet.integrable_weight_bumpRidgelet (k : ℕ) :
  MeasureTheory.Integrable
    (fun s ↦ (1 + |s|) ^ k * ‖LeanRidgelet.bumpRidgelet s‖)
    MeasureTheory.volume
    theorem LeanRidgelet.integrable_weight_bumpRidgelet
  (k : ℕ) :
  MeasureTheory.Integrable
    (fun s ↦
      (1 + |s|) ^ k *
        ‖LeanRidgelet.bumpRidgelet s‖)
    MeasureTheory.volume
  • theoremdefined in LeanRidgelet/L1/BumpRidgelet.lean
    complete
    theorem LeanRidgelet.norm_truncatedPower_one_le (z : ℝ) :
  ‖LeanRidgelet.truncatedPower 1 z‖ ≤ 1 * (1 + |z|) ^ 1
    theorem LeanRidgelet.norm_truncatedPower_one_le
  (z : ℝ) :
  ‖LeanRidgelet.truncatedPower 1 z‖ ≤
    1 * (1 + |z|) ^ 1