8.12.1. Lemma E.1 — Gaussian integral of a quadratic exponential (lem:gaussian-quadratic)🔗

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

Formalization note. Σ (named Cov) is IsPositiveTraceClass (positive, self-adjoint, summable trace HasSummableTrace along a Hilbert basis; no injectivity; defined in Transform/Defs as the parent structure of IsTraceClassCovariance, which adds injectivity), S is self-adjoint with ⟨Sx,x⟩ ≥ 0, Σ^{1/2} is data R with IsPositiveSqrt R Σ, 𝒩(0,Σ) is IsCenteredGaussian Cov μ. Part i: M = R S R is trace class (the manuscript's 'which is trace class'); part ii: the integral identity with det(I+M) = fredholmDet (R * S * R) (the product ∏(1+m_i) along an orthonormal eigenbasis chosen through Classical.choose, basis independence being a separate proof obligation), det^{-1/2} = (√det)⁻¹, and ⟨Σ^{1/2}(I+M)⁻¹Σ^{1/2}x,x⟩ = resolventForm R (R*S*R) x with (I+M)⁻¹ = Ring.inverse (1 + M).

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

omit [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H] in
/-- **Lemma [lem:gaussian-quadratic]** Gaussian integral of a quadratic exponential.  For a
positive self-adjoint trace-class `Σ` and a bounded positive self-adjoint `S`, the operator
`M = Σ^{1/2} S Σ^{1/2}` is trace class. -/
theorem lem_gaussian_quadratic_i {Cov S R : H →L[ℝ] H} (hCov : IsPositiveTraceClass Cov)
    (hS : IsSelfAdjoint S) (hS0 : ∀ x, 0 ≤ ⟪S x, x⟫) (hR : IsPositiveSqrt R Cov) :
    HasSummableTrace (R * S * R) := by

Status: verified by comparator.

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

/-- **Lemma [lem:gaussian-quadratic]** Gaussian integral of a quadratic exponential.  With
`M = Σ^{1/2} S Σ^{1/2}`,
`∫ e^{i⟨x,ξ⟩ - ⟨Sξ,ξ⟩/2} 𝒩(0,Σ)(dξ) = det(I+M)^{-1/2} exp(-½⟨Σ^{1/2}(I+M)⁻¹Σ^{1/2}x, x⟩)`. -/
theorem lem_gaussian_quadratic_ii {Cov S R : H →L[ℝ] H} (hCov : IsPositiveTraceClass Cov)
    (hS : IsSelfAdjoint S) (hS0 : ∀ x, 0 ≤ ⟪S x, x⟫) (hR : IsPositiveSqrt R Cov)
    (μ : Measure H) [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Cov μ) (x : H) :
    ∫ ξ, Complex.exp ((⟪x, ξ⟫ : ℝ) * Complex.I - ((⟪S ξ, ξ⟫ / 2 : ℝ) : ℂ)) ∂μ =
      (((Real.sqrt (fredholmDet (R * S * R)))⁻¹ : ℝ) : ℂ) *
        Complex.exp (-((resolventForm R (R * S * R) x / 2 : ℝ) : ℂ)) := by

Status: verified by comparator.

8.12.2. Lemma E.2 — Absolute hinge representation of the Gaussian (lem:gaussian-hinge)🔗

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

Formalization note. φ = gaussianFun (Tempered/Defs), φ'' = gaussianActDeriv2 (the explicit formula (b²-1)e^{-b²/2}), (u-b)_+ = LeanRidgelet.relu (u - b). i_a: absolute convergence (Integrable) for each u; i_b: the identity; ii: ∫ (1+|b|^k)|φ''(b)| db < ∞ for every k.

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

/-- **Lemma [lem:gaussian-hinge]** Absolute hinge representation of the Gaussian.  For
`φ(u) = e^{-u²/2}` the integral `∫ (u-b)_+ φ''(b) db` converges absolutely for each `u`. -/
theorem lem_gaussian_hinge_i_a (u : ℝ) :
    Integrable fun b : ℝ => relu (u - b) * gaussianActDeriv2 b := by

Status: verified by comparator.

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

/-- **Lemma [lem:gaussian-hinge]** Absolute hinge representation of the Gaussian.  For
`φ(u) = e^{-u²/2}`, `φ(u) = ∫ (u-b)_+ φ''(b) db` for each `u`. -/
theorem lem_gaussian_hinge_i_b (u : ℝ) :
    ∫ b : ℝ, relu (u - b) * gaussianActDeriv2 b = gaussianFun u := by

Status: verified by comparator.

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

/-- **Lemma [lem:gaussian-hinge]** Absolute hinge representation of the Gaussian.
`∫ (1 + |b|^k) |φ''(b)| db < ∞` for every `k ≥ 0`. -/
theorem lem_gaussian_hinge_ii (k : ℕ) :
    Integrable fun b : ℝ => (1 + |b| ^ k) * |gaussianActDeriv2 b| := by

Status: verified by comparator.