8.7. Manuscript Section 7🔗

8.7.1. Example 7.1 — Closed-form transform and its filtered network (`ex:closed-form`)🔗

Blueprint node: Proposition 6.2.1. Status: verified (all 11 Lean theorems verified).

Formalization note. Standing hypotheses: W self-adjoint, ⟨Wx,x⟩ ≥ 0, injective; Q^{1/2} is data S with IsPositiveSqrt S Q; M = S * W * S with HasSummableTrace; f_W = gaussianTarget W, D = fredholmDet (S*W*S), κ_W = gaussianKappa S W = ⟨S (I+M)⁻¹ S ξ, ξ⟩ with Ring.inverse. i_a: 𝒢_Q f_W = D^{-1/2} e^{-κ_W/2}; i_b: R_ρ f_W(a,c) = D^{-1/2}(ρ*φ_{κ_W(a)})(c) with gaussianSmooth (convolution with Mathlib's gaussianReal 0 v, δ_0 for v = 0), stated for every (a,c); i_c: f_W ∈ 𝒟_α (MemSpectralCore); i_d: non-cylindricity for W of infinite rank (IsCylindrical allows any finite-rank linear L, continuous or not, as in the manuscript's definition). ii_a: G = 𝒢_Q f_W regular along rays for every frequency window of ρ; ii_b: T_α f_W is represented by g_G (frame-operator identity of thm:C(iii), for the element of 𝒟_α equal a.e. to f_W); ii_c: eq:filtered-gaussian-target with P^{1/2} as data R, S_W = gaussianTargetResolvent S W, Σ_s = mixtureLayerCovariance R S_W s, det(I + 2s P^{1/2} S_W P^{1/2}) = fredholmDet ((2s) • (R S_W R)), the s-integral over Ioi 0. iii: β is a tempered distribution that is a Lipschitz non-polynomial function b (IsTemperedFunction, LipschitzWith L b, ¬IsPolynomialFun b); iii_a: R_ρ f_W = γ_G pointwise; iii_b: ∫ (1+‖a‖²+|c|²)|R_ρ f_W| dλ_α < ∞ (finite variation and second moment); iii_c: S_β[R_ρ f_W λ_α] = C_{β,ρ} g_G (integralNetworkDensity, temperedAdmissibilityConst); iii_d: the rate eq:spectral-barron in the conventions of Section 6, exactly as thm_E_iv with γ = R_ρ f_W: the Bochner expectation over sampleLaw n (densityLaw λ_α γ) of ‖densitySampledNetwork β λ_α γ θ − C g_G‖_{C(K)} (compactSupNorm) is at most 8V/√n (|β(0)| + Lip(β) R_K M₂) with V = densityWeight λ_α γ, R_K = compactRadius K, M₂² = secondMoment (densityLaw λ_α γ), n ≥ 1 (the earlier local Examples.polarSample/normalizedLaw/supNormOn/compactRadius/secondMoment and the lower-integral form were replaced by the Sampling/Defs objects).

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

/-- **Example [ex:closed-form]** Closed-form transform and its filtered network.  For `W` bounded,
positive, injective, self-adjoint with `M = Q^{1/2} W Q^{1/2}` trace class,
`𝒢_Q f_W(ξ) = D^{-1/2} e^{-κ_W(ξ)/2}` with `D = det(I+M)`. -/
theorem ex_closed_form_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 μ) (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)) :
    ∀ ξ : H, gaussFourier μ (gaussianTarget W) ξ =
      (((Real.sqrt (fredholmDet (S * W * S)))⁻¹ : ℝ) : ℂ) *
        Complex.exp (-((gaussianKappa S W ξ / 2 : ℝ) : ℂ)) := by