8.3.1. Lemma 3.1 — Homogeneous Gaussian mixture (lem:homogeneous-mixture)🔗

Blueprint node: Lemma 2.1.4. Status: verified (all 6 Lean theorems verified).

Formalization note. Stated for Gaussian layers N with IsCenteredGaussianLayers P N (ν_α := gaussianMixture N α, a Giry-monad bind); parts: σ-finite, finite on bounded Borel sets, ν_α(H) = ∞, full support (IsOpenPosMeasure), the pushforward identity, and its integrated form for nonnegative Borel F. The existence of the layers is the separate infrastructure statement OperatorRidgelet.exists_isCenteredGaussianLayers.

OperatorRidgelet.Paper.lem_homogeneous_mixture_i, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:homogeneous-mixture]** Homogeneous Gaussian mixture.  In infinite dimension the
mixture `ν_α` is σ-finite. -/
theorem lem_homogeneous_mixture_i (hH : ¬ FiniteDimensional ℝ H) {P : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) {N : ℝ → Measure H} (hN : IsCenteredGaussianLayers P N)
    {α : ℝ} (hα : 0 < α) :
    SigmaFinite (gaussianMixture N α) := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_homogeneous_mixture_ii, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:homogeneous-mixture]** Homogeneous Gaussian mixture.  The mixture `ν_α` is
finite on bounded Borel sets. -/
theorem lem_homogeneous_mixture_ii (hH : ¬ FiniteDimensional ℝ H) {P : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) {N : ℝ → Measure H} (hN : IsCenteredGaussianLayers P N)
    {α : ℝ} (hα : 0 < α) :
    ∀ E : Set H, MeasurableSet E → Bornology.IsBounded E → gaussianMixture N α E < ⊤ := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_homogeneous_mixture_iii, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:homogeneous-mixture]** Homogeneous Gaussian mixture.  The mixture `ν_α` is
infinite on `H`. -/
theorem lem_homogeneous_mixture_iii (hH : ¬ FiniteDimensional ℝ H) {P : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) {N : ℝ → Measure H} (hN : IsCenteredGaussianLayers P N)
    {α : ℝ} (hα : 0 < α) :
    gaussianMixture N α Set.univ = ⊤ := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_homogeneous_mixture_iv, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:homogeneous-mixture]** Homogeneous Gaussian mixture.  The mixture `ν_α` has
full support: it charges every nonempty open set. -/
theorem lem_homogeneous_mixture_iv (hH : ¬ FiniteDimensional ℝ H) {P : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) {N : ℝ → Measure H} (hN : IsCenteredGaussianLayers P N)
    {α : ℝ} (hα : 0 < α) :
    (gaussianMixture N α).IsOpenPosMeasure := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_homogeneous_mixture_v, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:homogeneous-mixture]** Homogeneous Gaussian mixture.  Homogeneity:
`(D_ω)_# ν_α = |ω|^{-α} ν_α` for `ω ≠ 0`. -/
theorem lem_homogeneous_mixture_v (hH : ¬ FiniteDimensional ℝ H) {P : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) {N : ℝ → Measure H} (hN : IsCenteredGaussianLayers P N)
    {α : ℝ} (hα : 0 < α) :
    IsHomogeneous α (gaussianMixture N α) := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_homogeneous_mixture_vi, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:homogeneous-mixture]** Homogeneous Gaussian mixture.  The integrated form of
homogeneity: `∫ F(ωa) ν_α(da) = |ω|^{-α} ∫ F dν_α` for every nonnegative Borel `F`. -/
theorem lem_homogeneous_mixture_vi (hH : ¬ FiniteDimensional ℝ H) {P : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) {N : ℝ → Measure H} (hN : IsCenteredGaussianLayers P N)
    {α : ℝ} (hα : 0 < α) :
    ∀ ω : ℝ, ω ≠ 0 → ∀ F : H → ℝ≥0∞, Measurable F →
      ∫⁻ a, F (ω • a) ∂gaussianMixture N α =
        ENNReal.ofReal (|ω| ^ (-α)) * ∫⁻ ξ, F ξ ∂gaussianMixture N α := by

Status: verified by comparator.

8.3.2. Definition 3.2 — Admissible analysis filter (def:admissible-filter)🔗

Blueprint node: Definition 2.2.2. Status: verified (its Lean theorem is verified).

Formalization note. ρ : SchwartzMap ℝ ℝ; 0 < C < ∞ is integrability plus positivity. IsBandPass includes ρ ≠ 0 (a band-pass filter is admissible, hence nonzero), which the claim 'admissible for every α > 0' (def_admissible_filter) needs.

OperatorRidgelet.IsAdmissible: definition in the library (structure in OperatorRidgelet/Transform/Defs.lean); see the Lean panel of the Blueprint node above.

OperatorRidgelet.admissibilityConst: definition in the library (def in OperatorRidgelet/Transform/Defs.lean); see the Lean panel of the Blueprint node above.

OperatorRidgelet.IsBandPass: definition in the library (structure in OperatorRidgelet/Transform/Defs.lean); see the Lean panel of the Blueprint node above.

OperatorRidgelet.crossAdmissibilityConst: definition in the library (def in OperatorRidgelet/Transform/Defs.lean); see the Lean panel of the Blueprint node above.

OperatorRidgelet.Paper.def_admissible_filter, theorem in Challenge/Transform.lean:

/-- **Definition [def:admissible-filter]** Admissible analysis filter.  A band-pass filter is
`α`-admissible for every `α > 0`. -/
theorem def_admissible_filter (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ) :
    ∀ α : ℝ, 0 < α → IsAdmissible α ρ := by

Status: verified by comparator.

8.3.3. Definition 3.3 — Gaussian-weighted ridgelet transform (def:ridgelet-analysis)🔗

Blueprint node: Definition 2.2.3. Status: defined (definitions only, nothing for comparator to check).

Formalization note. Defined for a general input measure μ (μ_Q is the instance IsCenteredGaussian Q μ); 𝒢_μ f is gaussFourier.

OperatorRidgelet.ridgelet: definition in the library (def in OperatorRidgelet/Transform/Defs.lean); see the Lean panel of the Blueprint node above.

OperatorRidgelet.parameterMeasure: definition in the library (def in OperatorRidgelet/Transform/Defs.lean); see the Lean panel of the Blueprint node above.

OperatorRidgelet.gaussFourier: definition in the library (def in OperatorRidgelet/Transform/Defs.lean); see the Lean panel of the Blueprint node above.

8.3.4. Lemma 3.4 — Fourier-slice identity (lem:fourier-slice)🔗

Blueprint node: Lemma 2.2.4. Status: verified (all 5 Lean theorems verified).

Formalization note. Stated for a general probability measure μ, as Theorem H.1 asserts; parts: bounded, jointly continuous, L¹ bound (with integrability), L² bound (with square integrability), Fourier-slice identity via biasFourier.

OperatorRidgelet.Paper.lem_fourier_slice_i, theorem in Challenge/Transform.lean:

omit [CompleteSpace H] [SecondCountableTopology H] [BorelSpace H] in
/-- **Lemma [lem:fourier-slice]** Fourier-slice identity.  `R_ρ f` is bounded on `H × ℝ`. -/
theorem lem_fourier_slice_i (μ : Measure H) [IsProbabilityMeasure μ] (ρ : SchwartzMap ℝ ℝ)
    (f : H → ℂ) (hf : Integrable f μ) :
    ∃ M : ℝ, ∀ p : H × ℝ, ‖ridgelet μ ρ f p‖ ≤ M := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_fourier_slice_ii, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:fourier-slice]** Fourier-slice identity.  `R_ρ f` is jointly continuous on
`H × ℝ`. -/
theorem lem_fourier_slice_ii (μ : Measure H) [IsProbabilityMeasure μ] (ρ : SchwartzMap ℝ ℝ)
    (f : H → ℂ) (hf : Integrable f μ) :
    Continuous (ridgelet μ ρ f) := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_fourier_slice_iii, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:fourier-slice]** Fourier-slice identity.  For every direction `a`, the bias
function `R_ρ f (a, ·)` is integrable with `‖R_ρ f(a,·)‖_{L¹} ≤ ‖f‖_{L¹(μ)} ‖ρ‖_{L¹}`. -/
theorem lem_fourier_slice_iii (μ : Measure H) [IsProbabilityMeasure μ] (ρ : SchwartzMap ℝ ℝ)
    (f : H → ℂ) (hf : Integrable f μ) :
    ∀ a : H, Integrable (fun c : ℝ => ridgelet μ ρ f (a, c)) ∧
      ∫ c : ℝ, ‖ridgelet μ ρ f (a, c)‖ ≤ (∫ x, ‖f x‖ ∂μ) * ∫ t : ℝ, ‖ρ t‖ := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_fourier_slice_iv, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:fourier-slice]** Fourier-slice identity.  If moreover `f ∈ L²(μ)`, then for every
direction `a` the bias function is square integrable with
`‖R_ρ f(a,·)‖²_{L²} ≤ ‖f‖²_{L²(μ)} ‖ρ‖²_{L²}`. -/
theorem lem_fourier_slice_iv (μ : Measure H) [IsProbabilityMeasure μ] (ρ : SchwartzMap ℝ ℝ)
    (f : H → ℂ) (hf : Integrable f μ) (hf₂ : MemLp f 2 μ) :
    ∀ a : H, MemLp (fun c : ℝ => ridgelet μ ρ f (a, c)) 2 volume ∧
      ∫ c : ℝ, ‖ridgelet μ ρ f (a, c)‖ ^ 2 ≤ (∫ x, ‖f x‖ ^ 2 ∂μ) * ∫ t : ℝ, ‖ρ t‖ ^ 2 := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_fourier_slice_v, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:fourier-slice]** Fourier-slice identity.  The partial Fourier transform in the
bias is `\widehat{R_ρ f}(a,ω) = ρ̂(ω) 𝒢_μ f(-ωa)`. -/
theorem lem_fourier_slice_v (μ : Measure H) [IsProbabilityMeasure μ] (ρ : SchwartzMap ℝ ℝ)
    (f : H → ℂ) (hf : Integrable f μ) :
    ∀ (a : H) (ω : ℝ),
      biasFourier (ridgelet μ ρ f) a ω = filterFourier ρ ω * gaussFourier μ f (-(ω • a)) := by

Status: verified by comparator.

8.3.5. Definition 3.5 — The coefficient operator (def:spectral-coefficient)🔗

Blueprint node: Definition 2.2.5. Status: verified (its Lean theorem is verified).

Formalization note. W_ρ G is the element of L²(λ) whose partial bias Fourier transform is ρ̂(ω)G(-ωa), characterized by Parseval against Schwartz test functions together with square integrability along ν-a.e. ray (HasBiasFourier), junk 0 if none; def_spectral_coefficient is the L² formula claim (λ-a.e. equality with coefficientFormula).

OperatorRidgelet.HasBiasFourier: definition in the library (structure in OperatorRidgelet/Transform/Defs.lean); see the Lean panel of the Blueprint node above.

OperatorRidgelet.spectralCoefficient: definition in the library (def in OperatorRidgelet/Transform/Defs.lean); see the Lean panel of the Blueprint node above.

OperatorRidgelet.coefficientFormula: definition in the library (def in OperatorRidgelet/Transform/Defs.lean); see the Lean panel of the Blueprint node above.

OperatorRidgelet.Paper.def_spectral_coefficient, theorem in Challenge/Transform.lean:

/-- **Definition [def:spectral-coefficient]** The coefficient operator.  For
`G ∈ L²(ν)` the coefficient `W_ρ G` is given by the explicit formula
`γ_G(a,c) = (2π)⁻¹ ∫ ρ̂(ω) G(-ωa) e^{iωc} dω`, `λ`-almost everywhere. -/
theorem def_spectral_coefficient {α : ℝ} (hα : 0 < α) (ν : Measure H) [SigmaFinite ν]
    (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) (G : H → ℂ)
    (hG : Measurable G) (hG₂ : MemLp G 2 ν) :
    (spectralCoefficient ν ρ G : H × ℝ → ℂ) =ᵐ[parameterMeasure ν] coefficientFormula ρ G := by

Status: verified by comparator.

8.3.6. Lemma 3.6 — The backprojection is the adjoint coefficient operator (lem:coefficient-adjoint)🔗

Blueprint node: Lemma 2.2.8. Status: verified (all 3 Lean theorems verified).

OperatorRidgelet.Paper.lem_coefficient_adjoint_i, theorem in Challenge/Revision.lean:

omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Lemma [lem:coefficient-adjoint]** The coefficient operator has the bounded ray-average
adjoint and the scaled left-inverse identity. -/
theorem lem_coefficient_adjoint_i (ν : Measure H) [SigmaFinite ν] {α : ℝ}
    (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
    (hρ : IsAdmissible α ρ) :
    ∃ W : Lp Y 2 ν →L[ℂ] Lp Y 2 (parameterMeasure ν),
      (∀ F, W F = spectralCoefficientVec ν ρ F) ∧
      (∀ γ, W.adjoint γ = backprojectionLpVec α ν ρ γ) ∧
      ‖W‖ ≤ Real.sqrt (admissibilityConst α ρ) ∧
      (∀ γ : Lp Y 2 (parameterMeasure ν), ‖backprojectionLpVec α ν ρ γ‖ ≤
        Real.sqrt (admissibilityConst α ρ) * ‖γ‖) ∧
      ∀ F, W.adjoint (W F) = (admissibilityConst α ρ : ℂ) • F := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_coefficient_adjoint_ii, theorem in Challenge/Revision.lean:

omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Lemma [lem:coefficient-adjoint]** The ray-average integral is absolutely convergent a.e. -/
theorem lem_coefficient_adjoint_ii (ν : Measure H) [SigmaFinite ν] {α : ℝ}
    (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ)
    (γ : Lp Y 2 (parameterMeasure ν)) (Φ : H → ℝ → Y)
    (hΦ : StronglyMeasurable (Function.uncurry Φ)) (hB : HasBiasFourierVec ν γ Φ) :
    ∀ᵐ ξ ∂ν, Integrable fun ω : ℝ =>
      ((starRingEnd ℂ) (filterFourier ρ ω) * ((|ω| ^ (-α) : ℝ) : ℂ)) •
        Φ (-(ω⁻¹ • ξ)) ω := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_coefficient_adjoint_iii, theorem in Challenge/Revision.lean:

omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Lemma [lem:coefficient-adjoint]** Every measurable Fourier representative gives Λ. -/
theorem lem_coefficient_adjoint_iii (ν : Measure H) [SigmaFinite ν] {α : ℝ}
    (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
    (γ : Lp Y 2 (parameterMeasure ν)) (Φ : H → ℝ → Y)
    (hΦ : StronglyMeasurable (Function.uncurry Φ)) (hB : HasBiasFourierVec ν γ Φ) :
    backprojectionVec α ν ρ γ =ᵐ[ν] backprojectionOfVec α ρ Φ := by

Status: verified by comparator.

8.3.7. Definition 3.7 — The Hilbert space \(\cE_\alpha\) (def:spectral-space)🔗

Blueprint node: Definition 2.3.1. Status: defined (definitions only, nothing for comparator to check).

Formalization note. 𝓔_α is represented by 𝒦_α = spectralRange (the closure of 𝒢_μ(𝒟) in L²(ν)) rather than by an abstract completion, since the positivity of the spectral form (Lemma 3.8) cannot enter a definition; U_α is spectralEmbed, the identity of 𝒦_α on the completion.

OperatorRidgelet.spectralCore: definition in the library (def in OperatorRidgelet/Transform/Defs.lean); see the Lean panel of the Blueprint node above.

OperatorRidgelet.spectralInner: definition in the library (def in OperatorRidgelet/Transform/Defs.lean); see the Lean panel of the Blueprint node above.

OperatorRidgelet.spectralRange: definition in the library (def in OperatorRidgelet/Transform/Defs.lean); see the Lean panel of the Blueprint node above.

OperatorRidgelet.gaussFourierLp: definition in the library (def in OperatorRidgelet/Transform/Defs.lean); see the Lean panel of the Blueprint node above.

OperatorRidgelet.spectralEmbed: definition in the library (def in OperatorRidgelet/Transform/Defs.lean); see the Lean panel of the Blueprint node above.

8.3.8. Lemma 3.8 — Positivity and the unitary extension (lem:spectral-unitary)🔗

Blueprint node: Lemma 2.3.2. Status: verified (all 3 Lean theorems verified).

Formalization note. Stated for abstract (μ, ν) with ν σ-finite of full support; parts: positive definiteness, isometry of 𝒢_μ into 𝒦 (Mathlib's inner product is conjugate linear in the first slot, hence ⟨Uf,Ug⟩ = ⟨g,f⟩_𝓔), density of the image (the unitary extension is the identity of 𝒦 in this representation).

OperatorRidgelet.Paper.lem_spectral_unitary_i, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:spectral-unitary]** Positivity and the unitary extension.  The spectral form is
positive definite on `𝒟`: `⟨f,f⟩_𝓔 = 0` forces `f = 0` in `L²(μ)`. -/
theorem lem_spectral_unitary_i (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
    [ν.IsOpenPosMeasure] :
    ∀ f : Lp ℂ 2 μ, f ∈ spectralCore μ ν → spectralInner μ ν f f = 0 → f = 0 := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_spectral_unitary_ii, theorem in Challenge/Transform.lean:

omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Lemma [lem:spectral-unitary]** Positivity and the unitary extension.  `𝒢_μ` is an
isometry from `(𝒟, ⟨·,·⟩_𝓔)` into `𝒦`: the `L²(ν)` inner product of `U f` and `U g` (which in
Mathlib is conjugate linear in the first argument) is `⟨g,f⟩_𝓔`. -/
theorem lem_spectral_unitary_ii (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
    [ν.IsOpenPosMeasure] :
    ∀ f g : spectralCore μ ν,
      inner ℂ (spectralEmbed μ ν f) (spectralEmbed μ ν g) =
        spectralInner μ ν ((g : Lp ℂ 2 μ) : H → ℂ) ((f : Lp ℂ 2 μ) : H → ℂ) := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_spectral_unitary_iii, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:spectral-unitary]** Positivity and the unitary extension.  The image of `𝒟`
under `𝒢_μ` is dense in `𝒦`, so the isometry extends uniquely to a unitary `U_α : 𝓔_α → 𝒦_α`
(the identity of `𝒦` in this representation). -/
theorem lem_spectral_unitary_iii (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
    [ν.IsOpenPosMeasure] :
    Dense (Set.range (spectralEmbed μ ν)) := by

Status: verified by comparator.

8.3.9. Lemma 3.9 — Gaussian decay with polynomial weights (lem:gaussian-decay)🔗

Blueprint node: Lemma 2.3.3. Status: verified (all 2 Lean theorems verified).

Formalization note. dim H = ∞ (the standing assumption under which ν_α is defined) is explicit; in part (ii) the exponent p is allowed to be 0 (0 ≤ p), which the proof of ex:core-elements uses.

OperatorRidgelet.Paper.lem_gaussian_decay_i, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:gaussian-decay]** Gaussian decay with polynomial weights.  For `t > 0` and every
integer `m ≥ 0`, `∫ ‖ξ‖^{2m} e^{-t⟨Qξ,ξ⟩} ν_α(dξ) < ∞`. -/
theorem lem_gaussian_decay_i (hH : ¬ FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) (hQ : IsTraceClassCovariance Q) {N : ℝ → Measure H}
    (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) :
    ∀ t : ℝ, 0 < t → ∀ m : ℕ,
      Integrable (fun ξ : H => ‖ξ‖ ^ (2 * m) * Real.exp (-t * ⟪Q ξ, ξ⟫))
        (gaussianMixture N α) := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_gaussian_decay_ii, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:gaussian-decay]** Gaussian decay with polynomial weights.  If `f ∈ L²(μ_Q)` and
`|𝒢_Q f(ξ)| ≤ C (1+‖ξ‖)^p e^{-t⟨Qξ,ξ⟩/2}`, then `f ∈ 𝒟_α` for every `α > 0`. -/
theorem lem_gaussian_decay_ii (hH : ¬ FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) (hQ : IsTraceClassCovariance Q) {N : ℝ → Measure H}
    (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) (μ : Measure H)
    [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Q μ) (f : Lp ℂ 2 μ) (C p t : ℝ)
    (hC : 0 < C) (hp : 0 ≤ p) (ht : 0 < t)
    (hdecay : ∀ ξ : H,
      ‖gaussFourier μ f ξ‖ ≤ C * (1 + ‖ξ‖) ^ p * Real.exp (-t * ⟪Q ξ, ξ⟫ / 2)) :
    f ∈ spectralCore μ (gaussianMixture N α) := by

Status: verified by comparator.

8.3.10. Example 3.10 — Elements of \(\cD_\alpha\) (ex:core-elements)🔗

Blueprint node: Proposition 2.3.4. Status: verified (all 5 Lean theorems verified).

Formalization note. Claims i–iii (in Paper.Transform) are the first sentence: 𝒢_Q 1, 1 ∈ 𝒟_α, 𝓔_α ≠ {0}. Claims iv (f_W ∈ 𝒟_α, with the hypotheses of ex:closed-form: W positive injective self-adjoint, S = Q^{1/2} as data with IsPositiveSqrt S Q, M = S W S with a summable trace) and v (the observables F_φ = ⟨ℱ(·),φ⟩ of the Gaussian-activation operator layers, under IsLayerData) are in Paper.Examples; membership of a function in 𝒟_α is MemSpectralCore μ ν f (f ∈ L²(μ) and 𝒢_μ f ∈ L²(ν)), related to the submodule spectralCore by memSpectralCore_iff.

OperatorRidgelet.Paper.ex_core_elements_i, theorem in Challenge/Transform.lean:

omit [CompleteSpace H] [SecondCountableTopology H] [BorelSpace H] in
/-- **Example [ex:core-elements]** Elements of `𝒟_α`.  The constant function has
`𝒢_Q 1 (ξ) = e^{-⟨Qξ,ξ⟩/2}`. -/
theorem ex_core_elements_i {Q : H →L[ℝ] H} (μ : Measure H) [IsProbabilityMeasure μ]
    (hμ : IsCenteredGaussian Q μ) :
    ∀ ξ : H, gaussFourier μ (fun _ => (1 : ℂ)) ξ = Complex.exp (-((⟪Q ξ, ξ⟫ / 2 : ℝ) : ℂ)) := by

Status: verified by comparator.

OperatorRidgelet.Paper.ex_core_elements_ii, theorem in Challenge/Transform.lean:

/-- **Example [ex:core-elements]** Elements of `𝒟_α`.  The constant function belongs to `𝒟_α`
for every `α > 0`. -/
theorem ex_core_elements_ii (hH : ¬ FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) (hQ : IsTraceClassCovariance Q) {N : ℝ → Measure H}
    (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) (μ : Measure H)
    [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Q μ) :
    MemLp.toLp (fun _ : H => (1 : ℂ)) (memLp_const 1) ∈ spectralCore μ (gaussianMixture N α) := by

Status: verified by comparator.

OperatorRidgelet.Paper.ex_core_elements_iii, theorem in Challenge/Transform.lean:

/-- **Example [ex:core-elements]** Elements of `𝒟_α`.  Consequently `𝓔_α ≠ {0}`. -/
theorem ex_core_elements_iii (hH : ¬ FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) (hQ : IsTraceClassCovariance Q) {N : ℝ → Measure H}
    (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) (μ : Measure H)
    [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Q μ) :
    spectralRange μ (gaussianMixture N α) ≠ ⊥ := by

Status: verified by comparator.

OperatorRidgelet.Paper.ex_core_elements_iv, theorem in Challenge/Examples.lean:

/-- **Example [ex:core-elements]** Elements of `𝒟_α`.  The non-cylindrical Gaussian target
`f_W` of Example `ex:closed-form` belongs to `𝒟_α` for every `α > 0`. -/
theorem ex_core_elements_iv (hH : ¬ FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) (hQ : IsTraceClassCovariance Q) {N : ℝ → Measure H}
    (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) (μ : Measure H)
    [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Q μ) (W S : H →L[ℝ] H)
    (hW : IsSelfAdjoint W) (hW0 : ∀ x, 0 ≤ ⟪W x, x⟫) (hWi : Function.Injective W)
    (hS : IsPositiveSqrt S Q) (hM : HasSummableTrace (S * W * S)) :
    MemSpectralCore μ (gaussianMixture N α) (gaussianTarget W) := by

Status: verified by comparator.

OperatorRidgelet.Paper.ex_core_elements_v, theorem in Challenge/Examples.lean:

/-- **Example [ex:core-elements]** Elements of `𝒟_α`.  The components `F_φ` of the
neural-operator layers with Gaussian activation of Example `ex:operator-layer` belong to `𝒟_α`
for every `α > 0`. -/
theorem ex_core_elements_v (hH : ¬ FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) (hQ : IsTraceClassCovariance Q) {N : ℝ → Measure H}
    (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) (μ : Measure H)
    [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Q μ) {Y : Type*} [NormedAddCommGroup Y]
    [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y] {Ω : Type*}
    [MeasurableSpace Ω] (m : Measure Ω) [IsFiniteMeasure m] (a : Ω → H) (b : Ω → Y)
    (hL : IsLayerData m a b) (φ : Y) :
    MemSpectralCore μ (gaussianMixture N α) (layerObservable m a b gaussianFun φ) := by

Status: verified by comparator.

8.3.11. Theorem 3.11 — Plancherel identity and injectivity (thm:B)🔗

Blueprint node: Theorem 2.4.2. Status: verified (all 7 Lean theorems verified).

Formalization note. Gaussian case with explicit hypotheses (IsCenteredGaussian Q μ, IsCenteredGaussianLayers P N, P, Q trace-class covariances, dim H = ∞); (i) split into membership in L²(λ_α) and the identity, (ii) into unique extension, norm identity, closed range, R_ρ = W_ρ U_α; the same claims for the abstract pair are thm:general-weights.

OperatorRidgelet.Paper.thm_B_i_a, theorem in Challenge/Transform.lean:

/-- **Theorem [thm:B]** Plancherel identity and injectivity.  For `f ∈ 𝒟_α` and an
`α`-admissible `ρ`, the transform `R_ρ f` belongs to `L²(λ_α)`. -/
theorem thm_B_i_a (hH : ¬ FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) (hQ : IsTraceClassCovariance Q) {N : ℝ → Measure H}
    (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) (μ : Measure H)
    [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
    (hρ : IsAdmissible α ρ) (f : Lp ℂ 2 μ) (hf : f ∈ spectralCore μ (gaussianMixture N α)) :
    MemLp (ridgelet μ ρ f) 2 (parameterMeasure (gaussianMixture N α)) := by

Status: verified by comparator.

OperatorRidgelet.Paper.thm_B_i_b, theorem in Challenge/Transform.lean:

/-- **Theorem [thm:B]** Plancherel identity and injectivity.  The Plancherel identity
`⟨R_{ρ₁} f, R_{ρ₂} g⟩_{L²(λ_α)} = C^{(α)}_{ρ₁,ρ₂} ⟨f,g⟩_{𝓔_α}` for `f, g ∈ 𝒟_α`. -/
theorem thm_B_i_b (hH : ¬ FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) (hQ : IsTraceClassCovariance Q) {N : ℝ → Measure H}
    (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) (μ : Measure H)
    [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Q μ) (ρ₁ ρ₂ : SchwartzMap ℝ ℝ)
    (hρ₁ : IsAdmissible α ρ₁) (hρ₂ : IsAdmissible α ρ₂) (f g : Lp ℂ 2 μ)
    (hf : f ∈ spectralCore μ (gaussianMixture N α))
    (hg : g ∈ spectralCore μ (gaussianMixture N α)) :
    ∫ p, ridgelet μ ρ₁ f p * (starRingEnd ℂ) (ridgelet μ ρ₂ g p)
        ∂parameterMeasure (gaussianMixture N α) =
      crossAdmissibilityConst α ρ₁ ρ₂ * spectralInner μ (gaussianMixture N α) f g := by

Status: verified by comparator.

OperatorRidgelet.Paper.thm_B_ii_a, theorem in Challenge/Transform.lean:

/-- **Theorem [thm:B]** Plancherel identity and injectivity.  An `α`-admissible `ρ` determines a
unique bounded extension `R_ρ : 𝓔_α → L²(λ_α)` of `f ↦ R_ρ f` from `𝒟_α`. -/
theorem thm_B_ii_a (hH : ¬ FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) (hQ : IsTraceClassCovariance Q) {N : ℝ → Measure H}
    (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) (μ : Measure H)
    [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
    (hρ : IsAdmissible α ρ) :
    ∃! R : spectralRange μ (gaussianMixture N α) →L[ℂ]
        Lp ℂ 2 (parameterMeasure (gaussianMixture N α)),
      ∀ f : spectralCore μ (gaussianMixture N α),
        (R (spectralEmbed μ (gaussianMixture N α) f) : H × ℝ → ℂ)
          =ᵐ[parameterMeasure (gaussianMixture N α)] ridgelet μ ρ f := by

Status: verified by comparator.

OperatorRidgelet.Paper.thm_B_ii_b, theorem in Challenge/Transform.lean:

/-- **Theorem [thm:B]** Plancherel identity and injectivity.  The extension satisfies
`‖R_ρ f‖² = C^{(α)}_ρ ‖f‖²_{𝓔_α}`. -/
theorem thm_B_ii_b (hH : ¬ FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) (hQ : IsTraceClassCovariance Q) {N : ℝ → Measure H}
    (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) (μ : Measure H)
    [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
    (hρ : IsAdmissible α ρ)
    (R : spectralRange μ (gaussianMixture N α) →L[ℂ]
      Lp ℂ 2 (parameterMeasure (gaussianMixture N α)))
    (hR : ∀ f : spectralCore μ (gaussianMixture N α),
      (R (spectralEmbed μ (gaussianMixture N α) f) : H × ℝ → ℂ)
        =ᵐ[parameterMeasure (gaussianMixture N α)] ridgelet μ ρ f) :
    ∀ G : spectralRange μ (gaussianMixture N α), ‖R G‖ ^ 2 = admissibilityConst α ρ * ‖G‖ ^ 2 := by

Status: verified by comparator.

OperatorRidgelet.Paper.thm_B_ii_c, theorem in Challenge/Transform.lean:

/-- **Theorem [thm:B]** Plancherel identity and injectivity.  The extension has closed range. -/
theorem thm_B_ii_c (hH : ¬ FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) (hQ : IsTraceClassCovariance Q) {N : ℝ → Measure H}
    (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) (μ : Measure H)
    [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
    (hρ : IsAdmissible α ρ)
    (R : spectralRange μ (gaussianMixture N α) →L[ℂ]
      Lp ℂ 2 (parameterMeasure (gaussianMixture N α)))
    (hR : ∀ f : spectralCore μ (gaussianMixture N α),
      (R (spectralEmbed μ (gaussianMixture N α) f) : H × ℝ → ℂ)
        =ᵐ[parameterMeasure (gaussianMixture N α)] ridgelet μ ρ f) :
    IsClosed (Set.range R) := by

Status: verified by comparator.

OperatorRidgelet.Paper.thm_B_ii_d, theorem in Challenge/Transform.lean:

/-- **Theorem [thm:B]** Plancherel identity and injectivity.  The extension factors as
`R_ρ = W_ρ U_α`: on `𝒦_α` it is the coefficient operator. -/
theorem thm_B_ii_d (hH : ¬ FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) (hQ : IsTraceClassCovariance Q) {N : ℝ → Measure H}
    (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) (μ : Measure H)
    [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
    (hρ : IsAdmissible α ρ)
    (R : spectralRange μ (gaussianMixture N α) →L[ℂ]
      Lp ℂ 2 (parameterMeasure (gaussianMixture N α)))
    (hR : ∀ f : spectralCore μ (gaussianMixture N α),
      (R (spectralEmbed μ (gaussianMixture N α) f) : H × ℝ → ℂ)
        =ᵐ[parameterMeasure (gaussianMixture N α)] ridgelet μ ρ f) :
    ∀ G : spectralRange μ (gaussianMixture N α),
      R G = spectralCoefficient (gaussianMixture N α) ρ
        ((G : Lp ℂ 2 (gaussianMixture N α)) : H → ℂ) := by

Status: verified by comparator.

OperatorRidgelet.Paper.thm_B_iii, theorem in Challenge/Transform.lean:

/-- **Theorem [thm:B]** Plancherel identity and injectivity.  Injectivity: if `ρ` is
`α`-admissible and `f ∈ L¹(μ_Q)`, then `R_ρ f = 0` `λ_α`-almost everywhere implies `f = 0`
`μ_Q`-almost everywhere. -/
theorem thm_B_iii (hH : ¬ FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) (hQ : IsTraceClassCovariance Q) {N : ℝ → Measure H}
    (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) (μ : Measure H)
    [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
    (hρ : IsAdmissible α ρ) (f : H → ℂ) (hf : Integrable f μ)
    (h : ridgelet μ ρ f =ᵐ[parameterMeasure (gaussianMixture N α)] 0) :
    f =ᵐ[μ] 0 := by

Status: verified by comparator.