Infinite-dimensional operator ridgelet transform

7.1. A Gaussian integral and a target with a closed-form transform🔗

DefinitionAux.10
uses 0
Used by 4
Reverse dependency previews
Preview
Example 7.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

These are the cylindricality and observation-map conventions used in the examples of Section 7.

A function f on H is cylindrical if f=\widetilde f\circ L for a linear map L:H\to\mathbb R^m, and a linear map has infinite rank when its range is not finite dimensional. The elementary obstruction: a target F cannot factor through an observation P if P(x)=P(y) but F(x)\ne F(y); in particular, if F separates 0 from a vector in the kernel of a linear P, then F is not cylindrical through P.

Lean code for DefinitionAux.10●5 declarations
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.IsCylindrical.{u_1, u_2} {H : Type u_1} {Y : Type u_2}
  [AddCommGroup H] [Module ℝ H] (f : H → Y) : Prop
    def OperatorRidgelet.IsCylindrical.{u_1, u_2}
  {H : Type u_1} {Y : Type u_2}
  [AddCommGroup H] [Module ℝ H]
  (f : H → Y) : Prop
    A function `f` on `H` is cylindrical if `f = f̃ ∘ L` for a finite-rank linear map `L`, here
a linear map `L : H → ℝ^m` (not assumed continuous).
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.HasInfiniteRank.{u_1, u_3} {H : Type u_1}
  [AddCommGroup H] [Module ℝ H] {F : Type u_3} [AddCommGroup F]
  [Module ℝ F] (L : H →ₗ[ℝ] F) : Prop
    def OperatorRidgelet.HasInfiniteRank.{u_1,
    u_3}
  {H : Type u_1} [AddCommGroup H]
  [Module ℝ H] {F : Type u_3}
  [AddCommGroup F] [Module ℝ F]
  (L : H →ₗ[ℝ] F) : Prop
    A linear map has infinite rank when its range is not finite dimensional.
  • defdefined in OperatorRidgelet/Cylindrical.lean
    complete
    def OperatorRidgelet.FactorsThrough.{u_1, u_2, u_3} {E : Type u_1}
  {Y : Type u_2} {Z : Type u_3} (F : E → Y) (P : E → Z) : Prop
    def OperatorRidgelet.FactorsThrough.{u_1, u_2,
    u_3}
  {E : Type u_1} {Y : Type u_2}
  {Z : Type u_3} (F : E → Y) (P : E → Z) :
  Prop
    A function `F` factors through an observation map `P`.
  • theoremdefined in OperatorRidgelet/Cylindrical.lean
    complete
    theorem OperatorRidgelet.not_factorsThrough_of_fibre_separation.{u_1, u_2, u_3}
  {E : Type u_1} {Y : Type u_2} {Z : Type u_3} {F : E → Y} {P : E → Z}
  {x y : E} (hP : P x = P y) (hF : F x ≠ F y) :
  ¬OperatorRidgelet.FactorsThrough F P
    theorem OperatorRidgelet.not_factorsThrough_of_fibre_separation.{u_1,
    u_2, u_3}
  {E : Type u_1} {Y : Type u_2}
  {Z : Type u_3} {F : E → Y} {P : E → Z}
  {x y : E} (hP : P x = P y)
  (hF : F x ≠ F y) :
  ¬OperatorRidgelet.FactorsThrough F P
    A function separating two points of one fibre cannot factor through the observation map.
  • theoremdefined in OperatorRidgelet/Cylindrical.lean
    complete
    theorem OperatorRidgelet.not_factorsThrough_linear_of_kernel_separation.{u_1,
    u_2, u_3, u_4}
  {𝕜 : Type u_1} {E : Type u_2} {Y : Type u_3} {Z : Type u_4}
  [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid Z]
  [Module 𝕜 Z] {F : E → Y} (P : E →ₗ[𝕜] Z) {x : E} (hx : x ∈ P.ker)
  (hF : F x ≠ F 0) : ¬OperatorRidgelet.FactorsThrough F ⇑P
    theorem OperatorRidgelet.not_factorsThrough_linear_of_kernel_separation.{u_1,
    u_2, u_3, u_4}
  {𝕜 : Type u_1} {E : Type u_2}
  {Y : Type u_3} {Z : Type u_4}
  [Semiring 𝕜] [AddCommMonoid E]
  [Module 𝕜 E] [AddCommMonoid Z]
  [Module 𝕜 Z] {F : E → Y} (P : E →ₗ[𝕜] Z)
  {x : E} (hx : x ∈ P.ker)
  (hF : F x ≠ F 0) :
  ¬OperatorRidgelet.FactorsThrough F ⇑P
    Separating zero from a kernel vector obstructs factorization through a linear map.
DefinitionAux.11
Statement uses 2
Statement dependency previews
Preview
Definition Aux.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 4
Reverse dependency previews
Preview
Definition Aux.12
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

These are the trace and determinant conventions for Lemma 7.1 and Example 7.2.

Mathlib has neither trace-class operators nor Fredholm determinants. The trace \operatorname{tr}P=\sum_i\langle Pe_i,e_i\rangle is taken along a Hilbert basis for which the sum converges; a positive trace-class operator is positive, self-adjoint, with summable trace; square roots Q^{1/2} are data S with S positive self-adjoint and S^2=Q; the Fredholm determinant \det(I+M)=\prod_i(1+m_i) is computed along an orthonormal eigenbasis of M; and (I+M)^{-1} enters through the quadratic form \langle S(I+M)^{-1}Sx,x\rangle.

Lean code for DefinitionAux.11●9 definitions
  • defdefined in OperatorRidgelet/Transform/Defs.lean
    complete
    def OperatorRidgelet.traceAlong.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {ι : Type u_2}
  (b : HilbertBasis ι ℝ H) (P : H →L[ℝ] H) : ℝ
    def OperatorRidgelet.traceAlong.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {ι : Type u_2}
  (b : HilbertBasis ι ℝ H)
  (P : H →L[ℝ] H) : ℝ
    The trace `∑ ⟪P e_i, e_i⟫` of `P` along the Hilbert basis `b`.
  • defdefined in OperatorRidgelet/Transform/Defs.lean
    complete
    def OperatorRidgelet.HasSummableTrace.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (P : H →L[ℝ] H) : Prop
    def OperatorRidgelet.HasSummableTrace.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  (P : H →L[ℝ] H) : Prop
    `P` is trace class in the sense of the manuscript: `∑ ⟪P e_i, e_i⟫` converges along some
Hilbert basis.
  • defdefined in OperatorRidgelet/Transform/Defs.lean
    complete
    def OperatorRidgelet.traceOf.{u_1} {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (P : H →L[ℝ] H) : ℝ
    def OperatorRidgelet.traceOf.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  (P : H →L[ℝ] H) : ℝ
    The trace `tr P = ∑ ⟪P e_i, e_i⟫`, along a Hilbert basis for which the sum converges (`0`
if there is none); for a positive operator the value does not depend on the basis.
  • structure(3 fields)defined in OperatorRidgelet/Transform/Defs.lean
    complete
    structure OperatorRidgelet.IsPositiveTraceClass.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  (P : H →L[ℝ] H) : Prop
    structure OperatorRidgelet.IsPositiveTraceClass.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] (P : H →L[ℝ] H) : Prop
    A positive, self-adjoint, trace-class operator: the hypothesis on `Σ` in Lemma
`lem:7.1`, and the covariance hypothesis `IsTraceClassCovariance` without
injectivity.

    Fields

    isSelfAdjoint : IsSelfAdjoint P
    `P` is self-adjoint. 
    inner_nonneg : ∀ (x : H), 0 ≤ inner ℝ (P x) x
    `P` is positive: `⟪P x, x⟫ ≥ 0`. 
    hasSummableTrace : OperatorRidgelet.HasSummableTrace P
    `P` is trace class: `∑ ⟪P e_j, e_j⟫ < ∞` along a Hilbert basis.
  • structure(3 fields)defined in OperatorRidgelet/Examples/Defs.lean
    complete
    structure OperatorRidgelet.IsPositiveSqrt.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  (S Q : H →L[ℝ] H) : Prop
    structure OperatorRidgelet.IsPositiveSqrt.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] (S Q : H →L[ℝ] H) :
  Prop
    `S` is the positive square root of `Q`: `S` is positive self-adjoint and `S² = Q`.

    Fields

    isSelfAdjoint : IsSelfAdjoint S
    `S` is self-adjoint. 
    inner_nonneg : ∀ (x : H), 0 ≤ inner ℝ (S x) x
    `S` is positive. 
    mul_self : S * S = Q
    `S * S = Q`.
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.HasEigenbasis.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {ι : Type u_2}
  (M : H →L[ℝ] H) (e : HilbertBasis ι ℝ H) (w : ι → ℝ) : Prop
    def OperatorRidgelet.HasEigenbasis.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {ι : Type u_2}
  (M : H →L[ℝ] H) (e : HilbertBasis ι ℝ H)
  (w : ι → ℝ) : Prop
    `e` is an orthonormal eigenbasis of `M` with eigenvalues `w`: `M e_i = w_i e_i`.
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.fredholmDetAlong.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {ι : Type u_2}
  (e : HilbertBasis ι ℝ H) (M : H →L[ℝ] H) : ℝ
    def OperatorRidgelet.fredholmDetAlong.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {ι : Type u_2}
  (e : HilbertBasis ι ℝ H)
  (M : H →L[ℝ] H) : ℝ
    The product `∏ (1 + ⟪M e_i, e_i⟫)` along the Hilbert basis `e`.
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.fredholmDet.{u_1} {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (M : H →L[ℝ] H) : ℝ
    def OperatorRidgelet.fredholmDet.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  (M : H →L[ℝ] H) : ℝ
    The Fredholm determinant `det(I + M)` of a (positive trace-class) operator `M`: the product
`∏ (1 + m_i)` over the eigenvalues, computed along an orthonormal eigenbasis of `M` (`1` if `M`
has none).
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.resolventForm.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (S M : H →L[ℝ] H)
  (x : H) : ℝ
    def OperatorRidgelet.resolventForm.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  (S M : H →L[ℝ] H) (x : H) : ℝ
    The quadratic form `⟪S (I + M)⁻¹ S x, x⟫`, with `(I + M)⁻¹ = Ring.inverse (1 + M)`.
DefinitionAux.12
Statement uses 3
Statement dependency previews
Preview
Definition Aux.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 4
Reverse dependency previews
Preview
Example 7.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

These are the Gaussian-target and activation definitions used in Sections 7.1 and 7.2, including Example 7.2.

The Gaussian activation \Phi(u)=\phi(u)=e^{-u^2/2} with \phi''(b)=(b^2-1)e^{-b^2/2}, the convolution (\rho*\phi_v)(c) with the centred Gaussian of variance v\ge0, the Gaussian target f_W(x)=e^{-\langle Wx,x\rangle/2}, and, for M=Q^{1/2}WQ^{1/2}, \kappa_W(\xi)=\langle Q^{1/2}(I+M)^{-1}Q^{1/2}\xi,\xi\rangle, S_W=Q^{1/2}(I+M)^{-1}Q^{1/2}, and \Sigma_s=2sP^{1/2}(I+2sP^{1/2}S_WP^{1/2})^{-1}P^{1/2}. Membership f\in\mathcal D_\alpha of a function (rather than of an L^2 class) means f\in L^2(\mu) and F_\mu f\in L^2(\nu), related to the submodule \mathcal D_\alpha by the stated lemmas.

Lean code for DefinitionAux.12●13 declarations
  • defdefined in OperatorRidgelet/Tempered/Defs.lean
    complete
    def OperatorRidgelet.gaussianFun (u : ℝ) : ℝ
    def OperatorRidgelet.gaussianFun (u : ℝ) : ℝ
    The Gaussian activation `u ↦ e^{-u²/2}`.
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.gaussianActDeriv2 (b : ℝ) : ℝ
    def OperatorRidgelet.gaussianActDeriv2
  (b : ℝ) : ℝ
    The second derivative `φ''(b) = (b² - 1) e^{-b²/2}` of the Gaussian activation
`φ = gaussianFun`.
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.gaussianSmooth (ρ : ℝ → ℝ) (v c : ℝ) : ℝ
    def OperatorRidgelet.gaussianSmooth
  (ρ : ℝ → ℝ) (v c : ℝ) : ℝ
    The convolution `(ρ * φ_v)(c) = ∫ ρ(c - t) 𝒩(0,v)(dt)` of a filter with the centred
one-dimensional Gaussian of variance `v ≥ 0` (`φ_0 = δ_0`).
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.gaussianTarget.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (W : H →L[ℝ] H)
  (x : H) : ℂ
    def OperatorRidgelet.gaussianTarget.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (W : H →L[ℝ] H)
  (x : H) : ℂ
    The Gaussian target `f_W(x) = e^{-⟨Wx,x⟩/2}` (`eq:gaussian-target`).
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.gaussianKappa.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (S W : H →L[ℝ] H)
  (ξ : H) : ℝ
    def OperatorRidgelet.gaussianKappa.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  (S W : H →L[ℝ] H) (ξ : H) : ℝ
    `κ_W(ξ) = ⟨Q^{1/2} (I + M)⁻¹ Q^{1/2} ξ, ξ⟩` with `M = Q^{1/2} W Q^{1/2}`, for `S = Q^{1/2}`
(`eq:gaussian-target`).
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.gaussianTargetResolvent.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (S W : H →L[ℝ] H) :
  H →L[ℝ] H
    def OperatorRidgelet.gaussianTargetResolvent.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  (S W : H →L[ℝ] H) : H →L[ℝ] H
    `S_W = Q^{1/2} (I + M)⁻¹ Q^{1/2}`, `M = Q^{1/2} W Q^{1/2}`, for `S = Q^{1/2}`
(`eq:filtered-gaussian-target`).
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.mixtureLayerCovariance.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (R T : H →L[ℝ] H)
  (s : ℝ) : H →L[ℝ] H
    def OperatorRidgelet.mixtureLayerCovariance.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  (R T : H →L[ℝ] H) (s : ℝ) : H →L[ℝ] H
    `Σ_s = 2s P^{1/2} (I + 2s P^{1/2} T P^{1/2})⁻¹ P^{1/2}` for `R = P^{1/2}` and `T = S_W`
(`eq:filtered-gaussian-target`).
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.MemSpectralCore.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (μ ν : MeasureTheory.Measure H) (f : H → ℂ) : Prop
    def OperatorRidgelet.MemSpectralCore.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  (f : H → ℂ) : Prop
    `f ∈ 𝒟_α` for a function `f`: `f ∈ L²(μ)` and `F_μ f ∈ L²(ν)`.
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.MemSpectralCoreVec.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (μ ν : MeasureTheory.Measure H) (f : H → Y) : Prop
    def OperatorRidgelet.MemSpectralCoreVec.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (μ ν : MeasureTheory.Measure H)
  (f : H → Y) : Prop
    `f ∈ 𝒟_α(Y)` for a `Y`-valued function `f`: `f ∈ L²(μ;Y)` and `F_μ f ∈ L²(ν;Y)`.
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.toLpOrZero.{u_1, u_2} {α : Type u_1} {E : Type u_2}
  [MeasurableSpace α] [NormedAddCommGroup E] (p : ENNReal)
  (μ : MeasureTheory.Measure α) (f : α → E) : ↥(MeasureTheory.Lp E p μ)
    def OperatorRidgelet.toLpOrZero.{u_1, u_2}
  {α : Type u_1} {E : Type u_2}
  [MeasurableSpace α]
  [NormedAddCommGroup E] (p : ENNReal)
  (μ : MeasureTheory.Measure α)
  (f : α → E) : ↥(MeasureTheory.Lp E p μ)
    The element of `L^p(μ)` represented by `f`, and `0` when `f ∉ L^p(μ)`.
  • theoremdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    theorem OperatorRidgelet.gaussFourier_congr_ae.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {μ : MeasureTheory.Measure H} {f g : H → ℂ} (h : f =ᵐ[μ] g) :
  OperatorRidgelet.gaussFourier μ f = OperatorRidgelet.gaussFourier μ g
    theorem OperatorRidgelet.gaussFourier_congr_ae.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  {μ : MeasureTheory.Measure H}
  {f g : H → ℂ} (h : f =ᵐ[μ] g) :
  OperatorRidgelet.gaussFourier μ f =
    OperatorRidgelet.gaussFourier μ g
    Almost-everywhere equal spectral densities define the same Gaussian Fourier target.
  • theoremdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    theorem OperatorRidgelet.toLp_mem_spectralCore_iff.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] {μ ν : MeasureTheory.Measure H}
  [MeasureTheory.IsFiniteMeasure μ] {f : H → ℂ}
  (hf : MeasureTheory.MemLp f 2 μ) :
  MeasureTheory.MemLp.toLp f hf ∈ OperatorRidgelet.spectralCore μ ν ↔
    MeasureTheory.MemLp (OperatorRidgelet.gaussFourier μ f) 2 ν
    theorem OperatorRidgelet.toLp_mem_spectralCore_iff.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  {μ ν : MeasureTheory.Measure H}
  [MeasureTheory.IsFiniteMeasure μ]
  {f : H → ℂ}
  (hf : MeasureTheory.MemLp f 2 μ) :
  MeasureTheory.MemLp.toLp f hf ∈
      OperatorRidgelet.spectralCore μ ν ↔
    MeasureTheory.MemLp
      (OperatorRidgelet.gaussFourier μ f)
      2 ν
    Passing a square-integrable density to `L²` preserves membership in the spectral core.
  • theoremdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    theorem OperatorRidgelet.memSpectralCore_iff.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] {μ ν : MeasureTheory.Measure H}
  [MeasureTheory.IsFiniteMeasure μ] {f : H → ℂ} :
  OperatorRidgelet.MemSpectralCore μ ν f ↔
    ∃ (hf : MeasureTheory.MemLp f 2 μ),
      MeasureTheory.MemLp.toLp f hf ∈ OperatorRidgelet.spectralCore μ ν
    theorem OperatorRidgelet.memSpectralCore_iff.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  {μ ν : MeasureTheory.Measure H}
  [MeasureTheory.IsFiniteMeasure μ]
  {f : H → ℂ} :
  OperatorRidgelet.MemSpectralCore μ ν f ↔
    ∃ (hf : MeasureTheory.MemLp f 2 μ),
      MeasureTheory.MemLp.toLp f hf ∈
        OperatorRidgelet.spectralCore μ ν
    The function-level spectral core agrees with membership of its `L²` representative.
Lemma7.1
Statement uses 2
Statement dependency previews
Preview
Definition Aux.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

Let \Sigma be a positive self-adjoint trace-class operator, S a bounded positive self-adjoint operator, and x\in H. Then M=\Sigma^{1/2}S\Sigma^{1/2} is trace class (i), and \int_He^{i\langle x,\xi\rangle-\langle S\xi,\xi\rangle/2}\,\mathcal N(0,\Sigma)(\mathrm d\xi)=\det(I+M)^{-1/2}\exp\bigl(-\tfrac12\langle\Sigma^{1/2}(I+M)^{-1}\Sigma^{1/2}x,x\rangle\bigr) (ii).

Lean code for Lemma7.1●2 theorems
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.lem_7_1_i.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  {Cov S R : H →L[ℝ] H}
  (hCov : OperatorRidgelet.IsPositiveTraceClass Cov)
  (hS : IsSelfAdjoint S) (hS0 : ∀ (x : H), 0 ≤ inner ℝ (S x) x)
  (hR : OperatorRidgelet.IsPositiveSqrt R Cov) :
  OperatorRidgelet.HasSummableTrace (R * S * R)
    theorem OperatorRidgelet.Paper.lem_7_1_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] {Cov S R : H →L[ℝ] H}
  (hCov :
    OperatorRidgelet.IsPositiveTraceClass
      Cov)
  (hS : IsSelfAdjoint S)
  (hS0 : ∀ (x : H), 0 ≤ inner ℝ (S x) x)
  (hR :
    OperatorRidgelet.IsPositiveSqrt R
      Cov) :
  OperatorRidgelet.HasSummableTrace
    (R * S * R)
    **Lemma [lem:7.1]** 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.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.lem_7_1_ii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Cov S R : H →L[ℝ] H}
  (hCov : OperatorRidgelet.IsPositiveTraceClass Cov)
  (hS : IsSelfAdjoint S) (hS0 : ∀ (x : H), 0 ≤ inner ℝ (S x) x)
  (hR : OperatorRidgelet.IsPositiveSqrt R Cov)
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Cov μ) (x : H) :
  ∫ (ξ : H),
      Complex.exp
        (↑(inner ℝ x ξ) * Complex.I - ↑(inner ℝ (S ξ) ξ / 2)) ∂μ =
    ↑(√(OperatorRidgelet.fredholmDet (R * S * R)))⁻¹ *
      Complex.exp
        (-↑(OperatorRidgelet.resolventForm R (R * S * R) x / 2))
    theorem OperatorRidgelet.Paper.lem_7_1_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Cov S R : H →L[ℝ] H}
  (hCov :
    OperatorRidgelet.IsPositiveTraceClass
      Cov)
  (hS : IsSelfAdjoint S)
  (hS0 : ∀ (x : H), 0 ≤ inner ℝ (S x) x)
  (hR :
    OperatorRidgelet.IsPositiveSqrt R Cov)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian
      Cov μ)
  (x : H) :
  ∫ (ξ : H),
      Complex.exp
        (↑(inner ℝ x ξ) * Complex.I -
          ↑(inner ℝ (S ξ) ξ / 2)) ∂μ =
    ↑(√(OperatorRidgelet.fredholmDet
              (R * S * R)))⁻¹ *
      Complex.exp
        (-↑(OperatorRidgelet.resolventForm
                R (R * S * R) x /
              2))
    **Lemma [lem:7.1]** 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⟩)`.
Proof for Lemma 7.1
uses 0

In an orthonormal eigenbasis (u_j) of M with eigenvalues m_j, the Gaussian series \xi=\sum_j\eta_j\Sigma^{1/2}u_j has law \mathcal N(0,\Sigma), \langle S\xi,\xi\rangle=\sum_jm_j\eta_j^2, and the expectation factorizes into one-dimensional Gaussian integrals (1+m_j)^{-1/2}e^{-x_j^2/(2(1+m_j))}.

Example7.2
Statement uses 2
Statement dependency previews
Preview
Definition Aux.10
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

Let W be bounded, positive, injective, self-adjoint with M=Q^{1/2}WQ^{1/2} trace class, f_W(x)=e^{-\langle Wx,x\rangle/2}, D=\det(I+M), and \kappa_W(\xi)=\langle Q^{1/2}(I+M)^{-1}Q^{1/2}\xi,\xi\rangle. For every \alpha>0 and band-pass \rho: (i) F_Qf_W(\xi)=D^{-1/2}e^{-\kappa_W(\xi)/2} and R_\rho f_W(a,c)=D^{-1/2}(\rho*\phi_{\kappa_W(a)})(c), so f_W\in\mathcal D_\alpha, and f_W is not cylindrical when W has infinite rank. (ii) G=F_Qf_W satisfies Definition 4.2 and T_\alpha f_W is represented by g_G(x)=D^{-1/2}\int_0^\infty\det(I+2sP^{1/2}S_WP^{1/2})^{-1/2}\exp(-\tfrac12\langle\Sigma_sx,x\rangle)\,s^{\alpha/2-1}\,\mathrm ds. (iii) For every real, globally Lipschitz, non-polynomial \beta, the coefficient measure \Gamma_G=\gamma_G\lambda_\alpha, with \gamma_G=R_\rho f_W, has finite total variation and second parameter moment, S_\beta[R_\rho f_W\lambda_\alpha]=C_{\beta,\rho}^{(\alpha)}g_G, and its sampled network converges at the rate N^{-1/2} in C(K).

Lean code for Example7.2●11 theorems
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_2_i_a.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (W S : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S)) (ξ : H) :
  OperatorRidgelet.gaussFourier μ (OperatorRidgelet.gaussianTarget W)
      ξ =
    ↑(√(OperatorRidgelet.fredholmDet (S * W * S)))⁻¹ *
      Complex.exp (-↑(OperatorRidgelet.gaussianKappa S W ξ / 2))
    theorem OperatorRidgelet.Paper.ex_7_2_i_a.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P Q : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (W S : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S))
  (ξ : H) :
  OperatorRidgelet.gaussFourier μ
      (OperatorRidgelet.gaussianTarget W)
      ξ =
    ↑(√(OperatorRidgelet.fredholmDet
              (S * W * S)))⁻¹ *
      Complex.exp
        (-↑(OperatorRidgelet.gaussianKappa
                S W ξ /
              2))
    **Example [ex:7.2]** Closed-form transform and integral representation of `T_α f_W`.
For `W` bounded,
positive, injective, self-adjoint with `M = Q^{1/2} W Q^{1/2}` trace class,
`F_Q f_W(ξ) = D^{-1/2} e^{-κ_W(ξ)/2}` with `D = det(I+M)`.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_2_i_b.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (W S : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S)) (p : H × ℝ) :
  OperatorRidgelet.ridgelet μ (⇑ρ) (OperatorRidgelet.gaussianTarget W)
      p =
    ↑((√(OperatorRidgelet.fredholmDet (S * W * S)))⁻¹ *
        OperatorRidgelet.gaussianSmooth (⇑ρ)
          (OperatorRidgelet.gaussianKappa S W p.1) p.2)
    theorem OperatorRidgelet.Paper.ex_7_2_i_b.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P Q : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (W S : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S))
  (p : H × ℝ) :
  OperatorRidgelet.ridgelet μ (⇑ρ)
      (OperatorRidgelet.gaussianTarget W)
      p =
    ↑((√(OperatorRidgelet.fredholmDet
              (S * W * S)))⁻¹ *
        OperatorRidgelet.gaussianSmooth
          (⇑ρ)
          (OperatorRidgelet.gaussianKappa
            S W p.1)
          p.2)
    **Example [ex:7.2]** Closed-form transform and integral representation of `T_α f_W`.
For every
band-pass `ρ`, `R_ρ f_W(a,c) = D^{-1/2} (ρ * φ_{κ_W(a)})(c)`.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_2_i_c.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (W S : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S)) :
  OperatorRidgelet.MemSpectralCore μ
    (OperatorRidgelet.gaussianMixture N α)
    (OperatorRidgelet.gaussianTarget W)
    theorem OperatorRidgelet.Paper.ex_7_2_i_c.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P Q : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (W S : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S)) :
  OperatorRidgelet.MemSpectralCore μ
    (OperatorRidgelet.gaussianMixture N α)
    (OperatorRidgelet.gaussianTarget W)
    **Example [ex:7.2]** Closed-form transform and integral representation of `T_α f_W`.
In particular
`f_W ∈ 𝒟_α` for every `α > 0`.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_2_i_d.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  (W : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x) (hWi : Function.Injective ⇑W)
  (hrank : OperatorRidgelet.HasInfiniteRank ↑W) :
  ¬OperatorRidgelet.IsCylindrical (OperatorRidgelet.gaussianTarget W)
    theorem OperatorRidgelet.Paper.ex_7_2_i_d.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] (W : H →L[ℝ] H)
  (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hrank :
    OperatorRidgelet.HasInfiniteRank ↑W) :
  ¬OperatorRidgelet.IsCylindrical
      (OperatorRidgelet.gaussianTarget W)
    **Example [ex:7.2]** Closed-form transform and integral representation of `T_α f_W`.
`f_W` is not
cylindrical when `W` has infinite rank.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_2_ii_a.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (W S : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S)) (I : Set ℝ) :
  OperatorRidgelet.IsFrequencyWindow (⇑ρ) I →
    OperatorRidgelet.IsRegularAlongRays
      (OperatorRidgelet.gaussianMixture N α) I
      (OperatorRidgelet.gaussFourier μ
        (OperatorRidgelet.gaussianTarget W))
    theorem OperatorRidgelet.Paper.ex_7_2_ii_a.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P Q : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (W S : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S))
  (I : Set ℝ) :
  OperatorRidgelet.IsFrequencyWindow (⇑ρ)
      I →
    OperatorRidgelet.IsRegularAlongRays
      (OperatorRidgelet.gaussianMixture N
        α)
      I
      (OperatorRidgelet.gaussFourier μ
        (OperatorRidgelet.gaussianTarget
          W))
    **Example [ex:7.2]** Closed-form transform and integral representation of `T_α f_W`.
For every
band-pass `ρ`, the density `G = F_Q f_W` is regular along rays.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_2_ii_b.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (W S : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S))
  (fW :
    ↥(OperatorRidgelet.spectralCore μ
        (OperatorRidgelet.gaussianMixture N α))) :
  ↑↑↑fW =ᵐ[μ] OperatorRidgelet.gaussianTarget W →
    ∀
      (g :
        ↥(OperatorRidgelet.spectralCore μ
            (OperatorRidgelet.gaussianMixture N α))),
      (OperatorRidgelet.frameOperator μ
            (OperatorRidgelet.gaussianMixture N α)
            (OperatorRidgelet.spectralEmbed μ
              (OperatorRidgelet.gaussianMixture N α) fW))
          (OperatorRidgelet.spectralEmbed μ
            (OperatorRidgelet.gaussianMixture N α) g) =
        ∫ (x : H),
          OperatorRidgelet.spectralTarget
              (OperatorRidgelet.gaussianMixture N α)
              (OperatorRidgelet.gaussFourier μ
                (OperatorRidgelet.gaussianTarget W))
              x *
            (starRingEnd ℂ) (↑↑↑g x) ∂μ
    theorem OperatorRidgelet.Paper.ex_7_2_ii_b.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P Q : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (W S : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S))
  (fW :
    ↥(OperatorRidgelet.spectralCore μ
        (OperatorRidgelet.gaussianMixture
          N α))) :
  ↑↑↑fW =ᵐ[μ]
      OperatorRidgelet.gaussianTarget W →
    ∀
      (g :
        ↥(OperatorRidgelet.spectralCore μ
            (OperatorRidgelet.gaussianMixture
              N α))),
      (OperatorRidgelet.frameOperator μ
            (OperatorRidgelet.gaussianMixture
              N α)
            (OperatorRidgelet.spectralEmbed
              μ
              (OperatorRidgelet.gaussianMixture
                N α)
              fW))
          (OperatorRidgelet.spectralEmbed
            μ
            (OperatorRidgelet.gaussianMixture
              N α)
            g) =
        ∫ (x : H),
          OperatorRidgelet.spectralTarget
              (OperatorRidgelet.gaussianMixture
                N α)
              (OperatorRidgelet.gaussFourier
                μ
                (OperatorRidgelet.gaussianTarget
                  W))
              x *
            (starRingEnd ℂ) (↑↑↑g x) ∂μ
    **Example [ex:7.2]** Closed-form transform and integral representation of `T_α f_W`.
The image
`T_α f_W` is represented by the bounded continuous function `g_G`, `G = F_Q f_W`:
`T_α f_W [g] = ∫ g_G(x) conj(g(x)) μ_Q(dx)` for `g ∈ 𝒟_α`.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_2_ii_c.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (W S R : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S))
  (hR : OperatorRidgelet.IsPositiveSqrt R P) (x : H) :
  OperatorRidgelet.spectralTarget (OperatorRidgelet.gaussianMixture N α)
      (OperatorRidgelet.gaussFourier μ
        (OperatorRidgelet.gaussianTarget W))
      x =
    ↑(√(OperatorRidgelet.fredholmDet (S * W * S)))⁻¹ *
      ∫ (s : ℝ) in Set.Ioi 0,
        ↑((√(OperatorRidgelet.fredholmDet
                    ((2 * s) •
                      (R *
                          OperatorRidgelet.gaussianTargetResolvent S W *
                        R))))⁻¹ *
              Real.exp
                (-inner ℝ
                      ((OperatorRidgelet.mixtureLayerCovariance R
                          (OperatorRidgelet.gaussianTargetResolvent S W)
                          s)
                        x)
                      x /
                  2) *
            s ^ (α / 2 - 1))
    theorem OperatorRidgelet.Paper.ex_7_2_ii_c.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P Q : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (W S R : H →L[ℝ] H)
  (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S))
  (hR :
    OperatorRidgelet.IsPositiveSqrt R P)
  (x : H) :
  OperatorRidgelet.spectralTarget
      (OperatorRidgelet.gaussianMixture N
        α)
      (OperatorRidgelet.gaussFourier μ
        (OperatorRidgelet.gaussianTarget
          W))
      x =
    ↑(√(OperatorRidgelet.fredholmDet
              (S * W * S)))⁻¹ *
      ∫ (s : ℝ) in Set.Ioi 0,
        ↑((√(OperatorRidgelet.fredholmDet
                    ((2 * s) •
                      (R *
                          OperatorRidgelet.gaussianTargetResolvent
                            S W *
                        R))))⁻¹ *
              Real.exp
                (-inner ℝ
                      ((OperatorRidgelet.mixtureLayerCovariance
                          R
                          (OperatorRidgelet.gaussianTargetResolvent
                            S W)
                          s)
                        x)
                      x /
                  2) *
            s ^ (α / 2 - 1))
    **Example [ex:7.2]** Closed-form transform and integral representation of `T_α f_W`.
With
`S_W = Q^{1/2}(I+M)⁻¹Q^{1/2}`, `R = P^{1/2}`, and
`Σ_s = 2s P^{1/2}(I + 2s P^{1/2} S_W P^{1/2})⁻¹ P^{1/2}`, the representing function is
`g_G(x) = D^{-1/2} ∫₀^∞ det(I + 2s P^{1/2} S_W P^{1/2})^{-1/2} exp(-½⟨Σ_s x,x⟩) s^{α/2-1} ds`
(`eq:filtered-gaussian-target`).
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_2_iii_a.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (W S : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S)) :
  OperatorRidgelet.ridgelet μ (⇑ρ) (OperatorRidgelet.gaussianTarget W) =
    OperatorRidgelet.coefficientFormula (⇑ρ)
      (OperatorRidgelet.gaussFourier μ
        (OperatorRidgelet.gaussianTarget W))
    theorem OperatorRidgelet.Paper.ex_7_2_iii_a.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P Q : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (W S : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S)) :
  OperatorRidgelet.ridgelet μ (⇑ρ)
      (OperatorRidgelet.gaussianTarget
        W) =
    OperatorRidgelet.coefficientFormula
      (⇑ρ)
      (OperatorRidgelet.gaussFourier μ
        (OperatorRidgelet.gaussianTarget
          W))
    **Example [ex:7.2]** Closed-form transform and integral representation of `T_α f_W`.
The ridgelet
coefficient of `f_W` is the coefficient `γ_G` of its density `G = F_Q f_W`:
`R_ρ f_W = γ_G`.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_2_iii_b.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (W S : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S)) :
  MeasureTheory.Integrable
    (fun p =>
      (1 + ‖p.1‖ ^ 2 + |p.2| ^ 2) *
        ‖OperatorRidgelet.ridgelet μ (⇑ρ)
            (OperatorRidgelet.gaussianTarget W) p‖)
    (OperatorRidgelet.parameterMeasure
      (OperatorRidgelet.gaussianMixture N α))
    theorem OperatorRidgelet.Paper.ex_7_2_iii_b.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P Q : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (W S : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S)) :
  MeasureTheory.Integrable
    (fun p =>
      (1 + ‖p.1‖ ^ 2 + |p.2| ^ 2) *
        ‖OperatorRidgelet.ridgelet μ (⇑ρ)
            (OperatorRidgelet.gaussianTarget
              W)
            p‖)
    (OperatorRidgelet.parameterMeasure
      (OperatorRidgelet.gaussianMixture N
        α))
    **Example [ex:7.2]** Closed-form transform and integral representation of `T_α f_W`.
The ridgelet
coefficient measure `(R_ρ f_W) λ_α` has finite total variation and second moment:
`∫ (1 + ‖a‖² + |c|²) |R_ρ f_W(a,c)| λ_α(da,dc) < ∞`.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_2_iii_c.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (W S : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S))
  (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
  (hβ : OperatorRidgelet.IsTemperedFunction β b) {L : NNReal}
  (hb : LipschitzWith L b) (hbp : ¬OperatorRidgelet.IsPolynomialFun b) :
  OperatorRidgelet.integralNetworkDensity (fun t => ↑(b t))
      (OperatorRidgelet.parameterMeasure
        (OperatorRidgelet.gaussianMixture N α))
      (OperatorRidgelet.ridgelet μ (⇑ρ)
        (OperatorRidgelet.gaussianTarget W)) =
    fun x =>
    OperatorRidgelet.temperedAdmissibilityConst α β ρ *
      OperatorRidgelet.spectralTarget
        (OperatorRidgelet.gaussianMixture N α)
        (OperatorRidgelet.gaussFourier μ
          (OperatorRidgelet.gaussianTarget W))
        x
    theorem OperatorRidgelet.Paper.ex_7_2_iii_c.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P Q : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (W S : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S))
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ)
  (hβ :
    OperatorRidgelet.IsTemperedFunction β
      b)
  {L : NNReal} (hb : LipschitzWith L b)
  (hbp :
    ¬OperatorRidgelet.IsPolynomialFun b) :
  OperatorRidgelet.integralNetworkDensity
      (fun t => ↑(b t))
      (OperatorRidgelet.parameterMeasure
        (OperatorRidgelet.gaussianMixture
          N α))
      (OperatorRidgelet.ridgelet μ (⇑ρ)
        (OperatorRidgelet.gaussianTarget
          W)) =
    fun x =>
    OperatorRidgelet.temperedAdmissibilityConst
        α β ρ *
      OperatorRidgelet.spectralTarget
        (OperatorRidgelet.gaussianMixture
          N α)
        (OperatorRidgelet.gaussFourier μ
          (OperatorRidgelet.gaussianTarget
            W))
        x
    **Example [ex:7.2]** Closed-form transform and integral representation of `T_α f_W`.
For every
real, globally Lipschitz, non-polynomial `β` (including ReLU), the integral network
`S_β[R_ρ f_W λ_α]` equals `C^{(α)}_{β,ρ} g_G`.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_2_iii_d.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (W S : H →L[ℝ] H)
  (hW : IsSelfAdjoint W) (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS : OperatorRidgelet.IsPositiveSqrt S Q)
  (hM : OperatorRidgelet.HasSummableTrace (S * W * S))
  (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
  (hβ : OperatorRidgelet.IsTemperedFunction β b) {L : NNReal}
  (hb : LipschitzWith L b) (hbp : ¬OperatorRidgelet.IsPolynomialFun b)
  (K : Set H) (hK : IsCompact K) (n : ℕ) (hn : 0 < n) :
  ∫ (θ : Fin n → H × ℝ),
      OperatorRidgelet.compactSupNorm K fun x =>
        OperatorRidgelet.densitySampledNetwork (fun t => ↑(b t))
            (OperatorRidgelet.parameterMeasure
              (OperatorRidgelet.gaussianMixture N α))
            (OperatorRidgelet.ridgelet μ (⇑ρ)
              (OperatorRidgelet.gaussianTarget W))
            θ x -
          OperatorRidgelet.temperedAdmissibilityConst α β ρ *
            OperatorRidgelet.spectralTarget
              (OperatorRidgelet.gaussianMixture N α)
              (OperatorRidgelet.gaussFourier μ
                (OperatorRidgelet.gaussianTarget W))
              x ∂OperatorRidgelet.sampleLaw n
        (OperatorRidgelet.densityLaw
          (OperatorRidgelet.parameterMeasure
            (OperatorRidgelet.gaussianMixture N α))
          (OperatorRidgelet.ridgelet μ (⇑ρ)
            (OperatorRidgelet.gaussianTarget W))) ≤
    8 *
          OperatorRidgelet.densityWeight
            (OperatorRidgelet.parameterMeasure
              (OperatorRidgelet.gaussianMixture N α))
            (OperatorRidgelet.ridgelet μ (⇑ρ)
              (OperatorRidgelet.gaussianTarget W)) /
        √↑n *
      (|b 0| +
        ↑L * OperatorRidgelet.compactRadius K *
          √(OperatorRidgelet.secondMoment
              (OperatorRidgelet.densityLaw
                (OperatorRidgelet.parameterMeasure
                  (OperatorRidgelet.gaussianMixture N α))
                (OperatorRidgelet.ridgelet μ (⇑ρ)
                  (OperatorRidgelet.gaussianTarget W)))))
    theorem OperatorRidgelet.Paper.ex_7_2_iii_d.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P Q : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (W S : H →L[ℝ] H) (hW : IsSelfAdjoint W)
  (hW0 : ∀ (x : H), 0 ≤ inner ℝ (W x) x)
  (hWi : Function.Injective ⇑W)
  (hS :
    OperatorRidgelet.IsPositiveSqrt S Q)
  (hM :
    OperatorRidgelet.HasSummableTrace
      (S * W * S))
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ)
  (hβ :
    OperatorRidgelet.IsTemperedFunction β
      b)
  {L : NNReal} (hb : LipschitzWith L b)
  (hbp :
    ¬OperatorRidgelet.IsPolynomialFun b)
  (K : Set H) (hK : IsCompact K) (n : ℕ)
  (hn : 0 < n) :
  ∫ (θ : Fin n → H × ℝ),
      OperatorRidgelet.compactSupNorm K
        fun x =>
        OperatorRidgelet.densitySampledNetwork
            (fun t => ↑(b t))
            (OperatorRidgelet.parameterMeasure
              (OperatorRidgelet.gaussianMixture
                N α))
            (OperatorRidgelet.ridgelet μ
              (⇑ρ)
              (OperatorRidgelet.gaussianTarget
                W))
            θ x -
          OperatorRidgelet.temperedAdmissibilityConst
              α β ρ *
            OperatorRidgelet.spectralTarget
              (OperatorRidgelet.gaussianMixture
                N α)
              (OperatorRidgelet.gaussFourier
                μ
                (OperatorRidgelet.gaussianTarget
                  W))
              x ∂OperatorRidgelet.sampleLaw
        n
        (OperatorRidgelet.densityLaw
          (OperatorRidgelet.parameterMeasure
            (OperatorRidgelet.gaussianMixture
              N α))
          (OperatorRidgelet.ridgelet μ
            (⇑ρ)
            (OperatorRidgelet.gaussianTarget
              W))) ≤
    8 *
          OperatorRidgelet.densityWeight
            (OperatorRidgelet.parameterMeasure
              (OperatorRidgelet.gaussianMixture
                N α))
            (OperatorRidgelet.ridgelet μ
              (⇑ρ)
              (OperatorRidgelet.gaussianTarget
                W)) /
        √↑n *
      (|b 0| +
        ↑L *
            OperatorRidgelet.compactRadius
              K *
          √(OperatorRidgelet.secondMoment
              (OperatorRidgelet.densityLaw
                (OperatorRidgelet.parameterMeasure
                  (OperatorRidgelet.gaussianMixture
                    N α))
                (OperatorRidgelet.ridgelet
                  μ (⇑ρ)
                  (OperatorRidgelet.gaussianTarget
                    W)))))
    **Example [ex:7.2]** Closed-form transform and integral representation of `T_α f_W`.
For every
real, globally Lipschitz, non-polynomial `β`, the sampled network `eq:polar-network` of
`R_ρ f_W λ_α` (with `V = ‖R_ρ f_W‖_{L¹(λ_α)}` and samples from `p = |R_ρ f_W| λ_α / V`, as in
Theorem `thm:6.6`(iv)) converges to `C^{(α)}_{β,ρ} g_G` at the rate `n^{-1/2}` in `C(K)`, as in
`eq:spectral-barron`: `E‖f_n - C g_G‖_{C(K)} ≤ 8V n^{-1/2} (|β(0)| + Lip(β) R_K M₂)`.
Proof for Example 7.2
Proof uses 7
Proof dependency previews
Preview
Lemma 3.1
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

Lemma 7.1 with \Sigma=Q, S=W gives F_Qf_W, Fourier inversion in the bias gives the convolution, (I+M)^{-1}\ge(1+\|M\|)^{-1}I gives the decay needed by Lemma 3.12, and f_W(x)<1=f_W(0) for x\ne0 in the kernel of a finite-rank map. Part (ii) is Theorem 4.8 (iii) with the Gaussian integral applied on each Gaussian component of \nu_\alpha; part (iii) is Lemma 4.4 (a) with S_W\ge(1+\|M\|)^{-1}Q followed by Theorem 6.6.