Infinite-dimensional operator ridgelet transform

3.4. The Hilbert space E-alpha🔗

Definition3.10
Statement uses 2
Statement dependency previews
Preview
Definition Aux.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 11
Reverse dependency previews
Preview
Lemma 3.11
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

\mathcal D_\alpha=\{f\in L^2(H,\mu_Q):F_Qf\in L^2(H,\nu_\alpha)\} with \langle f,g\rangle_{\mathcal E_\alpha}=\int_HF_Qf\,\overline{F_Qg}\,\mathrm d\nu_\alpha. The Hilbert space \mathcal E_\alpha is the completion of \mathcal D_\alpha in this norm, and \mathcal K_\alpha=\overline{F_Q(\mathcal D_\alpha)}^{L^2(\nu_\alpha)} is the closure of the range of F_Q on \mathcal D_\alpha. The formalization represents \mathcal E_\alpha by \mathcal K_\alpha and the core restriction of F_Q by the map F_Q:\mathcal D_\alpha\to\mathcal K_\alpha, f\mapsto F_Qf.

Lean code for Definition3.10●5 definitions
  • defdefined in OperatorRidgelet/Transform/Defs.lean
    complete
    def OperatorRidgelet.spectralCore.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] :
  Submodule ℂ ↥(MeasureTheory.Lp ℂ 2 μ)
    def OperatorRidgelet.spectralCore.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] :
  Submodule ℂ ↥(MeasureTheory.Lp ℂ 2 μ)
    The core `𝒟 = {f ∈ L²(μ) : F_μ f ∈ L²(ν)}` (the manuscript's `𝒟_α` for `ν = ν_α`), as a
submodule of `L²(μ)`.
  • defdefined in OperatorRidgelet/Transform/Defs.lean
    complete
    def OperatorRidgelet.spectralInner.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (μ ν : MeasureTheory.Measure H) (f g : H → ℂ) : ℂ
    def OperatorRidgelet.spectralInner.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  (f g : H → ℂ) : ℂ
    The spectral inner product `⟨f,g⟩_𝓔 = ∫ F_μ f conj(F_μ g) dν`, linear in the first
argument as in the manuscript.
  • defdefined in OperatorRidgelet/Transform/Defs.lean
    complete
    def OperatorRidgelet.spectralRange.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] :
  Submodule ℂ ↥(MeasureTheory.Lp ℂ 2 ν)
    def OperatorRidgelet.spectralRange.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] :
  Submodule ℂ ↥(MeasureTheory.Lp ℂ 2 ν)
    The closed subspace `𝒦 = closure (F_μ 𝒟) ⊆ L²(ν)` (the manuscript's `𝒦_α`), which
represents the Hilbert space `𝓔_α` in this formalization.
  • defdefined in OperatorRidgelet/Transform/Defs.lean
    complete
    def OperatorRidgelet.gaussFourierLp.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (f : ↥(OperatorRidgelet.spectralCore μ ν)) : ↥(MeasureTheory.Lp ℂ 2 ν)
    def OperatorRidgelet.gaussFourierLp.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (f :
    ↥(OperatorRidgelet.spectralCore μ
        ν)) :
  ↥(MeasureTheory.Lp ℂ 2 ν)
    `F_μ f` as an element of `L²(ν)`, for `f ∈ 𝒟`.
  • defdefined in OperatorRidgelet/Transform/Defs.lean
    complete
    def OperatorRidgelet.spectralEmbed.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (f : ↥(OperatorRidgelet.spectralCore μ ν)) :
  ↥(OperatorRidgelet.spectralRange μ ν)
    def OperatorRidgelet.spectralEmbed.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (f :
    ↥(OperatorRidgelet.spectralCore μ
        ν)) :
  ↥(OperatorRidgelet.spectralRange μ ν)
    The map `F_Q : 𝒟 → 𝒦`, `f ↦ F_μ f`; the unitary `F_Q : 𝓔_α → 𝒦_α` of the manuscript is
its extension to the completion, which is the identity of `𝒦` in this representation.
Lemma3.11
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 3.14
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The spectral form is positive definite on \mathcal D_\alpha (i), F_Q is an isometry from (\mathcal D_\alpha,\langle\cdot,\cdot\rangle_{\mathcal E_\alpha}) into \mathcal K_\alpha (ii), and its image is dense (iii), so that F_Q extends uniquely to a unitary F_Q:\mathcal E_\alpha\to\mathcal K_\alpha. The same symbol denotes the concrete Gaussian integral on the core and its unitary extension. Outside the core it is an L^2(\nu_\alpha) class; no pointwise Gaussian integral representation is assumed.

Lean code for Lemma3.11●3 theorems
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.lem_3_11_i.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure]
  (f : ↥(MeasureTheory.Lp ℂ 2 μ)) :
  f ∈ OperatorRidgelet.spectralCore μ ν →
    OperatorRidgelet.spectralInner μ ν ↑↑f ↑↑f = 0 → f = 0
    theorem OperatorRidgelet.Paper.lem_3_11_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure]
  (f : ↥(MeasureTheory.Lp ℂ 2 μ)) :
  f ∈ OperatorRidgelet.spectralCore μ ν →
    OperatorRidgelet.spectralInner μ ν ↑↑f
          ↑↑f =
        0 →
      f = 0
    **Lemma [lem:3.11]** Positivity and the unitary extension.  The spectral form is
positive definite on `𝒟`: `⟨f,f⟩_𝓔 = 0` forces `f = 0` in `L²(μ)`.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.lem_3_11_ii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] (f g : ↥(OperatorRidgelet.spectralCore μ ν)) :
  inner ℂ (OperatorRidgelet.spectralEmbed μ ν f)
      (OperatorRidgelet.spectralEmbed μ ν g) =
    OperatorRidgelet.spectralInner μ ν ↑↑↑g ↑↑↑f
    theorem OperatorRidgelet.Paper.lem_3_11_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure]
  (f g :
    ↥(OperatorRidgelet.spectralCore μ
        ν)) :
  inner ℂ
      (OperatorRidgelet.spectralEmbed μ ν
        f)
      (OperatorRidgelet.spectralEmbed μ ν
        g) =
    OperatorRidgelet.spectralInner μ ν
      ↑↑↑g ↑↑↑f
    **Lemma [lem:3.11]** Positivity and the unitary extension.  `F_μ` is an
isometry from `(𝒟, ⟨·,·⟩_𝓔)` into `𝒦`: the `L²(ν)` inner product of `F_Q f` and `F_Q g` (which in
Mathlib is conjugate linear in the first argument) is `⟨g,f⟩_𝓔`.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.lem_3_11_iii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] :
  Dense (Set.range (OperatorRidgelet.spectralEmbed μ ν))
    theorem OperatorRidgelet.Paper.lem_3_11_iii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] :
  Dense
    (Set.range
      (OperatorRidgelet.spectralEmbed μ
        ν))
    **Lemma [lem:3.11]** Positivity and the unitary extension.  The image of `𝒟`
under `F_μ` is dense in `𝒦`, so the isometry extends uniquely to a unitary `F_Q : 𝓔_α → 𝒦_α`
(the identity of `𝒦` in this representation).
Proof for Lemma 3.11
uses 1

If the norm of f\in\mathcal D_\alpha vanishes, then F_Qf=0 almost everywhere, hence everywhere by continuity and full support of \nu_\alpha; the Fourier transform determines finite complex Borel measures on a separable Hilbert space, so f\mu_Q=0.

Lemma3.12
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
Example 3.13
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

For every t>0, \alpha>0, and integer m\ge0, \int_H\|\xi\|^{2m}e^{-t\langle Q\xi,\xi\rangle}\,\nu_\alpha(\mathrm d\xi)<\infty (i). Consequently, if f\in L^2(\mu_Q) and |F_Qf(\xi)|\le C(1+\|\xi\|)^pe^{-t\langle Q\xi,\xi\rangle/2}, then f\in\mathcal D_\alpha for every \alpha>0 (ii).

Lean code for Lemma3.12●2 theorems
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.lem_3_12_i.{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 < α) (t : ℝ) :
  0 < t →
    ∀ (m : ℕ),
      MeasureTheory.Integrable
        (fun ξ => ‖ξ‖ ^ (2 * m) * Real.exp (-t * inner ℝ (Q ξ) ξ))
        (OperatorRidgelet.gaussianMixture N α)
    theorem OperatorRidgelet.Paper.lem_3_12_i.{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 < α) (t : ℝ) :
  0 < t →
    ∀ (m : ℕ),
      MeasureTheory.Integrable
        (fun ξ =>
          ‖ξ‖ ^ (2 * m) *
            Real.exp
              (-t * inner ℝ (Q ξ) ξ))
        (OperatorRidgelet.gaussianMixture
          N α)
    **Lemma [lem:3.12]** Gaussian decay with polynomial weights.  For `t > 0` and every
integer `m ≥ 0`, `∫ ‖ξ‖^{2m} e^{-t⟨Qξ,ξ⟩} ν_α(dξ) < ∞`.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.lem_3_12_ii.{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 μ)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ)) (C p t : ℝ) (hC : 0 < C) (hp : 0 ≤ p)
  (ht : 0 < t)
  (hdecay :
    ∀ (ξ : H),
      ‖OperatorRidgelet.gaussFourier μ (↑↑f) ξ‖ ≤
        C * (1 + ‖ξ‖) ^ p * Real.exp (-t * inner ℝ (Q ξ) ξ / 2)) :
  f ∈
    OperatorRidgelet.spectralCore μ
      (OperatorRidgelet.gaussianMixture N α)
    theorem OperatorRidgelet.Paper.lem_3_12_ii.{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
      μ)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ))
  (C p t : ℝ) (hC : 0 < C) (hp : 0 ≤ p)
  (ht : 0 < t)
  (hdecay :
    ∀ (ξ : H),
      ‖OperatorRidgelet.gaussFourier μ
            (↑↑f) ξ‖ ≤
        C * (1 + ‖ξ‖) ^ p *
          Real.exp
            (-t * inner ℝ (Q ξ) ξ / 2)) :
  f ∈
    OperatorRidgelet.spectralCore μ
      (OperatorRidgelet.gaussianMixture N
        α)
    **Lemma [lem:3.12]** Gaussian decay with polynomial weights.  If `f ∈ L²(μ_Q)` and
`|F_Q f(ξ)| ≤ C (1+‖ξ‖)^p e^{-t⟨Qξ,ξ⟩/2}`, then `f ∈ 𝒟_α` for every `α > 0`.
Proof for Lemma 3.12
uses 1

On each Gaussian component, Cauchy–Schwarz separates the polynomial factor, whose moments are finite, from the Gaussian factor, whose integral is \prod_j(1+8st\theta_j)^{-1/2} with \theta_j>0 the eigenvalues of P^{1/2}QP^{1/2}; retaining k>4m+2\alpha factors makes the mixture integral finite.

Example3.13
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 0✓L∃∀N

The constant function 1 has F_Q1(\xi)=e^{-\langle Q\xi,\xi\rangle/2} (i), so 1\in\mathcal D_\alpha for every \alpha>0 (ii) and \mathcal E_\alpha\ne\{0\} (iii).

Lean code for Example3.13●5 theorems
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.ex_3_13_i.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Q : H →L[ℝ] H} (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ξ : H) :
  OperatorRidgelet.gaussFourier μ (fun x => 1) ξ =
    Complex.exp (-↑(inner ℝ (Q ξ) ξ / 2))
    theorem OperatorRidgelet.Paper.ex_3_13_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Q : H →L[ℝ] H}
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ξ : H) :
  OperatorRidgelet.gaussFourier μ
      (fun x => 1) ξ =
    Complex.exp (-↑(inner ℝ (Q ξ) ξ / 2))
    **Example [ex:3.13]** Elements of `𝒟_α`.  The constant function has
`F_Q 1 (ξ) = e^{-⟨Qξ,ξ⟩/2}`.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.ex_3_13_ii.{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 μ) :
  MeasureTheory.MemLp.toLp (fun x => 1) ⋯ ∈
    OperatorRidgelet.spectralCore μ
      (OperatorRidgelet.gaussianMixture N α)
    theorem OperatorRidgelet.Paper.ex_3_13_ii.{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
      μ) :
  MeasureTheory.MemLp.toLp (fun x => 1)
      ⋯ ∈
    OperatorRidgelet.spectralCore μ
      (OperatorRidgelet.gaussianMixture N
        α)
    **Example [ex:3.13]** Elements of `𝒟_α`.  The constant function belongs to `𝒟_α`
for every `α > 0`.
  • theoremdefined in OperatorRidgelet/Paper/Transform.lean
    complete
    theorem OperatorRidgelet.Paper.ex_3_13_iii.{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 μ) :
  OperatorRidgelet.spectralRange μ
      (OperatorRidgelet.gaussianMixture N α) ≠
    ⊥
    theorem OperatorRidgelet.Paper.ex_3_13_iii.{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
      μ) :
  OperatorRidgelet.spectralRange μ
      (OperatorRidgelet.gaussianMixture N
        α) ≠
    ⊥
    **Example [ex:3.13]** Elements of `𝒟_α`.  Consequently `𝓔_α ≠ {0}`.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_3_13_iv.{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_3_13_iv.{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:3.13]** Elements of `𝒟_α`.  The non-cylindrical Gaussian target
`f_W` of Example `ex:7.2` belongs to `𝒟_α` for every `α > 0`.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_3_13_v.{u_1, u_2, u_3} {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 μ) {Y : Type u_2}
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  [SecondCountableTopology Y] {Ω : Type u_3} [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y) (hL : OperatorRidgelet.IsLayerData m a b)
  (φ : Y) :
  OperatorRidgelet.MemSpectralCore μ
    (OperatorRidgelet.gaussianMixture N α)
    (OperatorRidgelet.layerObservable m a b OperatorRidgelet.gaussianFun
      φ)
    theorem OperatorRidgelet.Paper.ex_3_13_v.{u_1,
    u_2, u_3}
  {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
      μ)
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  {Ω : Type u_3} [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b)
  (φ : Y) :
  OperatorRidgelet.MemSpectralCore μ
    (OperatorRidgelet.gaussianMixture N α)
    (OperatorRidgelet.layerObservable m a
      b OperatorRidgelet.gaussianFun φ)
    **Example [ex:3.13]** Elements of `𝒟_α`.  The components `F_φ` of the
neural-operator layers with Gaussian activation of Example `ex:7.6` belong to `𝒟_α`
for every `α > 0`.
Proof for Example 3.13
uses 1

The Gaussian characteristic functional gives F_Q1, and the decay lemma with m=0, p=0, t=1 gives 1\in\mathcal D_\alpha.

Further core elements are the Gaussian targets and Gaussian-activation operator layers proved in Section 7. The Lean panel for the preceding example also retains two verified facets about those later examples. They support this preview and are not used in the proof of the constant example or the next theorem.