7.3. Neural-operator layers🔗

Example7.6

Statement uses 6

Statement dependency previews

Preview

Definition 2.2

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Example 7.8

Loading preview

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

✓L∃∀N

The standing hypotheses on (a,b), the norm \|A\|_\infty, the layer \mathcal F, the observable F_\varphi, the weight w_\varphi, the operator A:H\to L^2(m), the covariances S_y=Q-(1+\sigma_y^2)^{-1}(Qa_y)\otimes(Qa_y) with \sigma_y^2=\langle Qa_y,a_y\rangle, the Y-valued coefficient measure \Gamma=\iota_\#(b_y\,m(\mathrm dy)) with \iota(y)=(a_y,0), and the coefficient measure of the ReLU form, the pushforward of \phi''(b)\,b_y\,m(\mathrm dy)\,\mathrm db under (y,b)\mapsto(a_y,-b).

(i) \mathcal F=S_\beta[\Gamma] with \Gamma=\iota_\#(b_y\,m(\mathrm dy)), whose total variation is at most \int\|b_y\|m(\mathrm dy) and whose second parameter moment is at most \|A\|_\infty^2; hence width-N networks approximate \mathcal F at the rate N^{-1/2} in L^2(\zeta;Y), and for globally Lipschitz \beta the whole output function is approximated uniformly, \mathbb E\|F_N-\mathcal F\|_{C(K;Y)}\le\frac{B_1}{\sqrt N}(4|\beta(0)|+8\operatorname{Lip}(\beta)R_K\|A\|_\infty) with B_1=\int\|v_y\|\,m(\mathrm dy), the scalar observable having the same bound with \|w_\varphi\|_{L^1(m)} in place of B_1. (ii) For \beta=\Phi, F_\varphi\in\mathcal D_\alpha for every \alpha>0, F_QF_\varphi(\xi)=\int_\Omega w_\varphi(y)(1+\sigma_y^2)^{-1/2}e^{-\langle S_y\xi,\xi\rangle/2}\,m(\mathrm dy), R_\rho F_\varphi(a,c)=\int_\Omega w_\varphi(y)(1+\sigma_y^2)^{-1/2}(\rho*\phi_{\langle S_ya,a\rangle})(c)\,m(\mathrm dy), and S_y\ge(1+\|Q\|\|A\|_\infty^2)^{-1}Q; consequently F_QF_\varphi satisfies Definition 4.2, the reconstruction formulas of Theorem 4.8 hold for F_\varphi, and R_\rho F_\varphi synthesizes, with any real Lipschitz non-polynomial \beta', the target C_{\beta',\rho}^{(\alpha)}T_\alpha F_\varphi with the finite-width rate of Theorem 6.6; the same holds for \mathcal F as a Y-valued target. (iii) The Gaussian-activation layer is also the ReLU network \mathcal F(x)=\int_{\Omega\times\mathbb R}b_y\,\phi''(b)\operatorname{ReLU}(\langle a_y,x\rangle-b)\,m(\mathrm dy)\,\mathrm db with finite coefficient measure and finite moments. (iv) If A has infinite rank, \beta=\Phi, and w_\varphi>0 m-almost everywhere, then F_\varphi is not cylindrical.

Lean code for Example7.6●37 declarations

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_i_a.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω] (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m] (a : Ω → H) (b : Ω → Y)
  (hL : OperatorRidgelet.IsLayerData m a b) (β : ℝ → ℝ)
  (hβc : Continuous β) (hβp : OperatorRidgelet.HasPolynomialGrowth β) :
  OperatorRidgelet.operatorLayer m a b β =
    OperatorRidgelet.integralNetwork (fun t => ↑(β t))
      (OperatorRidgelet.layerMeasure m a b)

theorem OperatorRidgelet.Paper.ex_7_6_i_a.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b)
  (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp :
    OperatorRidgelet.HasPolynomialGrowth
      β) :
  OperatorRidgelet.operatorLayer m a b β =
    OperatorRidgelet.integralNetwork
      (fun t => ↑(β t))
      (OperatorRidgelet.layerMeasure m a
        b)

**Example [ex:7.6]** Neural-operator layer as an integral network.  Network
structure: `ℱ = S_β[Γ]` with the `Y`-valued measure `Γ = ι_#(b_y m(dy))`, `ι(y) = (a_y, 0)`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_i_b.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3} [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y) (hL : OperatorRidgelet.IsLayerData m a b) :
  OperatorRidgelet.totalVariation
      (OperatorRidgelet.layerMeasure m a b) ≤
    ∫⁻ (y : Ω), ‖b y‖ₑ ∂m

theorem OperatorRidgelet.Paper.ex_7_6_i_b.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b) :
  OperatorRidgelet.totalVariation
      (OperatorRidgelet.layerMeasure m a
        b) ≤
    ∫⁻ (y : Ω), ‖b y‖ₑ ∂m

**Example [ex:7.6]** Neural-operator layer as an integral network.  The total
variation of `Γ` is at most `∫ ‖b_y‖ m(dy)`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_i_c.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3} [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y) (hL : OperatorRidgelet.IsLayerData m a b) :
  ∫⁻ (θ : H × ℝ),
      ENNReal.ofReal
        (‖θ.1‖ ^ 2 +
          |θ.2| ^ 2) ∂(OperatorRidgelet.layerMeasure m a b).variation ≤
    ENNReal.ofReal (OperatorRidgelet.layerSupNorm a ^ 2) *
      OperatorRidgelet.totalVariation
        (OperatorRidgelet.layerMeasure m a b)

theorem OperatorRidgelet.Paper.ex_7_6_i_c.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b) :
  ∫⁻ (θ : H × ℝ),
      ENNReal.ofReal
        (‖θ.1‖ ^ 2 +
          |θ.2| ^
            2) ∂(OperatorRidgelet.layerMeasure
          m a b).variation ≤
    ENNReal.ofReal
        (OperatorRidgelet.layerSupNorm a ^
          2) *
      OperatorRidgelet.totalVariation
        (OperatorRidgelet.layerMeasure m a
          b)

**Example [ex:7.6]** Neural-operator layer as an integral network.  The second
parameter moment of `Γ` is at most `‖A‖_∞²`: `∫ (‖a‖² + c²) d|Γ| ≤ ‖A‖_∞² ‖Γ‖_TV`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_i_d.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {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) (β : ℝ → ℝ) {L : NNReal}
  (hβ : LipschitzWith L β) (ζ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure ζ]
  (hζ : MeasureTheory.Integrable (fun x => ‖x‖ ^ 2) ζ) (n : ℕ)
  (hn : 0 < n) :
  ∫ (θ : Fin n → H × ℝ),
      ∫ (x : H),
        ‖OperatorRidgelet.polarSampledNetwork (fun t => ↑(β t))
                (OperatorRidgelet.layerMeasure m a b) θ x -
              OperatorRidgelet.operatorLayer m a b β x‖ ^
          2 ∂ζ ∂OperatorRidgelet.sampleLaw n
        (OperatorRidgelet.polarLaw
          (OperatorRidgelet.layerMeasure m a b)) ≤
    2 * (∫ (y : Ω), ‖b y‖ ∂m) ^ 2 / ↑n *
      (|β 0| ^ 2 +
        ↑L ^ 2 * (1 + ∫ (x : H), ‖x‖ ^ 2 ∂ζ) *
          OperatorRidgelet.layerSupNorm a ^ 2)

theorem OperatorRidgelet.Paper.ex_7_6_i_d.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {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)
  (β : ℝ → ℝ) {L : NNReal}
  (hβ : LipschitzWith L β)
  (ζ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure ζ]
  (hζ :
    MeasureTheory.Integrable
      (fun x => ‖x‖ ^ 2) ζ)
  (n : ℕ) (hn : 0 < n) :
  ∫ (θ : Fin n → H × ℝ),
      ∫ (x : H),
        ‖OperatorRidgelet.polarSampledNetwork
                (fun t => ↑(β t))
                (OperatorRidgelet.layerMeasure
                  m a b)
                θ x -
              OperatorRidgelet.operatorLayer
                m a b β x‖ ^
          2 ∂ζ ∂OperatorRidgelet.sampleLaw
        n
        (OperatorRidgelet.polarLaw
          (OperatorRidgelet.layerMeasure m
            a b)) ≤
    2 * (∫ (y : Ω), ‖b y‖ ∂m) ^ 2 / ↑n *
      (|β 0| ^ 2 +
        ↑L ^ 2 *
            (1 + ∫ (x : H), ‖x‖ ^ 2 ∂ζ) *
          OperatorRidgelet.layerSupNorm
              a ^
            2)

**Example [ex:7.6]** Neural-operator layer as an integral network.  Hence
Corollary `cor:6.10` gives width-`n` networks approximating `ℱ` at the rate `n^{-1/2}` in
`L²(ζ;Y)`: for globally Lipschitz `β`, the polar sampled network of `Γ` (samples from
`p = |Γ|/V`) satisfies, by (b) and (c),
`E‖f_n - ℱ‖²_{L²(ζ;Y)} ≤ 2 (∫‖b_y‖ m(dy))² n⁻¹ (|β(0)|² + Lip(β)² (1 + ∫‖x‖² dζ) ‖A‖_∞²)`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_i_e.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω] (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m] (a : Ω → H) (b : Ω → Y)
  (hL : OperatorRidgelet.IsLayerData m a b) (β : ℝ → ℝ) {L : NNReal}
  (hβ : LipschitzWith L β) (φ : Y) (K : Set H) (hK : IsCompact K)
  (n : ℕ) (hn : 0 < n) :
  ∫ (θ : Fin n → H × ℝ),
      OperatorRidgelet.compactSupNorm K fun x =>
        OperatorRidgelet.polarSampledNetwork (fun t => ↑(β t))
            (OperatorRidgelet.layerMeasure m a
              (OperatorRidgelet.layerWeight b φ))
            θ x -
          OperatorRidgelet.layerObservable m a b β φ
            x ∂OperatorRidgelet.sampleLaw n
        (OperatorRidgelet.polarLaw
          (OperatorRidgelet.layerMeasure m a
            (OperatorRidgelet.layerWeight b φ))) ≤
    (8 * ∫ (y : Ω), ‖OperatorRidgelet.layerWeight b φ y‖ ∂m) / √↑n *
      (|β 0| +
        ↑L * OperatorRidgelet.compactRadius K *
          OperatorRidgelet.layerSupNorm a)

theorem OperatorRidgelet.Paper.ex_7_6_i_e.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b)
  (β : ℝ → ℝ) {L : NNReal}
  (hβ : LipschitzWith L β) (φ : Y)
  (K : Set H) (hK : IsCompact K) (n : ℕ)
  (hn : 0 < n) :
  ∫ (θ : Fin n → H × ℝ),
      OperatorRidgelet.compactSupNorm K
        fun x =>
        OperatorRidgelet.polarSampledNetwork
            (fun t => ↑(β t))
            (OperatorRidgelet.layerMeasure
              m a
              (OperatorRidgelet.layerWeight
                b φ))
            θ x -
          OperatorRidgelet.layerObservable
            m a b β φ
            x ∂OperatorRidgelet.sampleLaw
        n
        (OperatorRidgelet.polarLaw
          (OperatorRidgelet.layerMeasure m
            a
            (OperatorRidgelet.layerWeight
              b φ))) ≤
    (8 *
          ∫ (y : Ω),
            ‖OperatorRidgelet.layerWeight
                b φ y‖ ∂m) /
        √↑n *
      (|β 0| +
        ↑L *
            OperatorRidgelet.compactRadius
              K *
          OperatorRidgelet.layerSupNorm a)

**Example [ex:7.6]** Neural-operator layer as an integral network.  For each
`φ ∈ Y` and globally Lipschitz `β`, Theorem `thm:6.5` applied to
`F_φ = S_β[Γ_φ]`, `Γ_φ = ι_#(w_φ m)`, gives for the polar sampled network `F_{φ,n}` of `Γ_φ`
`E‖F_{φ,n} - F_φ‖_{C(K)} ≤ 8 ‖w_φ‖_{L¹(m)} n^{-1/2} (|β(0)| + Lip(β) R_K ‖A‖_∞)`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_i_f.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {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) (β : ℝ → ℝ) {L : NNReal}
  (hβ : LipschitzWith L β) (K : Set H) (hK : IsCompact K) (n : ℕ)
  (hn : 0 < n) :
  ∫ (θ : Fin n → H × ℝ),
      OperatorRidgelet.compactSupNorm K fun x =>
        OperatorRidgelet.polarSampledNetwork (fun t => ↑(β t))
            (OperatorRidgelet.layerMeasure m a b) θ x -
          OperatorRidgelet.operatorLayer m a b β
            x ∂OperatorRidgelet.sampleLaw n
        (OperatorRidgelet.polarLaw
          (OperatorRidgelet.layerMeasure m a b)) ≤
    (∫ (y : Ω), ‖b y‖ ∂m) / √↑n *
      (4 * |β 0| +
        8 * ↑L * OperatorRidgelet.compactRadius K *
          OperatorRidgelet.layerSupNorm a)

theorem OperatorRidgelet.Paper.ex_7_6_i_f.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {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)
  (β : ℝ → ℝ) {L : NNReal}
  (hβ : LipschitzWith L β) (K : Set H)
  (hK : IsCompact K) (n : ℕ)
  (hn : 0 < n) :
  ∫ (θ : Fin n → H × ℝ),
      OperatorRidgelet.compactSupNorm K
        fun x =>
        OperatorRidgelet.polarSampledNetwork
            (fun t => ↑(β t))
            (OperatorRidgelet.layerMeasure
              m a b)
            θ x -
          OperatorRidgelet.operatorLayer m
            a b β
            x ∂OperatorRidgelet.sampleLaw
        n
        (OperatorRidgelet.polarLaw
          (OperatorRidgelet.layerMeasure m
            a b)) ≤
    (∫ (y : Ω), ‖b y‖ ∂m) / √↑n *
      (4 * |β 0| +
        8 * ↑L *
            OperatorRidgelet.compactRadius
              K *
          OperatorRidgelet.layerSupNorm a)

**Example [ex:7.6]** Neural-operator layer as an integral network.  For globally
Lipschitz `β`, Theorem `thm:6.5` applied to `F = S_β[Γ]`, `Γ = ι_#(v_y m)`, bounds
the error of the polar sampled network uniformly on the whole output function:
`E‖F_N - F‖_{C(K;Y)} ≤ B₁ N^{-1/2} (4|β(0)| + 8 Lip(β) R_K ‖A‖_∞)` with
`B₁ = ∫ ‖v_y‖ m(dy)` (`eq:operator-layer-uniform`).

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_ii_a.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [SecondCountableTopology Y] {Ω : Type u_3}
  [MeasurableSpace Ω] (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 μ)
  (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_7_6_ii_a.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  {Ω : Type u_3} [MeasurableSpace Ω]
  (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
      μ)
  (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:7.6]** Neural-operator layer as an integral network.  Gaussian
activation `β = Φ`: `F_φ ∈ 𝒟_α` for every `α > 0`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_ii_b.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [MeasurableSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω] {Q : H →L[ℝ] H}
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ)
  (m : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y) (hL : OperatorRidgelet.IsLayerData m a b)
  (φ : Y) (ξ : H) :
  OperatorRidgelet.gaussFourier μ
      (OperatorRidgelet.layerObservable m a b
        OperatorRidgelet.gaussianFun φ)
      ξ =
    ∫ (y : Ω),
      OperatorRidgelet.layerWeight b φ y *
        ↑((√(1 + inner ℝ (Q (a y)) (a y)))⁻¹ *
            Real.exp
              (-inner ℝ ((OperatorRidgelet.layerCovariance Q a y) ξ) ξ /
                2)) ∂m

theorem OperatorRidgelet.Paper.ex_7_6_ii_b.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω] {Q : H →L[ℝ] H}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b)
  (φ : Y) (ξ : H) :
  OperatorRidgelet.gaussFourier μ
      (OperatorRidgelet.layerObservable m
        a b OperatorRidgelet.gaussianFun
        φ)
      ξ =
    ∫ (y : Ω),
      OperatorRidgelet.layerWeight b φ y *
        ↑((√(1 +
                  inner ℝ (Q (a y))
                    (a y)))⁻¹ *
            Real.exp
              (-inner ℝ
                    ((OperatorRidgelet.layerCovariance
                        Q a y)
                      ξ)
                    ξ /
                2)) ∂m

**Example [ex:7.6]** Neural-operator layer as an integral network.  Gaussian
activation: with `σ_y² = ⟨Qa_y,a_y⟩` and `S_y = Q - (1+σ_y²)⁻¹ (Qa_y) ⊗ (Qa_y)`,
`F_Q F_φ(ξ) = ∫ w_φ(y) (1+σ_y²)^{-1/2} e^{-⟨S_yξ,ξ⟩/2} m(dy)` (`eq:operator-layer-transform`).

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_ii_c.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [MeasurableSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω] {Q : H →L[ℝ] H}
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m] (a : Ω → H) (b : Ω → Y)
  (hL : OperatorRidgelet.IsLayerData m a b) (φ : Y) (p : H × ℝ) :
  OperatorRidgelet.ridgelet μ (⇑ρ)
      (OperatorRidgelet.layerObservable m a b
        OperatorRidgelet.gaussianFun φ)
      p =
    ∫ (y : Ω),
      OperatorRidgelet.layerWeight b φ y *
        ↑((√(1 + inner ℝ (Q (a y)) (a y)))⁻¹ *
            OperatorRidgelet.gaussianSmooth (⇑ρ)
              (inner ℝ ((OperatorRidgelet.layerCovariance Q a y) p.1)
                p.1)
              p.2) ∂m

theorem OperatorRidgelet.Paper.ex_7_6_ii_c.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω] {Q : H →L[ℝ] H}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b)
  (φ : Y) (p : H × ℝ) :
  OperatorRidgelet.ridgelet μ (⇑ρ)
      (OperatorRidgelet.layerObservable m
        a b OperatorRidgelet.gaussianFun
        φ)
      p =
    ∫ (y : Ω),
      OperatorRidgelet.layerWeight b φ y *
        ↑((√(1 +
                  inner ℝ (Q (a y))
                    (a y)))⁻¹ *
            OperatorRidgelet.gaussianSmooth
              (⇑ρ)
              (inner ℝ
                ((OperatorRidgelet.layerCovariance
                    Q a y)
                  p.1)
                p.1)
              p.2) ∂m

**Example [ex:7.6]** Neural-operator layer as an integral network.  Gaussian
activation: for every band-pass `ρ`,
`R_ρ F_φ(a,c) = ∫ w_φ(y) (1+σ_y²)^{-1/2} (ρ * φ_{⟨S_ya,a⟩})(c) m(dy)`
(`eq:operator-layer-transform`).

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_ii_d.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3} [MeasurableSpace Ω] {Q : H →L[ℝ] H}
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  (m : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y) (hL : OperatorRidgelet.IsLayerData m a b)
  (y : Ω) (ξ : H) :
  (1 + ‖Q‖ * OperatorRidgelet.layerSupNorm a ^ 2)⁻¹ * inner ℝ (Q ξ) ξ ≤
    inner ℝ ((OperatorRidgelet.layerCovariance Q a y) ξ) ξ

theorem OperatorRidgelet.Paper.ex_7_6_ii_d.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω] {Q : H →L[ℝ] H}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b)
  (y : Ω) (ξ : H) :
  (1 +
          ‖Q‖ *
            OperatorRidgelet.layerSupNorm
                a ^
              2)⁻¹ *
      inner ℝ (Q ξ) ξ ≤
    inner ℝ
      ((OperatorRidgelet.layerCovariance Q
          a y)
        ξ)
      ξ

**Example [ex:7.6]** Neural-operator layer as an integral network.  Gaussian
activation: `S_y ≥ (1 + ‖Q‖ ‖A‖_∞²)⁻¹ Q`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_ii_e.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [SecondCountableTopology Y] {Ω : Type u_3}
  [MeasurableSpace Ω] (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 ρ) (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m] (a : Ω → H) (b : Ω → Y)
  (hL : OperatorRidgelet.IsLayerData m a b) (φ : Y) (I : Set ℝ) :
  OperatorRidgelet.IsFrequencyWindow (⇑ρ) I →
    OperatorRidgelet.IsRegularAlongRays
      (OperatorRidgelet.gaussianMixture N α) I
      (OperatorRidgelet.gaussFourier μ
        (OperatorRidgelet.layerObservable m a b
          OperatorRidgelet.gaussianFun φ))

theorem OperatorRidgelet.Paper.ex_7_6_ii_e.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  {Ω : Type u_3} [MeasurableSpace Ω]
  (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 ρ)
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b)
  (φ : Y) (I : Set ℝ) :
  OperatorRidgelet.IsFrequencyWindow (⇑ρ)
      I →
    OperatorRidgelet.IsRegularAlongRays
      (OperatorRidgelet.gaussianMixture N
        α)
      I
      (OperatorRidgelet.gaussFourier μ
        (OperatorRidgelet.layerObservable
          m a b
          OperatorRidgelet.gaussianFun φ))

**Example [ex:7.6]** Neural-operator layer as an integral network.  Gaussian
activation: consequently `F_Q F_φ` is regular along rays, for every band-pass `ρ`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_ii_f.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [SecondCountableTopology Y] {Ω : Type u_3}
  [MeasurableSpace Ω] (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 μ)
  (m : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y) (hL : OperatorRidgelet.IsLayerData m a b)
  (φ : Y)
  (F :
    ↥(OperatorRidgelet.spectralCore μ
        (OperatorRidgelet.gaussianMixture N α))) :
  ↑↑↑F =ᵐ[μ]
      OperatorRidgelet.layerObservable m a b
        OperatorRidgelet.gaussianFun φ →
    ∀
      (g :
        ↥(OperatorRidgelet.spectralCore μ
            (OperatorRidgelet.gaussianMixture N α))),
      (OperatorRidgelet.frameOperator μ
            (OperatorRidgelet.gaussianMixture N α)
            (OperatorRidgelet.spectralEmbed μ
              (OperatorRidgelet.gaussianMixture N α) F))
          (OperatorRidgelet.spectralEmbed μ
            (OperatorRidgelet.gaussianMixture N α) g) =
        ∫ (x : H),
          OperatorRidgelet.spectralTarget
              (OperatorRidgelet.gaussianMixture N α)
              (OperatorRidgelet.gaussFourier μ
                (OperatorRidgelet.layerObservable m a b
                  OperatorRidgelet.gaussianFun φ))
              x *
            (starRingEnd ℂ) (↑↑↑g x) ∂μ

theorem OperatorRidgelet.Paper.ex_7_6_ii_f.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  {Ω : Type u_3} [MeasurableSpace Ω]
  (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
      μ)
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b)
  (φ : Y)
  (F :
    ↥(OperatorRidgelet.spectralCore μ
        (OperatorRidgelet.gaussianMixture
          N α))) :
  ↑↑↑F =ᵐ[μ]
      OperatorRidgelet.layerObservable m a
        b OperatorRidgelet.gaussianFun φ →
    ∀
      (g :
        ↥(OperatorRidgelet.spectralCore μ
            (OperatorRidgelet.gaussianMixture
              N α))),
      (OperatorRidgelet.frameOperator μ
            (OperatorRidgelet.gaussianMixture
              N α)
            (OperatorRidgelet.spectralEmbed
              μ
              (OperatorRidgelet.gaussianMixture
                N α)
              F))
          (OperatorRidgelet.spectralEmbed
            μ
            (OperatorRidgelet.gaussianMixture
              N α)
            g) =
        ∫ (x : H),
          OperatorRidgelet.spectralTarget
              (OperatorRidgelet.gaussianMixture
                N α)
              (OperatorRidgelet.gaussFourier
                μ
                (OperatorRidgelet.layerObservable
                  m a b
                  OperatorRidgelet.gaussianFun
                  φ))
              x *
            (starRingEnd ℂ) (↑↑↑g x) ∂μ

**Example [ex:7.6]** Neural-operator layer as an integral network.  Gaussian
activation: the reconstruction formulas of Theorem `thm:4.8` hold for `F_φ`; in particular
`T_α F_φ` is represented by `g_G`, `G = F_Q F_φ`: `T_α F_φ [g] = ∫ g_G(x) conj(g(x)) μ_Q(dx)`
for `g ∈ 𝒟_α`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_ii_g.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [MeasurableSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω] {Q : H →L[ℝ] H}
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m] (a : Ω → H) (b : Ω → Y)
  (hL : OperatorRidgelet.IsLayerData m a b) (φ : Y) :
  OperatorRidgelet.ridgelet μ (⇑ρ)
      (OperatorRidgelet.layerObservable m a b
        OperatorRidgelet.gaussianFun φ) =
    OperatorRidgelet.coefficientFormula (⇑ρ)
      (OperatorRidgelet.gaussFourier μ
        (OperatorRidgelet.layerObservable m a b
          OperatorRidgelet.gaussianFun φ))

theorem OperatorRidgelet.Paper.ex_7_6_ii_g.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω] {Q : H →L[ℝ] H}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b)
  (φ : Y) :
  OperatorRidgelet.ridgelet μ (⇑ρ)
      (OperatorRidgelet.layerObservable m
        a b OperatorRidgelet.gaussianFun
        φ) =
    OperatorRidgelet.coefficientFormula
      (⇑ρ)
      (OperatorRidgelet.gaussFourier μ
        (OperatorRidgelet.layerObservable
          m a b
          OperatorRidgelet.gaussianFun φ))

**Example [ex:7.6]** Neural-operator layer as an integral network.  Gaussian
activation: the ridgelet coefficient of `F_φ` is the coefficient `γ_G` of `G = F_Q F_φ`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_ii_h.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [SecondCountableTopology Y] {Ω : Type u_3}
  [MeasurableSpace Ω] (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 ρ) (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m] (a : Ω → H) (b : Ω → Y)
  (hL : OperatorRidgelet.IsLayerData m a b) (φ : Y) :
  MeasureTheory.Integrable
    (fun p =>
      (1 + ‖p.1‖ ^ 2 + |p.2| ^ 2) *
        ‖OperatorRidgelet.ridgelet μ (⇑ρ)
            (OperatorRidgelet.layerObservable m a b
              OperatorRidgelet.gaussianFun φ)
            p‖)
    (OperatorRidgelet.parameterMeasure
      (OperatorRidgelet.gaussianMixture N α))

theorem OperatorRidgelet.Paper.ex_7_6_ii_h.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  {Ω : Type u_3} [MeasurableSpace Ω]
  (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 ρ)
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b)
  (φ : Y) :
  MeasureTheory.Integrable
    (fun p =>
      (1 + ‖p.1‖ ^ 2 + |p.2| ^ 2) *
        ‖OperatorRidgelet.ridgelet μ (⇑ρ)
            (OperatorRidgelet.layerObservable
              m a b
              OperatorRidgelet.gaussianFun
              φ)
            p‖)
    (OperatorRidgelet.parameterMeasure
      (OperatorRidgelet.gaussianMixture N
        α))

**Example [ex:7.6]** Neural-operator layer as an integral network.  Gaussian
activation: the coefficient measure `(R_ρ F_φ) λ_α` has finite total variation and moments,
`∫ (1 + ‖a‖² + |c|²) |R_ρ F_φ(a,c)| λ_α(da,dc) < ∞`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_ii_i.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [SecondCountableTopology Y] {Ω : Type u_3}
  [MeasurableSpace Ω] (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 ρ) (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m] (a : Ω → H) (b : Ω → Y)
  (hL : OperatorRidgelet.IsLayerData m a b) (φ : Y)
  (β' : TemperedDistribution ℝ ℂ) (b' : ℝ → ℝ)
  (hβ' : OperatorRidgelet.IsTemperedFunction β' b') {L : NNReal}
  (hb' : LipschitzWith L b')
  (hb'p : ¬OperatorRidgelet.IsPolynomialFun b') :
  OperatorRidgelet.integralNetworkDensity (fun t => ↑(b' t))
      (OperatorRidgelet.parameterMeasure
        (OperatorRidgelet.gaussianMixture N α))
      (OperatorRidgelet.ridgelet μ (⇑ρ)
        (OperatorRidgelet.layerObservable m a b
          OperatorRidgelet.gaussianFun φ)) =
    fun x =>
    OperatorRidgelet.temperedAdmissibilityConst α β' ρ *
      OperatorRidgelet.spectralTarget
        (OperatorRidgelet.gaussianMixture N α)
        (OperatorRidgelet.gaussFourier μ
          (OperatorRidgelet.layerObservable m a b
            OperatorRidgelet.gaussianFun φ))
        x

theorem OperatorRidgelet.Paper.ex_7_6_ii_i.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  {Ω : Type u_3} [MeasurableSpace Ω]
  (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 ρ)
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b)
  (φ : Y) (β' : TemperedDistribution ℝ ℂ)
  (b' : ℝ → ℝ)
  (hβ' :
    OperatorRidgelet.IsTemperedFunction β'
      b')
  {L : NNReal} (hb' : LipschitzWith L b')
  (hb'p :
    ¬OperatorRidgelet.IsPolynomialFun
        b') :
  OperatorRidgelet.integralNetworkDensity
      (fun t => ↑(b' t))
      (OperatorRidgelet.parameterMeasure
        (OperatorRidgelet.gaussianMixture
          N α))
      (OperatorRidgelet.ridgelet μ (⇑ρ)
        (OperatorRidgelet.layerObservable
          m a b
          OperatorRidgelet.gaussianFun
          φ)) =
    fun x =>
    OperatorRidgelet.temperedAdmissibilityConst
        α β' ρ *
      OperatorRidgelet.spectralTarget
        (OperatorRidgelet.gaussianMixture
          N α)
        (OperatorRidgelet.gaussFourier μ
          (OperatorRidgelet.layerObservable
            m a b
            OperatorRidgelet.gaussianFun
            φ))
        x

**Example [ex:7.6]** Neural-operator layer as an integral network.  Gaussian
activation: the ridgelet coefficient `R_ρ F_φ` synthesizes, with any real Lipschitz
non-polynomial `β'`, the target `C^{(α)}_{β',ρ} T_α F_φ` (represented by `g_G`).

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_ii_j.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [SecondCountableTopology Y] {Ω : Type u_3}
  [MeasurableSpace Ω] (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 ρ) (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m] (a : Ω → H) (b : Ω → Y)
  (hL : OperatorRidgelet.IsLayerData m a b) (φ : Y)
  (β' : TemperedDistribution ℝ ℂ) (b' : ℝ → ℝ)
  (hβ' : OperatorRidgelet.IsTemperedFunction β' b') {L : NNReal}
  (hb' : LipschitzWith L b')
  (hb'p : ¬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.layerObservable m a b
                OperatorRidgelet.gaussianFun φ))
            θ x -
          OperatorRidgelet.temperedAdmissibilityConst α β' ρ *
            OperatorRidgelet.spectralTarget
              (OperatorRidgelet.gaussianMixture N α)
              (OperatorRidgelet.gaussFourier μ
                (OperatorRidgelet.layerObservable m a b
                  OperatorRidgelet.gaussianFun φ))
              x ∂OperatorRidgelet.sampleLaw n
        (OperatorRidgelet.densityLaw
          (OperatorRidgelet.parameterMeasure
            (OperatorRidgelet.gaussianMixture N α))
          (OperatorRidgelet.ridgelet μ (⇑ρ)
            (OperatorRidgelet.layerObservable m a b
              OperatorRidgelet.gaussianFun φ))) ≤
    8 *
          OperatorRidgelet.densityWeight
            (OperatorRidgelet.parameterMeasure
              (OperatorRidgelet.gaussianMixture N α))
            (OperatorRidgelet.ridgelet μ (⇑ρ)
              (OperatorRidgelet.layerObservable m a b
                OperatorRidgelet.gaussianFun φ)) /
        √↑n *
      (|b' 0| +
        ↑L * OperatorRidgelet.compactRadius K *
          √(OperatorRidgelet.secondMoment
              (OperatorRidgelet.densityLaw
                (OperatorRidgelet.parameterMeasure
                  (OperatorRidgelet.gaussianMixture N α))
                (OperatorRidgelet.ridgelet μ (⇑ρ)
                  (OperatorRidgelet.layerObservable m a b
                    OperatorRidgelet.gaussianFun φ)))))

theorem OperatorRidgelet.Paper.ex_7_6_ii_j.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  {Ω : Type u_3} [MeasurableSpace Ω]
  (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 ρ)
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b)
  (φ : Y) (β' : TemperedDistribution ℝ ℂ)
  (b' : ℝ → ℝ)
  (hβ' :
    OperatorRidgelet.IsTemperedFunction β'
      b')
  {L : NNReal} (hb' : LipschitzWith L b')
  (hb'p :
    ¬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.layerObservable
                m a b
                OperatorRidgelet.gaussianFun
                φ))
            θ x -
          OperatorRidgelet.temperedAdmissibilityConst
              α β' ρ *
            OperatorRidgelet.spectralTarget
              (OperatorRidgelet.gaussianMixture
                N α)
              (OperatorRidgelet.gaussFourier
                μ
                (OperatorRidgelet.layerObservable
                  m a b
                  OperatorRidgelet.gaussianFun
                  φ))
              x ∂OperatorRidgelet.sampleLaw
        n
        (OperatorRidgelet.densityLaw
          (OperatorRidgelet.parameterMeasure
            (OperatorRidgelet.gaussianMixture
              N α))
          (OperatorRidgelet.ridgelet μ
            (⇑ρ)
            (OperatorRidgelet.layerObservable
              m a b
              OperatorRidgelet.gaussianFun
              φ))) ≤
    8 *
          OperatorRidgelet.densityWeight
            (OperatorRidgelet.parameterMeasure
              (OperatorRidgelet.gaussianMixture
                N α))
            (OperatorRidgelet.ridgelet μ
              (⇑ρ)
              (OperatorRidgelet.layerObservable
                m a b
                OperatorRidgelet.gaussianFun
                φ)) /
        √↑n *
      (|b' 0| +
        ↑L *
            OperatorRidgelet.compactRadius
              K *
          √(OperatorRidgelet.secondMoment
              (OperatorRidgelet.densityLaw
                (OperatorRidgelet.parameterMeasure
                  (OperatorRidgelet.gaussianMixture
                    N α))
                (OperatorRidgelet.ridgelet
                  μ (⇑ρ)
                  (OperatorRidgelet.layerObservable
                    m a b
                    OperatorRidgelet.gaussianFun
                    φ)))))

**Example [ex:7.6]** Neural-operator layer as an integral network.  Gaussian
activation: the sampled network `eq:polar-network` of `R_ρ F_φ λ_α` with a real Lipschitz
non-polynomial `β'` (with `V = ‖R_ρ F_φ‖_{L¹(λ_α)}` and samples from `p = |R_ρ F_φ| λ_α / V`,
as in Theorem `thm:6.6`(iv)) converges to `C^{(α)}_{β',ρ} g_G` at the finite-width rate of
`eq:spectral-barron`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_ii_k.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [SecondCountableTopology Y] {Ω : Type u_3}
  [MeasurableSpace Ω] (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 μ)
  (m : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y) (hL : OperatorRidgelet.IsLayerData m a b) :
  OperatorRidgelet.MemSpectralCoreVec μ
    (OperatorRidgelet.gaussianMixture N α)
    (OperatorRidgelet.operatorLayer m a b OperatorRidgelet.gaussianFun)

theorem OperatorRidgelet.Paper.ex_7_6_ii_k.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  {Ω : Type u_3} [MeasurableSpace Ω]
  (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
      μ)
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b) :
  OperatorRidgelet.MemSpectralCoreVec μ
    (OperatorRidgelet.gaussianMixture N α)
    (OperatorRidgelet.operatorLayer m a b
      OperatorRidgelet.gaussianFun)

**Example [ex:7.6]** Neural-operator layer as an integral network.  The same
holds for `ℱ` itself as a `Y`-valued target: `ℱ ∈ 𝒟_α(Y)` for every `α > 0`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_ii_l.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [MeasurableSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω] {Q : H →L[ℝ] H}
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ)
  (m : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y) (hL : OperatorRidgelet.IsLayerData m a b)
  (ξ : H) :
  OperatorRidgelet.gaussFourierVec μ
      (OperatorRidgelet.operatorLayer m a b
        OperatorRidgelet.gaussianFun)
      ξ =
    ∫ (y : Ω),
      ↑((√(1 + inner ℝ (Q (a y)) (a y)))⁻¹ *
            Real.exp
              (-inner ℝ ((OperatorRidgelet.layerCovariance Q a y) ξ) ξ /
                2)) •
        b y ∂m

theorem OperatorRidgelet.Paper.ex_7_6_ii_l.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω] {Q : H →L[ℝ] H}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b)
  (ξ : H) :
  OperatorRidgelet.gaussFourierVec μ
      (OperatorRidgelet.operatorLayer m a
        b OperatorRidgelet.gaussianFun)
      ξ =
    ∫ (y : Ω),
      ↑((√(1 +
                  inner ℝ (Q (a y))
                    (a y)))⁻¹ *
            Real.exp
              (-inner ℝ
                    ((OperatorRidgelet.layerCovariance
                        Q a y)
                      ξ)
                    ξ /
                2)) •
        b y ∂m

**Example [ex:7.6]** Neural-operator layer as an integral network.  The same
holds for `ℱ` itself as a `Y`-valued target:
`F_Q ℱ(ξ) = ∫ (1+σ_y²)^{-1/2} e^{-⟨S_yξ,ξ⟩/2} b_y m(dy)`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_ii_m.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [SecondCountableTopology Y] {Ω : Type u_3}
  [MeasurableSpace Ω] (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 ρ) (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m] (a : Ω → H) (b : Ω → Y)
  (hL : OperatorRidgelet.IsLayerData m a b) (I : Set ℝ) :
  OperatorRidgelet.IsFrequencyWindow (⇑ρ) I →
    OperatorRidgelet.IsRegularAlongRays
      (OperatorRidgelet.gaussianMixture N α) I
      (OperatorRidgelet.gaussFourierVec μ
        (OperatorRidgelet.operatorLayer m a b
          OperatorRidgelet.gaussianFun))

theorem OperatorRidgelet.Paper.ex_7_6_ii_m.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  {Ω : Type u_3} [MeasurableSpace Ω]
  (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 ρ)
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b)
  (I : Set ℝ) :
  OperatorRidgelet.IsFrequencyWindow (⇑ρ)
      I →
    OperatorRidgelet.IsRegularAlongRays
      (OperatorRidgelet.gaussianMixture N
        α)
      I
      (OperatorRidgelet.gaussFourierVec μ
        (OperatorRidgelet.operatorLayer m
          a b
          OperatorRidgelet.gaussianFun))

**Example [ex:7.6]** Neural-operator layer as an integral network.  The same
holds for `ℱ` itself as a `Y`-valued target: `F_Q ℱ` is regular along rays for every band-pass
`ρ`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_ii_n.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [MeasurableSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω] {Q : H →L[ℝ] H}
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m] (a : Ω → H) (b : Ω → Y)
  (hL : OperatorRidgelet.IsLayerData m a b) :
  OperatorRidgelet.ridgeletVec μ (⇑ρ)
      (OperatorRidgelet.operatorLayer m a b
        OperatorRidgelet.gaussianFun) =
    OperatorRidgelet.coefficientFormulaVec (⇑ρ)
      (OperatorRidgelet.gaussFourierVec μ
        (OperatorRidgelet.operatorLayer m a b
          OperatorRidgelet.gaussianFun))

theorem OperatorRidgelet.Paper.ex_7_6_ii_n.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω] {Q : H →L[ℝ] H}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b) :
  OperatorRidgelet.ridgeletVec μ (⇑ρ)
      (OperatorRidgelet.operatorLayer m a
        b OperatorRidgelet.gaussianFun) =
    OperatorRidgelet.coefficientFormulaVec
      (⇑ρ)
      (OperatorRidgelet.gaussFourierVec μ
        (OperatorRidgelet.operatorLayer m
          a b
          OperatorRidgelet.gaussianFun))

**Example [ex:7.6]** Neural-operator layer as an integral network.  The same
holds for `ℱ` itself as a `Y`-valued target: `R_ρ ℱ = γ_{F_Q ℱ}` for every band-pass `ρ`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_ii_o.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [SecondCountableTopology Y] {Ω : Type u_3}
  [MeasurableSpace Ω] (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 ρ) (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m] (a : Ω → H) (b : Ω → Y)
  (hL : OperatorRidgelet.IsLayerData m a b) :
  MeasureTheory.Integrable
    (fun p =>
      (1 + ‖p.1‖ ^ 2 + |p.2| ^ 2) *
        ‖OperatorRidgelet.ridgeletVec μ (⇑ρ)
            (OperatorRidgelet.operatorLayer m a b
              OperatorRidgelet.gaussianFun)
            p‖)
    (OperatorRidgelet.parameterMeasure
      (OperatorRidgelet.gaussianMixture N α))

theorem OperatorRidgelet.Paper.ex_7_6_ii_o.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  {Ω : Type u_3} [MeasurableSpace Ω]
  (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 ρ)
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b) :
  MeasureTheory.Integrable
    (fun p =>
      (1 + ‖p.1‖ ^ 2 + |p.2| ^ 2) *
        ‖OperatorRidgelet.ridgeletVec μ
            (⇑ρ)
            (OperatorRidgelet.operatorLayer
              m a b
              OperatorRidgelet.gaussianFun)
            p‖)
    (OperatorRidgelet.parameterMeasure
      (OperatorRidgelet.gaussianMixture N
        α))

**Example [ex:7.6]** Neural-operator layer as an integral network.  The same
holds for `ℱ` itself as a `Y`-valued target: the coefficient measure `(R_ρ ℱ) λ_α` has finite
total variation and moments.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_ii_p.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [SecondCountableTopology Y] {Ω : Type u_3}
  [MeasurableSpace Ω] (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 ρ) (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m] (a : Ω → H) (b : Ω → Y)
  (hL : OperatorRidgelet.IsLayerData m a b)
  (β' : TemperedDistribution ℝ ℂ) (b' : ℝ → ℝ)
  (hβ' : OperatorRidgelet.IsTemperedFunction β' b') {L : NNReal}
  (hb' : LipschitzWith L b')
  (hb'p : ¬OperatorRidgelet.IsPolynomialFun b') :
  OperatorRidgelet.integralNetworkDensity (fun t => ↑(b' t))
      (OperatorRidgelet.parameterMeasure
        (OperatorRidgelet.gaussianMixture N α))
      (OperatorRidgelet.ridgeletVec μ (⇑ρ)
        (OperatorRidgelet.operatorLayer m a b
          OperatorRidgelet.gaussianFun)) =
    fun x =>
    OperatorRidgelet.temperedAdmissibilityConst α β' ρ •
      OperatorRidgelet.spectralTarget
        (OperatorRidgelet.gaussianMixture N α)
        (OperatorRidgelet.gaussFourierVec μ
          (OperatorRidgelet.operatorLayer m a b
            OperatorRidgelet.gaussianFun))
        x

theorem OperatorRidgelet.Paper.ex_7_6_ii_p.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  {Ω : Type u_3} [MeasurableSpace Ω]
  (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 ρ)
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b)
  (β' : TemperedDistribution ℝ ℂ)
  (b' : ℝ → ℝ)
  (hβ' :
    OperatorRidgelet.IsTemperedFunction β'
      b')
  {L : NNReal} (hb' : LipschitzWith L b')
  (hb'p :
    ¬OperatorRidgelet.IsPolynomialFun
        b') :
  OperatorRidgelet.integralNetworkDensity
      (fun t => ↑(b' t))
      (OperatorRidgelet.parameterMeasure
        (OperatorRidgelet.gaussianMixture
          N α))
      (OperatorRidgelet.ridgeletVec μ (⇑ρ)
        (OperatorRidgelet.operatorLayer m
          a b
          OperatorRidgelet.gaussianFun)) =
    fun x =>
    OperatorRidgelet.temperedAdmissibilityConst
        α β' ρ •
      OperatorRidgelet.spectralTarget
        (OperatorRidgelet.gaussianMixture
          N α)
        (OperatorRidgelet.gaussFourierVec
          μ
          (OperatorRidgelet.operatorLayer
            m a b
            OperatorRidgelet.gaussianFun))
        x

**Example [ex:7.6]** Neural-operator layer as an integral network.  The same
holds for `ℱ` itself as a `Y`-valued target: `R_ρ ℱ` synthesizes, with any real Lipschitz
non-polynomial `β'`, the `Y`-valued target `C^{(α)}_{β',ρ} g_{F_Q ℱ}`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_iii_a.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3} [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y) (hL : OperatorRidgelet.IsLayerData m a b)
  (x : H) :
  OperatorRidgelet.operatorLayer m a b OperatorRidgelet.gaussianFun x =
    ∫ (p : Ω × ℝ),
      ↑(OperatorRidgelet.gaussianActDeriv2 p.2 *
            LeanRidgelet.relu (inner ℝ (a p.1) x - p.2)) •
        b p.1 ∂m.prod MeasureTheory.volume

theorem OperatorRidgelet.Paper.ex_7_6_iii_a.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b)
  (x : H) :
  OperatorRidgelet.operatorLayer m a b
      OperatorRidgelet.gaussianFun x =
    ∫ (p : Ω × ℝ),
      ↑(OperatorRidgelet.gaussianActDeriv2
              p.2 *
            LeanRidgelet.relu
              (inner ℝ (a p.1) x - p.2)) •
        b p.1 ∂m.prod MeasureTheory.volume

**Example [ex:7.6]** Neural-operator layer as an integral network.  ReLU form:
by `eq:gaussian-parameter-closed-forms`, the Gaussian-activation layer is
`ℱ(x) = ∫∫ b_y φ''(b) ReLU(⟨a_y,x⟩ - b) m(dy) db`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_iii_b.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω] (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m] (a : Ω → H) (b : Ω → Y)
  (hL : OperatorRidgelet.IsLayerData m a b) :
  OperatorRidgelet.operatorLayer m a b OperatorRidgelet.gaussianFun =
    OperatorRidgelet.integralNetwork (fun t => ↑(LeanRidgelet.relu t))
      (OperatorRidgelet.layerHingeMeasure m a b)

theorem OperatorRidgelet.Paper.ex_7_6_iii_b.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b) :
  OperatorRidgelet.operatorLayer m a b
      OperatorRidgelet.gaussianFun =
    OperatorRidgelet.integralNetwork
      (fun t => ↑(LeanRidgelet.relu t))
      (OperatorRidgelet.layerHingeMeasure
        m a b)

**Example [ex:7.6]** Neural-operator layer as an integral network.  ReLU form:
the Gaussian-activation layer is the ReLU network with the coefficient measure
`(y,b) ↦ (a_y, -b)`-pushforward of `φ''(b) b_y m(dy) db`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_iii_c.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3} [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y) (hL : OperatorRidgelet.IsLayerData m a b) :
  MeasureTheory.IsFiniteMeasure
    (OperatorRidgelet.layerHingeMeasure m a b).variation

theorem OperatorRidgelet.Paper.ex_7_6_iii_c.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b) :
  MeasureTheory.IsFiniteMeasure
    (OperatorRidgelet.layerHingeMeasure m
        a b).variation

**Example [ex:7.6]** Neural-operator layer as an integral network.  ReLU form:
the ReLU coefficient measure is finite.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_iii_d.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3} [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y) (hL : OperatorRidgelet.IsLayerData m a b)
  (k : ℕ) :
  ∫⁻ (θ : H × ℝ),
      ENNReal.ofReal
        ((1 + ‖θ.1‖ + |θ.2|) ^
          k) ∂(OperatorRidgelet.layerHingeMeasure m a b).variation <
    ⊤

theorem OperatorRidgelet.Paper.ex_7_6_iii_d.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b)
  (k : ℕ) :
  ∫⁻ (θ : H × ℝ),
      ENNReal.ofReal
        ((1 + ‖θ.1‖ + |θ.2|) ^
          k) ∂(OperatorRidgelet.layerHingeMeasure
          m a b).variation <
    ⊤

**Example [ex:7.6]** Neural-operator layer as an integral network.  ReLU form:
the ReLU coefficient measure has all moments finite.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_6_iv.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  {Ω : Type u_3} [MeasurableSpace Ω] (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m] (a : Ω → H) (b : Ω → Y)
  (hL : OperatorRidgelet.IsLayerData m a b) (φ : Y)
  (hA : OperatorRidgelet.HasInfiniteRank (OperatorRidgelet.layerA m a))
  (hw :
    ∀ᵐ (y : Ω) ∂m,
      0 < (OperatorRidgelet.layerWeight b φ y).re ∧
        (OperatorRidgelet.layerWeight b φ y).im = 0) :
  ¬OperatorRidgelet.IsCylindrical
      (OperatorRidgelet.layerObservable m a b
        OperatorRidgelet.gaussianFun φ)

theorem OperatorRidgelet.Paper.ex_7_6_iv.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {Ω : Type u_3}
  [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (a : Ω → H) (b : Ω → Y)
  (hL :
    OperatorRidgelet.IsLayerData m a b)
  (φ : Y)
  (hA :
    OperatorRidgelet.HasInfiniteRank
      (OperatorRidgelet.layerA m a))
  (hw :
    ∀ᵐ (y : Ω) ∂m,
      0 <
          (OperatorRidgelet.layerWeight b
              φ y).re ∧
        (OperatorRidgelet.layerWeight b φ
              y).im =
          0) :
  ¬OperatorRidgelet.IsCylindrical
      (OperatorRidgelet.layerObservable m
        a b OperatorRidgelet.gaussianFun
        φ)

**Example [ex:7.6]** Neural-operator layer as an integral network.
Non-cylindricity: if `A` has infinite rank, `β = Φ`, and `w_φ > 0` `m`-almost everywhere, then
`F_φ` is not cylindrical.

defdefined in OperatorRidgelet/Network/Defs.lean

complete

def OperatorRidgelet.HasPolynomialGrowth (β : ℝ → ℝ) : Prop

def OperatorRidgelet.HasPolynomialGrowth
  (β : ℝ → ℝ) : Prop

`β : ℝ → ℝ` has polynomial growth: `|β(t)| ≤ C (1 + |t|)^p` for some constants `C`, `p`.

structure(4 fields)defined in OperatorRidgelet/Examples/Defs.lean

complete

structure OperatorRidgelet.IsLayerData.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] {Y : Type u_2} [NormedAddCommGroup Y]
  {Ω : Type u_3} [MeasurableSpace Ω] (m : MeasureTheory.Measure Ω)
  (a : Ω → H) (b : Ω → Y) : Prop

structure OperatorRidgelet.IsLayerData.{u_1, u_2,
    u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  {Ω : Type u_3} [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω)
  (a : Ω → H) (b : Ω → Y) : Prop

The standing hypotheses of the neural-operator layer: `y ↦ a_y ∈ H` is Borel and bounded,
`y ↦ b_y ∈ Y` is Borel with `∫ ‖b_y‖ m(dy) < ∞`.

Fields

stronglyMeasurable_a : MeasureTheory.StronglyMeasurable a

`y ↦ a_y` is Borel.

bounded_a : ∃ C, ∀ (y : Ω), ‖a y‖ ≤ C

`y ↦ a_y` is bounded.

stronglyMeasurable_b : MeasureTheory.StronglyMeasurable b

`y ↦ b_y` is Borel.

integrable_b : MeasureTheory.Integrable b m

`∫ ‖b_y‖ m(dy) < ∞`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.layerSupNorm.{u_1, u_3} {H : Type u_1}
  [NormedAddCommGroup H] {Ω : Type u_3} (a : Ω → H) : ℝ

def OperatorRidgelet.layerSupNorm.{u_1, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  {Ω : Type u_3} (a : Ω → H) : ℝ

`‖A‖_∞ = sup_y ‖a_y‖`, the supremum over the parameter space `Ω` of the layer (junk `0` if
unbounded).  This is a genuinely different notion from the compact-open norm `compactSupNorm K`
of `OperatorRidgelet.Sampling.Defs`, which is a supremum over a set of inputs `x ∈ K`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.operatorLayer.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] {Ω : Type u_3}
  [MeasurableSpace Ω] (m : MeasureTheory.Measure Ω) (a : Ω → H)
  (b : Ω → Y) (β : ℝ → ℝ) (x : H) : Y

def OperatorRidgelet.operatorLayer.{u_1, u_2,
    u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] {Ω : Type u_3}
  [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω)
  (a : Ω → H) (b : Ω → Y) (β : ℝ → ℝ)
  (x : H) : Y

The neural-operator layer `ℱ(x) = B β(Ax) = ∫ β(⟨a_y,x⟩) b_y m(dy)` (`eq:operator-layer`).

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.layerWeight.{u_2, u_3} {Y : Type u_2}
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] {Ω : Type u_3}
  (b : Ω → Y) (φ : Y) (y : Ω) : ℂ

def OperatorRidgelet.layerWeight.{u_2, u_3}
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] {Ω : Type u_3}
  (b : Ω → Y) (φ : Y) (y : Ω) : ℂ

The weight `w_φ(y) = ⟨b_y, φ⟩_Y` of the scalar observable.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.layerObservable.{u_1, u_2, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] {Ω : Type u_3}
  [MeasurableSpace Ω] (m : MeasureTheory.Measure Ω) (a : Ω → H)
  (b : Ω → Y) (β : ℝ → ℝ) (φ : Y) (x : H) : ℂ

def OperatorRidgelet.layerObservable.{u_1,
    u_2, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] {Ω : Type u_3}
  [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω)
  (a : Ω → H) (b : Ω → Y) (β : ℝ → ℝ)
  (φ : Y) (x : H) : ℂ

The scalar observable `F_φ(x) = ⟨ℱ(x), φ⟩_Y` of the layer.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.layerA.{u_1, u_3} {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Ω : Type u_3} [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω) (a : Ω → H) : H →ₗ[ℝ] Ω →ₘ[m] ℝ

def OperatorRidgelet.layerA.{u_1, u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Ω : Type u_3}
  [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω)
  (a : Ω → H) : H →ₗ[ℝ] Ω →ₘ[m] ℝ

The operator `A : H → L²(m)`, `(Ax)(y) = ⟨a_y, x⟩`, as a linear map into the a.e.-classes
`Ω →ₘ[m] ℝ` (`0` if `a` is not measurable).

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.layerCovariance.{u_1, u_3} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {Ω : Type u_3}
  (Q : H →L[ℝ] H) (a : Ω → H) (y : Ω) : H →L[ℝ] H

def OperatorRidgelet.layerCovariance.{u_1,
    u_3}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Ω : Type u_3}
  (Q : H →L[ℝ] H) (a : Ω → H) (y : Ω) :
  H →L[ℝ] H

The covariance `S_y = Q - (1 + σ_y²)⁻¹ (Qa_y) ⊗ (Qa_y)`, `σ_y² = ⟨Qa_y, a_y⟩`, of
Example `ex:7.6`(ii).

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.layerMeasure.{u_1, u_2, u_3} {H : Type u_1}
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  {Ω : Type u_3} [MeasurableSpace Ω] [MeasurableSpace H]
  (m : MeasureTheory.Measure Ω) (a : Ω → H) (b : Ω → Y) :
  MeasureTheory.VectorMeasure (H × ℝ) Y

def OperatorRidgelet.layerMeasure.{u_1, u_2,
    u_3}
  {H : Type u_1} {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] {Ω : Type u_3}
  [MeasurableSpace Ω] [MeasurableSpace H]
  (m : MeasureTheory.Measure Ω)
  (a : Ω → H) (b : Ω → Y) :
  MeasureTheory.VectorMeasure (H × ℝ) Y

The `Y`-valued coefficient measure `Γ = ι_#(b_y m(dy))`, `ι(y) = (a_y, 0)`, of the layer.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.layerHingeMeasure.{u_1, u_2, u_3} {H : Type u_1}
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  {Ω : Type u_3} [MeasurableSpace Ω] [MeasurableSpace H]
  (m : MeasureTheory.Measure Ω) (a : Ω → H) (b : Ω → Y) :
  MeasureTheory.VectorMeasure (H × ℝ) Y

def OperatorRidgelet.layerHingeMeasure.{u_1,
    u_2, u_3}
  {H : Type u_1} {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] {Ω : Type u_3}
  [MeasurableSpace Ω] [MeasurableSpace H]
  (m : MeasureTheory.Measure Ω)
  (a : Ω → H) (b : Ω → Y) :
  MeasureTheory.VectorMeasure (H × ℝ) Y

The coefficient measure of the ReLU form of the Gaussian-activation layer: the pushforward
of `φ''(b) b_y m(dy) db` under `(y, b) ↦ (a_y, -b)`.

Proof for Example 7.6

Proof uses 7

Proof dependency previews

Preview

Lemma 3.5

Loading preview

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

Part (i) is the change of variables for the pushforward measure and \|\iota(y)\|^2\le\|A\|_\infty^2. For (ii), the pair (\langle a_y,x\rangle,\langle x,\xi\rangle) is centred Gaussian under \mu_Q and \mathbb E[e^{-Z^2/2}e^{-iW}]=(1+\sigma^2)^{-1/2}\exp(-\tau^2/2+r^2/(2(1+\sigma^2))); Cauchy–Schwarz gives the lower bound on S_y, Lemma 4.4 (a) and (c) give the condition in Definition 4.2, and Theorem 4.8, Theorem 6.6, and Theorem 4.11 give the rest. Part (iii) is Fubini with Lemma 7.3; for (iv), a vector x\in\ker L\setminus\ker A gives F_\varphi(tx)=F_\varphi(0) for all t, while dominated convergence gives F_\varphi(tx)\to\int w_\varphi\mathbf 1_{\{Ax=0\}}\mathrm dm<F_\varphi(0).

Remark 7.7 (Equivariance of the transform).

If a unitary U satisfies UQU^*=Q, then the Gaussian input law is invariant and R_\rho[f\circ U](a,b)=R_\rho f(Ua,b). If also UPU^*=P, the direction and parameter measures are invariant and the Plancherel and reconstruction formulas commute with this action. On L^2(\mathbb R^d), a translation-invariant Gaussian input law with injective trace-class covariance is unavailable. The Gaussian weight therefore breaks translation invariance there; the operator-layer network identity itself does not use that input weight.