Infinite-dimensional operator ridgelet transform

Formalization infrastructure🔗

This reference chapter records mathematical infrastructure used by the Lean proofs. It is separate from the manuscript's numbered exposition. Each statement below is proved; the links expose its Lean formulation and dependencies. Auxiliary definitions elsewhere in the Blueprint likewise have descriptive identifiers and are not additional manuscript results.

The formalization uses the bias coordinate c=-b; some statements carry the abstract input/direction measures used in the supporting proofs. The L^2 conclusion of Theorem 5.10 and the closed forms of the constants in Proposition 5.12 are recorded in weaker forms in the Lean statements. These distinctions are explained with the corresponding formal statements.

TheoremAux.15
uses 1used by 1✓L∃∀N

For an injective, positive, self-adjoint, trace-class P on a separable Hilbert space there is a family of Gaussian components \mathcal N(0,2sP), s>0, with characteristic functionals e^{-s\langle P\xi,\xi\rangle}: the Gaussian series X=\sum_j\sqrt{p_j}Z_je_j of Section 3, which converges in L^2(\Omega;H) and almost surely. Mathlib has the class of Gaussian measures but no constructor of a centred Gaussian measure with a prescribed trace-class covariance in infinite dimension.

Lean code for TheoremAux.15●1 theorem
  • theoremdefined in OperatorRidgelet/Transform/Infra.lean
    complete
    theorem OperatorRidgelet.exists_isCenteredGaussianLayers.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (P : H →L[ℝ] H) (hP : OperatorRidgelet.IsTraceClassCovariance P) :
  ∃ N, OperatorRidgelet.IsCenteredGaussianLayers P N
    theorem OperatorRidgelet.exists_isCenteredGaussianLayers.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (P : H →L[ℝ] H)
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P) :
  ∃ N,
    OperatorRidgelet.IsCenteredGaussianLayers
      P N
    Existence of the Gaussian components `𝒩(0,2sP)`, `s > 0`, for an injective, positive,
self-adjoint, trace-class `P`: the Gaussian series construction of Section 3.
TheoremAux.16
uses 1used by 1✓L∃∀N

For a positive operator, the trace \sum_i\langle Pe_i,e_i\rangle has the same value along every Hilbert basis. The Fredholm determinant \prod_i(1+m_i) of a positive trace-class operator has the same value along every orthonormal eigenbasis. Thus the chosen bases in traceOf and fredholmDet do not affect the Gaussian-target formulas. The trace is compared through the orthonormal eigenbasis supplied by its convergence; the multiplicity of a nonzero eigenvalue is identified with the trace of the projection onto its eigenspace.

Lean code for TheoremAux.16●2 theorems
  • theoremdefined in OperatorRidgelet/BasisIndependence.lean
    complete
    theorem OperatorRidgelet.traceOf_eq_traceAlong.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  {P : H →L[ℝ] H} (hP : IsSelfAdjoint P)
  (hpos : ∀ (x : H), 0 ≤ inner ℝ (P x) x)
  (h : OperatorRidgelet.HasSummableTrace P) {ι : Type u_2}
  (b : HilbertBasis ι ℝ H) :
  OperatorRidgelet.traceOf P = OperatorRidgelet.traceAlong b P
    theorem OperatorRidgelet.traceOf_eq_traceAlong.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] {P : H →L[ℝ] H}
  (hP : IsSelfAdjoint P)
  (hpos : ∀ (x : H), 0 ≤ inner ℝ (P x) x)
  (h :
    OperatorRidgelet.HasSummableTrace P)
  {ι : Type u_2}
  (b : HilbertBasis ι ℝ H) :
  OperatorRidgelet.traceOf P =
    OperatorRidgelet.traceAlong b P
    **The trace is the sum along every Hilbert basis.**  The basis chosen in the definition of
`traceOf` is immaterial: for a positive self-adjoint operator with summable trace,
`traceOf P = ∑ ⟪P e_i, e_i⟫` along any Hilbert basis.
  • theoremdefined in OperatorRidgelet/BasisIndependence.lean
    complete
    theorem OperatorRidgelet.fredholmDet_eq_fredholmDetAlong.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] {M : H →L[ℝ] H} (hM : IsSelfAdjoint M)
  (hpos : ∀ (x : H), 0 ≤ inner ℝ (M x) x)
  (htr : OperatorRidgelet.HasSummableTrace M)
  (hex : ∃ κ e' w', OperatorRidgelet.HasEigenbasis M e' w')
  {ι : Type u_2} {e : HilbertBasis ι ℝ H} {w : ι → ℝ}
  (he : OperatorRidgelet.HasEigenbasis M e w) :
  OperatorRidgelet.fredholmDet M = OperatorRidgelet.fredholmDetAlong e M
    theorem OperatorRidgelet.fredholmDet_eq_fredholmDetAlong.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] {M : H →L[ℝ] H}
  (hM : IsSelfAdjoint M)
  (hpos : ∀ (x : H), 0 ≤ inner ℝ (M x) x)
  (htr :
    OperatorRidgelet.HasSummableTrace M)
  (hex :
    ∃ κ e' w',
      OperatorRidgelet.HasEigenbasis M e'
        w')
  {ι : Type u_2} {e : HilbertBasis ι ℝ H}
  {w : ι → ℝ}
  (he :
    OperatorRidgelet.HasEigenbasis M e
      w) :
  OperatorRidgelet.fredholmDet M =
    OperatorRidgelet.fredholmDetAlong e M
    **The Fredholm determinant is the product along every orthonormal eigenbasis.**  The basis
chosen in the definition of `fredholmDet` is immaterial: for a positive self-adjoint operator
with summable trace, `fredholmDet M = ∏ (1 + ⟪M e_i, e_i⟫)` along any orthonormal eigenbasis.