2.3. The Hilbert space🔗

Definition2.3.1

Statement uses 2

Statement dependency previews

Preview

Definition 2.1.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 12

Reverse dependency previews

Preview

Lemma 2.3.2

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):\mathcal G_Qf\in L^2(H,\nu_\alpha)\} with \langle f,g\rangle_{\mathcal E_\alpha}=\int_H\mathcal G_Qf\,\overline{\mathcal G_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{\mathcal G_Q(\mathcal D_\alpha)}^{L^2(\nu_\alpha)} is the closure of the range of \mathcal G_Q on \mathcal D_\alpha. The formalization represents \mathcal E_\alpha by \mathcal K_\alpha and the unitary U_\alpha by the map U:\mathcal D_\alpha\to\mathcal K_\alpha, f\mapsto\mathcal G_Qf.

Lean code for Definition2.3.1●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 ∈ 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 conj(𝒢_μ 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 (𝒢_μ 𝒟) ⊆ 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` 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 `U : 𝒟 → 𝒦`, `f ↦ 𝒢_μ f`; the unitary `U_α : 𝓔_α → 𝒦_α` of the manuscript is
its extension to the completion, which is the identity of `𝒦` in this representation.

Lemma2.3.2

Statement uses 2

Statement dependency previews

Preview

Lemma 2.1.4

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 3

Reverse dependency previews

Preview

Theorem 2.4.1

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), \mathcal G_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 \mathcal G_Q extends uniquely to a unitary U_\alpha:\mathcal E_\alpha\to\mathcal K_\alpha.

Lean code for Lemma2.3.2●3 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_spectral_unitary_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_spectral_unitary_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:spectral-unitary]** 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_spectral_unitary_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_spectral_unitary_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:spectral-unitary]** Positivity and the unitary extension.  `𝒢_μ` is an
isometry from `(𝒟, ⟨·,·⟩_𝓔)` into `𝒦`: the `L²(ν)` inner product of `U f` and `U 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_spectral_unitary_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_spectral_unitary_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:spectral-unitary]** Positivity and the unitary extension.  The image of `𝒟`
under `𝒢_μ` is dense in `𝒦`, so the isometry extends uniquely to a unitary `U_α : 𝓔_α → 𝒦_α`
(the identity of `𝒦` in this representation).

Proof for Lemma 2.3.2

uses 0

If the norm of f\in\mathcal D_\alpha vanishes, then \mathcal G_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.

Lemma2.3.3

Statement uses 3

Statement dependency previews

Preview

Definition 2.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 4

Reverse dependency previews

Preview

Proposition 2.3.4

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 |\mathcal G_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 Lemma2.3.3●2 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.lem_gaussian_decay_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_gaussian_decay_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:gaussian-decay]** 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_gaussian_decay_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_gaussian_decay_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:gaussian-decay]** Gaussian decay with polynomial weights.  If `f ∈ L²(μ_Q)` and
`|𝒢_Q f(ξ)| ≤ C (1+‖ξ‖)^p e^{-t⟨Qξ,ξ⟩/2}`, then `f ∈ 𝒟_α` for every `α > 0`.

Proof for Lemma 2.3.3

uses 0

On each Gaussian layer, 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.

Proposition2.3.4

Statement uses 5

Statement dependency previews

Preview

Definition 2.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

The constant function 1 has \mathcal G_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). The non-cylindrical Gaussian target f_W(x)=e^{-\langle Wx,x\rangle/2} of Proposition 6.2.1 belongs to every \mathcal D_\alpha (iv), and so do the components of the neural-operator layers with Gaussian activation of Proposition 6.4.2 (v).

Lean code for Proposition2.3.4●5 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_core_elements_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_core_elements_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:core-elements]** Elements of `𝒟_α`.  The constant function has
`𝒢_Q 1 (ξ) = e^{-⟨Qξ,ξ⟩/2}`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_core_elements_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_core_elements_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:core-elements]** Elements of `𝒟_α`.  The constant function belongs to `𝒟_α`
for every `α > 0`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.ex_core_elements_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_core_elements_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:core-elements]** Elements of `𝒟_α`.  Consequently `𝓔_α ≠ {0}`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_core_elements_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_core_elements_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:core-elements]** Elements of `𝒟_α`.  The non-cylindrical Gaussian target
`f_W` of Example `ex:closed-form` belongs to `𝒟_α` for every `α > 0`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_core_elements_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_core_elements_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:core-elements]** Elements of `𝒟_α`.  The components `F_φ` of the
neural-operator layers with Gaussian activation of Example `ex:operator-layer` belong to `𝒟_α`
for every `α > 0`.

Proof for Proposition 2.3.4

uses 0

The Gaussian characteristic functional gives \mathcal G_Q1, and the decay lemma with m=0, p=0, t=1 gives 1\in\mathcal D_\alpha; the other two assertions are proved with the examples, using only the decay lemma and the Fourier-slice identity.