6.4. Neural-operator layers🔗

Let (\Omega,m) be a finite measure space, y\mapsto a_y\in H Borel and bounded with \|A\|_\infty=\sup_y\|a_y\|, and y\mapsto b_y\in Y Borel with \int_\Omega\|b_y\|_Ym(\mathrm dy)<\infty. With (Ax)(y)=\langle a_y,x\rangle and Bu=\int_\Omega b_yu(y)\,m(\mathrm dy), the layer with a continuous real activation \beta of polynomial growth is \mathcal F(x)=B\,\beta(Ax)=\int_\Omega b_y\,\beta(\langle a_y,x\rangle)\,m(\mathrm dy); for \varphi\in Y the scalar observable is F_\varphi(x)=\langle\mathcal F(x),\varphi\rangle_Y and w_\varphi(y)=\langle b_y,\varphi\rangle_Y.

Definition6.4.1

Statement uses 3

Statement dependency previews

Preview

Definition 1.1.2

Loading preview

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

Used by 5

Reverse dependency previews

Preview

Proposition 6.4.2

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).

Lean code for Definition6.4.1●10 definitions

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:operator-layer`(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)`.

Proposition6.4.2

Statement uses 13

Statement dependency previews

Preview

Definition 1.1.2

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Proposition 2.3.4

Loading preview

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

✓L∃∀N

(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, \mathcal G_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 \mathcal G_QF_\varphi is regular along rays, the reconstruction formulas of Theorem 3.2.7 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 5.2.1; 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 Proposition6.4.2●27 theorems

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_operator_layer_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_operator_layer_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:operator-layer]** 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_operator_layer_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_operator_layer_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:operator-layer]** 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_operator_layer_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_operator_layer_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:operator-layer]** 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_operator_layer_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_operator_layer_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:operator-layer]** Neural-operator layer as an integral network.  Hence
Corollary `cor:vector-rates` 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_operator_layer_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_operator_layer_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:operator-layer]** Neural-operator layer as an integral network.  For each
`φ ∈ Y` and globally Lipschitz `β`, Theorem `thm:lipschitz-barron` 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_operator_layer_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_operator_layer_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:operator-layer]** Neural-operator layer as an integral network.  For globally
Lipschitz `β`, Theorem `thm:lipschitz-barron` 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_operator_layer_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_operator_layer_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:operator-layer]** Neural-operator layer as an integral network.  Gaussian
activation `β = Φ`: `F_φ ∈ 𝒟_α` for every `α > 0`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_operator_layer_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_operator_layer_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:operator-layer]** 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)`,
`𝒢_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_operator_layer_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_operator_layer_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:operator-layer]** 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_operator_layer_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_operator_layer_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:operator-layer]** 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_operator_layer_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_operator_layer_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:operator-layer]** Neural-operator layer as an integral network.  Gaussian
activation: consequently `𝒢_Q F_φ` is regular along rays, for every band-pass `ρ`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_operator_layer_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_operator_layer_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:operator-layer]** Neural-operator layer as an integral network.  Gaussian
activation: the reconstruction formulas of Theorem `thm:C` hold for `F_φ`; in particular
`T_α F_φ` is represented by `g_G`, `G = 𝒢_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_operator_layer_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_operator_layer_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:operator-layer]** Neural-operator layer as an integral network.  Gaussian
activation: the ridgelet coefficient of `F_φ` is the coefficient `γ_G` of `G = 𝒢_Q F_φ`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_operator_layer_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_operator_layer_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:operator-layer]** Neural-operator layer as an integral network.  Gaussian
activation: the ridgelet coefficient `R_ρ F_φ` has finite variation and moments,
`∫ (1 + ‖a‖² + |c|²) |R_ρ F_φ(a,c)| λ_α(da,dc) < ∞`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_operator_layer_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_operator_layer_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:operator-layer]** 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_operator_layer_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_operator_layer_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:operator-layer]** 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:E`(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_operator_layer_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_operator_layer_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:operator-layer]** 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_operator_layer_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_operator_layer_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:operator-layer]** Neural-operator layer as an integral network.  The same
holds for `ℱ` itself as a `Y`-valued target:
`𝒢_Q ℱ(ξ) = ∫ (1+σ_y²)^{-1/2} e^{-⟨S_yξ,ξ⟩/2} b_y m(dy)`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_operator_layer_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_operator_layer_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:operator-layer]** Neural-operator layer as an integral network.  The same
holds for `ℱ` itself as a `Y`-valued target: `𝒢_Q ℱ` is regular along rays for every band-pass
`ρ`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_operator_layer_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_operator_layer_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:operator-layer]** Neural-operator layer as an integral network.  The same
holds for `ℱ` itself as a `Y`-valued target: `R_ρ ℱ = γ_{𝒢_Q ℱ}` for every band-pass `ρ`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_operator_layer_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_operator_layer_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:operator-layer]** Neural-operator layer as an integral network.  The same
holds for `ℱ` itself as a `Y`-valued target: `R_ρ ℱ` has finite variation and moments.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_operator_layer_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_operator_layer_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:operator-layer]** 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_{𝒢_Q ℱ}`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_operator_layer_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_operator_layer_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:operator-layer]** 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_operator_layer_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_operator_layer_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:operator-layer]** 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_operator_layer_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_operator_layer_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:operator-layer]** 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_operator_layer_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_operator_layer_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:operator-layer]** 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_operator_layer_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_operator_layer_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:operator-layer]** 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.

Proof for Proposition 6.4.2

uses 0

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 5.2.2 (a) and (c) give regularity along rays, and Theorem 3.2.7, Theorem 5.2.1, and Theorem 3.3.2 give the rest. Part (iii) is Fubini with Lemma 6.1.6; 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).

Definition6.4.3

uses 1used by 1✓L∃∀N

The torus \mathbb T^d=(\mathbb R/2\pi\mathbb Z)^d with normalized Haar measure, H=L^2(\mathbb T^d;\mathbb R) and Y=L^2(\mathbb T^d), the translations (\tau_zx)(t)=x(t-z), the convolution-layer data a_y=k(y-\cdot) and b_y=\psi(\cdot-y), the constant function 1, the characters e_n(t)=e^{i\langle n,t\rangle} and Fourier coefficients \widehat f(n), and the Bessel operator (I-\Delta)^{-s}, multiplying the n-th Fourier coefficient by (1+|n|^2)^{-s}.

Lean code for Definition6.4.3●13 definitions

abbrevdefined in OperatorRidgelet/Examples/Defs.lean

complete

abbrev OperatorRidgelet.Torus (d : ℕ) : Type

abbrev OperatorRidgelet.Torus (d : ℕ) : Type

The torus `𝕋^d = (ℝ/2πℤ)^d`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.torusHaar (d : ℕ) :
  MeasureTheory.Measure (OperatorRidgelet.Torus d)

def OperatorRidgelet.torusHaar (d : ℕ) :
  MeasureTheory.Measure
    (OperatorRidgelet.Torus d)

The normalized Haar (probability) measure on `𝕋^d`.

abbrevdefined in OperatorRidgelet/Examples/Defs.lean

complete

abbrev OperatorRidgelet.TorusL2 (d : ℕ) : Type

abbrev OperatorRidgelet.TorusL2 (d : ℕ) : Type

`L²(𝕋^d; ℝ)`, the input space of the convolution layer.

abbrevdefined in OperatorRidgelet/Examples/Defs.lean

complete

abbrev OperatorRidgelet.TorusL2C (d : ℕ) : Type

abbrev OperatorRidgelet.TorusL2C (d : ℕ) : Type

`L²(𝕋^d)`, the output space of the convolution layer.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.torusTranslate (d : ℕ) (z : OperatorRidgelet.Torus d) :
  OperatorRidgelet.TorusL2 d →ₗᵢ[ℝ] OperatorRidgelet.TorusL2 d

def OperatorRidgelet.torusTranslate (d : ℕ)
  (z : OperatorRidgelet.Torus d) :
  OperatorRidgelet.TorusL2 d →ₗᵢ[ℝ]
    OperatorRidgelet.TorusL2 d

The translation `(τ_z x)(t) = x(t - z)` on `L²(𝕋^d; ℝ)`, a linear isometry.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.torusTranslateC (d : ℕ)
  (z : OperatorRidgelet.Torus d) :
  OperatorRidgelet.TorusL2C d →ₗᵢ[ℂ] OperatorRidgelet.TorusL2C d

def OperatorRidgelet.torusTranslateC (d : ℕ)
  (z : OperatorRidgelet.Torus d) :
  OperatorRidgelet.TorusL2C d →ₗᵢ[ℂ]
    OperatorRidgelet.TorusL2C d

The translation `(τ_z u)(t) = u(t - z)` on `L²(𝕋^d)`, a linear isometry.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.convDirection {d : ℕ} (k : OperatorRidgelet.TorusL2 d)
  (y : OperatorRidgelet.Torus d) : OperatorRidgelet.TorusL2 d

def OperatorRidgelet.convDirection {d : ℕ}
  (k : OperatorRidgelet.TorusL2 d)
  (y : OperatorRidgelet.Torus d) :
  OperatorRidgelet.TorusL2 d

The direction `a_y = k(y - ·)` of the convolution layer.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.convOutput {d : ℕ} (ψ : OperatorRidgelet.TorusL2 d)
  (y : OperatorRidgelet.Torus d) : OperatorRidgelet.TorusL2C d

def OperatorRidgelet.convOutput {d : ℕ}
  (ψ : OperatorRidgelet.TorusL2 d)
  (y : OperatorRidgelet.Torus d) :
  OperatorRidgelet.TorusL2C d

The output `b_y = ψ(· - y)` of the convolution layer, as an element of `L²(𝕋^d)`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.torusOne (d : ℕ) : OperatorRidgelet.TorusL2C d

def OperatorRidgelet.torusOne (d : ℕ) :
  OperatorRidgelet.TorusL2C d

The constant function `1` in `L²(𝕋^d)`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.torusCharacter {d : ℕ} (n : Fin d → ℤ)
  (t : OperatorRidgelet.Torus d) : ℂ

def OperatorRidgelet.torusCharacter {d : ℕ}
  (n : Fin d → ℤ)
  (t : OperatorRidgelet.Torus d) : ℂ

The character `e_n(t) = e^{i⟨n,t⟩}` of `𝕋^d`, `n ∈ ℤ^d`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.torusFourierCoeff {d : ℕ}
  (f : OperatorRidgelet.Torus d → ℂ) (n : Fin d → ℤ) : ℂ

def OperatorRidgelet.torusFourierCoeff {d : ℕ}
  (f : OperatorRidgelet.Torus d → ℂ)
  (n : Fin d → ℤ) : ℂ

The Fourier coefficient `f̂(n) = ∫ f(t) e^{-i⟨n,t⟩} dt` of a function on `𝕋^d` (normalized
Haar measure).

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.torusFreqNormSq {d : ℕ} (n : Fin d → ℤ) : ℝ

def OperatorRidgelet.torusFreqNormSq {d : ℕ}
  (n : Fin d → ℤ) : ℝ

`|n|² = ∑ n_j²` for a frequency `n ∈ ℤ^d`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.besselOperator (d : ℕ) (s : ℝ) :
  OperatorRidgelet.TorusL2 d →L[ℝ] OperatorRidgelet.TorusL2 d

def OperatorRidgelet.besselOperator (d : ℕ)
  (s : ℝ) :
  OperatorRidgelet.TorusL2 d →L[ℝ]
    OperatorRidgelet.TorusL2 d

The Bessel operator `(I - Δ)^{-s}` on `L²(𝕋^d; ℝ)`: the bounded operator that multiplies the
`n`-th Fourier coefficient by `(1 + |n|²)^{-s}` (chosen among the operators with this
property, which determines it; `0` if there is none).

Proposition6.4.4

Statement uses 6

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

Let k,\psi\in L^2(\mathbb T^d;\mathbb R), a_y=k(y-\cdot), and b_y=\psi(\cdot-y). Then \langle a_y,x\rangle=(k*x)(y) (i), the layer is \mathcal F(x)=\psi*\beta(k*x) (ii), \|A\|_\infty=\|k\|_2 (iii), \int\|b_y\|\mathrm dy=\|\psi\|_2 (iv), the standing hypotheses hold (v), and \mathcal F commutes with all translations (vi) and with every isometry of \mathbb T^d fixing k and \psi (vii). If \widehat k(n)\ne0 for infinitely many n, then A has infinite rank (viii); with \varphi\equiv1, F_1(x)=\widehat\psi(0)\int_{\mathbb T^d}\beta((k*x)(y))\mathrm dy (ix), which is not cylindrical when moreover \widehat\psi(0)\ne0 (x). The operator (I-\Delta)^{-s} with s>d/2 is an injective trace-class covariance (xi) and translation invariant (xii), and for Q=P=(I-\Delta)^{-s} the transform is equivariant: R_\rho[f\circ\tau_z](a,c)=R_\rho f(\tau_za,c) (xiii).

Lean code for Proposition6.4.4●13 theorems

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_convolution_i (d : ℕ)
  (k x : OperatorRidgelet.TorusL2 d) (y : OperatorRidgelet.Torus d) :
  inner ℝ (OperatorRidgelet.convDirection k y) x =
    ∫ (t : OperatorRidgelet.Torus d),
      ↑↑k (y - t) * ↑↑x t ∂OperatorRidgelet.torusHaar d

theorem OperatorRidgelet.Paper.ex_convolution_i
  (d : ℕ)
  (k x : OperatorRidgelet.TorusL2 d)
  (y : OperatorRidgelet.Torus d) :
  inner ℝ
      (OperatorRidgelet.convDirection k y)
      x =
    ∫ (t : OperatorRidgelet.Torus d),
      ↑↑k (y - t) *
        ↑↑x
          t ∂OperatorRidgelet.torusHaar d

**Example [ex:convolution]** Periodic convolution layer.  With `a_y = k(y - ·)`,
`⟨a_y, x⟩ = (k * x)(y)`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_convolution_ii (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d) (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp : OperatorRidgelet.HasPolynomialGrowth β)
  (x : OperatorRidgelet.TorusL2 d) :
  ↑↑(OperatorRidgelet.operatorLayer (OperatorRidgelet.torusHaar d)
          (OperatorRidgelet.convDirection k)
          (OperatorRidgelet.convOutput ψ) β
          x) =ᵐ[OperatorRidgelet.torusHaar d]
    fun t =>
    ∫ (y : OperatorRidgelet.Torus d),
      ↑(↑↑ψ (t - y) *
          β
            (inner ℝ (OperatorRidgelet.convDirection k y)
              x)) ∂OperatorRidgelet.torusHaar d

theorem OperatorRidgelet.Paper.ex_convolution_ii
  (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d)
  (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp :
    OperatorRidgelet.HasPolynomialGrowth
      β)
  (x : OperatorRidgelet.TorusL2 d) :
  ↑↑(OperatorRidgelet.operatorLayer
          (OperatorRidgelet.torusHaar d)
          (OperatorRidgelet.convDirection
            k)
          (OperatorRidgelet.convOutput ψ)
          β
          x) =ᵐ[OperatorRidgelet.torusHaar
      d]
    fun t =>
    ∫ (y : OperatorRidgelet.Torus d),
      ↑(↑↑ψ (t - y) *
          β
            (inner ℝ
              (OperatorRidgelet.convDirection
                k y)
              x)) ∂OperatorRidgelet.torusHaar
        d

**Example [ex:convolution]** Periodic convolution layer.  With `a_y = k(y - ·)` and
`b_y = ψ(· - y)`, the layer is `ℱ(x) = ψ * β(k * x)`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_convolution_iii (d : ℕ)
  (k : OperatorRidgelet.TorusL2 d) :
  OperatorRidgelet.layerSupNorm (OperatorRidgelet.convDirection k) = ‖k‖

theorem OperatorRidgelet.Paper.ex_convolution_iii
  (d : ℕ)
  (k : OperatorRidgelet.TorusL2 d) :
  OperatorRidgelet.layerSupNorm
      (OperatorRidgelet.convDirection k) =
    ‖k‖

**Example [ex:convolution]** Periodic convolution layer.  `‖A‖_∞ = ‖k‖₂`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_convolution_iv (d : ℕ)
  (ψ : OperatorRidgelet.TorusL2 d) :
  ∫ (y : OperatorRidgelet.Torus d),
      ‖OperatorRidgelet.convOutput ψ y‖ ∂OperatorRidgelet.torusHaar d =
    ‖ψ‖

theorem OperatorRidgelet.Paper.ex_convolution_iv
  (d : ℕ)
  (ψ : OperatorRidgelet.TorusL2 d) :
  ∫ (y : OperatorRidgelet.Torus d),
      ‖OperatorRidgelet.convOutput ψ
          y‖ ∂OperatorRidgelet.torusHaar
        d =
    ‖ψ‖

**Example [ex:convolution]** Periodic convolution layer.  `∫ ‖b_y‖ dy = ‖ψ‖₂`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_convolution_v (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d) :
  OperatorRidgelet.IsLayerData (OperatorRidgelet.torusHaar d)
    (OperatorRidgelet.convDirection k) (OperatorRidgelet.convOutput ψ)

theorem OperatorRidgelet.Paper.ex_convolution_v
  (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d) :
  OperatorRidgelet.IsLayerData
    (OperatorRidgelet.torusHaar d)
    (OperatorRidgelet.convDirection k)
    (OperatorRidgelet.convOutput ψ)

**Example [ex:convolution]** Periodic convolution layer.  The convolution layer satisfies the
standing hypotheses of the neural-operator layer (`y ↦ a_y`, `y ↦ b_y` are continuous and
bounded into `L²`), so Example `ex:operator-layer` applies.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_convolution_vi (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d) (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp : OperatorRidgelet.HasPolynomialGrowth β)
  (z : OperatorRidgelet.Torus d) (x : OperatorRidgelet.TorusL2 d) :
  OperatorRidgelet.operatorLayer (OperatorRidgelet.torusHaar d)
      (OperatorRidgelet.convDirection k) (OperatorRidgelet.convOutput ψ)
      β ((OperatorRidgelet.torusTranslate d z) x) =
    (OperatorRidgelet.torusTranslateC d z)
      (OperatorRidgelet.operatorLayer (OperatorRidgelet.torusHaar d)
        (OperatorRidgelet.convDirection k)
        (OperatorRidgelet.convOutput ψ) β x)

theorem OperatorRidgelet.Paper.ex_convolution_vi
  (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d)
  (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp :
    OperatorRidgelet.HasPolynomialGrowth
      β)
  (z : OperatorRidgelet.Torus d)
  (x : OperatorRidgelet.TorusL2 d) :
  OperatorRidgelet.operatorLayer
      (OperatorRidgelet.torusHaar d)
      (OperatorRidgelet.convDirection k)
      (OperatorRidgelet.convOutput ψ) β
      ((OperatorRidgelet.torusTranslate d
          z)
        x) =
    (OperatorRidgelet.torusTranslateC d z)
      (OperatorRidgelet.operatorLayer
        (OperatorRidgelet.torusHaar d)
        (OperatorRidgelet.convDirection k)
        (OperatorRidgelet.convOutput ψ) β
        x)

**Example [ex:convolution]** Periodic convolution layer.  `ℱ` commutes with all translations
of `𝕋^d`: `ℱ(τ_z x) = τ_z ℱ(x)`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_convolution_vii (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d) (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp : OperatorRidgelet.HasPolynomialGrowth β)
  (σ : OperatorRidgelet.Torus d ≃+ OperatorRidgelet.Torus d) :
  Isometry ⇑σ →
    ∀
      (hσ :
        MeasureTheory.MeasurePreserving (⇑σ)
          (OperatorRidgelet.torusHaar d)
          (OperatorRidgelet.torusHaar d)),
      (fun t => ↑↑k (σ t)) =ᵐ[OperatorRidgelet.torusHaar d] ↑↑k →
        (fun t => ↑↑ψ (σ t)) =ᵐ[OperatorRidgelet.torusHaar d] ↑↑ψ →
          ∀ (x : OperatorRidgelet.TorusL2 d),
            OperatorRidgelet.operatorLayer
                (OperatorRidgelet.torusHaar d)
                (OperatorRidgelet.convDirection k)
                (OperatorRidgelet.convOutput ψ) β
                ((MeasureTheory.Lp.compMeasurePreserving (⇑σ) hσ) x) =
              (MeasureTheory.Lp.compMeasurePreserving (⇑σ) hσ)
                (OperatorRidgelet.operatorLayer
                  (OperatorRidgelet.torusHaar d)
                  (OperatorRidgelet.convDirection k)
                  (OperatorRidgelet.convOutput ψ) β x)

theorem OperatorRidgelet.Paper.ex_convolution_vii
  (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d)
  (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp :
    OperatorRidgelet.HasPolynomialGrowth
      β)
  (σ :
    OperatorRidgelet.Torus d ≃+
      OperatorRidgelet.Torus d) :
  Isometry ⇑σ →
    ∀
      (hσ :
        MeasureTheory.MeasurePreserving
          (⇑σ)
          (OperatorRidgelet.torusHaar d)
          (OperatorRidgelet.torusHaar d)),
      (fun t =>
            ↑↑k
              (σ
                t)) =ᵐ[OperatorRidgelet.torusHaar
            d]
          ↑↑k →
        (fun t =>
              ↑↑ψ
                (σ
                  t)) =ᵐ[OperatorRidgelet.torusHaar
              d]
            ↑↑ψ →
          ∀
            (x :
              OperatorRidgelet.TorusL2 d),
            OperatorRidgelet.operatorLayer
                (OperatorRidgelet.torusHaar
                  d)
                (OperatorRidgelet.convDirection
                  k)
                (OperatorRidgelet.convOutput
                  ψ)
                β
                ((MeasureTheory.Lp.compMeasurePreserving
                    (⇑σ) hσ)
                  x) =
              (MeasureTheory.Lp.compMeasurePreserving
                  (⇑σ) hσ)
                (OperatorRidgelet.operatorLayer
                  (OperatorRidgelet.torusHaar
                    d)
                  (OperatorRidgelet.convDirection
                    k)
                  (OperatorRidgelet.convOutput
                    ψ)
                  β x)

**Example [ex:convolution]** Periodic convolution layer.  `ℱ` commutes with every isometry
`σ` of `𝕋^d` (an isometric automorphism of the group, measure preserving) that fixes `k` and
`ψ`: `ℱ(x ∘ σ) = ℱ(x) ∘ σ`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_convolution_viii (d : ℕ)
  (k : OperatorRidgelet.TorusL2 d)
  (hk :
    {n |
        OperatorRidgelet.torusFourierCoeff (fun t => ↑(↑↑k t)) n ≠
          0}.Infinite) :
  OperatorRidgelet.HasInfiniteRank
    (OperatorRidgelet.layerA (OperatorRidgelet.torusHaar d)
      (OperatorRidgelet.convDirection k))

theorem OperatorRidgelet.Paper.ex_convolution_viii
  (d : ℕ) (k : OperatorRidgelet.TorusL2 d)
  (hk :
    {n |
        OperatorRidgelet.torusFourierCoeff
            (fun t => ↑(↑↑k t)) n ≠
          0}.Infinite) :
  OperatorRidgelet.HasInfiniteRank
    (OperatorRidgelet.layerA
      (OperatorRidgelet.torusHaar d)
      (OperatorRidgelet.convDirection k))

**Example [ex:convolution]** Periodic convolution layer.  If `k̂(n) ≠ 0` for infinitely many
`n ∈ ℤ^d`, then `A` has infinite rank.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_convolution_ix (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d) (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp : OperatorRidgelet.HasPolynomialGrowth β)
  (x : OperatorRidgelet.TorusL2 d) :
  OperatorRidgelet.layerObservable (OperatorRidgelet.torusHaar d)
      (OperatorRidgelet.convDirection k) (OperatorRidgelet.convOutput ψ)
      β (OperatorRidgelet.torusOne d) x =
    OperatorRidgelet.torusFourierCoeff (fun t => ↑(↑↑ψ t)) 0 *
      ∫ (y : OperatorRidgelet.Torus d),
        ↑(β
            (inner ℝ (OperatorRidgelet.convDirection k y)
              x)) ∂OperatorRidgelet.torusHaar d

theorem OperatorRidgelet.Paper.ex_convolution_ix
  (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d)
  (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp :
    OperatorRidgelet.HasPolynomialGrowth
      β)
  (x : OperatorRidgelet.TorusL2 d) :
  OperatorRidgelet.layerObservable
      (OperatorRidgelet.torusHaar d)
      (OperatorRidgelet.convDirection k)
      (OperatorRidgelet.convOutput ψ) β
      (OperatorRidgelet.torusOne d) x =
    OperatorRidgelet.torusFourierCoeff
        (fun t => ↑(↑↑ψ t)) 0 *
      ∫ (y : OperatorRidgelet.Torus d),
        ↑(β
            (inner ℝ
              (OperatorRidgelet.convDirection
                k y)
              x)) ∂OperatorRidgelet.torusHaar
          d

**Example [ex:convolution]** Periodic convolution layer.  With `φ ≡ 1` the observable is
`F_1(x) = ψ̂(0) ∫ β((k * x)(y)) dy`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_convolution_x (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d)
  (hk :
    {n |
        OperatorRidgelet.torusFourierCoeff (fun t => ↑(↑↑k t)) n ≠
          0}.Infinite)
  (hψ : OperatorRidgelet.torusFourierCoeff (fun t => ↑(↑↑ψ t)) 0 ≠ 0) :
  ¬OperatorRidgelet.IsCylindrical
      (OperatorRidgelet.layerObservable (OperatorRidgelet.torusHaar d)
        (OperatorRidgelet.convDirection k)
        (OperatorRidgelet.convOutput ψ) OperatorRidgelet.gaussianFun
        (OperatorRidgelet.torusOne d))

theorem OperatorRidgelet.Paper.ex_convolution_x
  (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d)
  (hk :
    {n |
        OperatorRidgelet.torusFourierCoeff
            (fun t => ↑(↑↑k t)) n ≠
          0}.Infinite)
  (hψ :
    OperatorRidgelet.torusFourierCoeff
        (fun t => ↑(↑↑ψ t)) 0 ≠
      0) :
  ¬OperatorRidgelet.IsCylindrical
      (OperatorRidgelet.layerObservable
        (OperatorRidgelet.torusHaar d)
        (OperatorRidgelet.convDirection k)
        (OperatorRidgelet.convOutput ψ)
        OperatorRidgelet.gaussianFun
        (OperatorRidgelet.torusOne d))

**Example [ex:convolution]** Periodic convolution layer.  If `k̂(n) ≠ 0` for infinitely many
`n` and `ψ̂(0) ≠ 0`, then the observable `F_1` of the Gaussian-activation layer is not
cylindrical.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_convolution_xi (d : ℕ) (s : ℝ)
  (hs : ↑d / 2 < s) :
  OperatorRidgelet.IsTraceClassCovariance
    (OperatorRidgelet.besselOperator d s)

theorem OperatorRidgelet.Paper.ex_convolution_xi
  (d : ℕ) (s : ℝ) (hs : ↑d / 2 < s) :
  OperatorRidgelet.IsTraceClassCovariance
    (OperatorRidgelet.besselOperator d s)

**Example [ex:convolution]** Periodic convolution layer.  For `s > d/2`, the operator
`(I - Δ)^{-s}` is injective, positive, self-adjoint, and trace class.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_convolution_xii (d : ℕ) (s : ℝ)
  (hs : ↑d / 2 < s) (z : OperatorRidgelet.Torus d)
  (x : OperatorRidgelet.TorusL2 d) :
  (OperatorRidgelet.besselOperator d s)
      ((OperatorRidgelet.torusTranslate d z) x) =
    (OperatorRidgelet.torusTranslate d z)
      ((OperatorRidgelet.besselOperator d s) x)

theorem OperatorRidgelet.Paper.ex_convolution_xii
  (d : ℕ) (s : ℝ) (hs : ↑d / 2 < s)
  (z : OperatorRidgelet.Torus d)
  (x : OperatorRidgelet.TorusL2 d) :
  (OperatorRidgelet.besselOperator d s)
      ((OperatorRidgelet.torusTranslate d
          z)
        x) =
    (OperatorRidgelet.torusTranslate d z)
      ((OperatorRidgelet.besselOperator d
          s)
        x)

**Example [ex:convolution]** Periodic convolution layer.  `(I - Δ)^{-s}` is translation
invariant: `(I - Δ)^{-s} τ_z = τ_z (I - Δ)^{-s}`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_convolution_xiii (d : ℕ) (s : ℝ)
  (hs : ↑d / 2 < s) [MeasurableSpace (OperatorRidgelet.TorusL2 d)]
  [BorelSpace (OperatorRidgelet.TorusL2 d)]
  (μ : MeasureTheory.Measure (OperatorRidgelet.TorusL2 d))
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian
      (OperatorRidgelet.besselOperator d s) μ)
  (ρ : SchwartzMap ℝ ℝ) (f : OperatorRidgelet.TorusL2 d → ℂ)
  (hf : MeasureTheory.Integrable f μ) (z : OperatorRidgelet.Torus d)
  (p : OperatorRidgelet.TorusL2 d × ℝ) :
  OperatorRidgelet.ridgelet μ (⇑ρ)
      (fun x => f ((OperatorRidgelet.torusTranslate d z) x)) p =
    OperatorRidgelet.ridgelet μ (⇑ρ) f
      ((OperatorRidgelet.torusTranslate d z) p.1, p.2)

theorem OperatorRidgelet.Paper.ex_convolution_xiii
  (d : ℕ) (s : ℝ) (hs : ↑d / 2 < s)
  [MeasurableSpace
      (OperatorRidgelet.TorusL2 d)]
  [BorelSpace
      (OperatorRidgelet.TorusL2 d)]
  (μ :
    MeasureTheory.Measure
      (OperatorRidgelet.TorusL2 d))
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian
      (OperatorRidgelet.besselOperator d
        s)
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (f : OperatorRidgelet.TorusL2 d → ℂ)
  (hf : MeasureTheory.Integrable f μ)
  (z : OperatorRidgelet.Torus d)
  (p : OperatorRidgelet.TorusL2 d × ℝ) :
  OperatorRidgelet.ridgelet μ (⇑ρ)
      (fun x =>
        f
          ((OperatorRidgelet.torusTranslate
              d z)
            x))
      p =
    OperatorRidgelet.ridgelet μ (⇑ρ) f
      ((OperatorRidgelet.torusTranslate d
            z)
          p.1,
        p.2)

**Example [ex:convolution]** Periodic convolution layer.  With `Q = P = (I - Δ)^{-s}`,
`s > d/2`, the transform is equivariant: `R_ρ[f ∘ τ_z](a,c) = R_ρ f(τ_z a, c)` for every
translation `τ_z` and every `f ∈ L¹(μ_Q)`.

Proof for Proposition 6.4.4

uses 0

With normalized Haar measure \|a_y\|=\|k\|_2 and \|b_y\|=\|\psi\|_2, convolutions commute with translations and with isometries fixing their kernels, \beta acts pointwise, A is diagonal in the Fourier basis with entries \widehat k(n), w_1=\widehat\psi(0) is a nonzero constant so Proposition 6.4.2 (iv) applies, and (I-\Delta)^{-s} has eigenvalues (1+|n|^2)^{-s}, summable for s>d/2.

Definition6.4.5

Statement uses 2

Statement dependency previews

Preview

Definition 6.1.5

Loading preview

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

used by 1✓L∃∀N

The interval \Omega=(0,1) with Lebesgue measure, H=Y=L^2(0,1), the Green kernel g(y,t)=\sinh(\min(y,t))\sinh(1-\max(y,t))/\sinh1, the layer data a_y=b_y=g(y,\cdot), the Dirichlet solution operator \mathsf G=(I-\partial_t^2)^{-1} as the integral operator with kernel g, its eigenvalues \lambda_n=(1+\pi^2n^2)^{-1} and eigenfunctions e_n(t)=\sqrt2\sin(n\pi t), and the 2N-neuron ReLU truncation \mathsf G_Nx=\sum_{n=1}^N\lambda_n[\operatorname{ReLU}(\langle e_n,x\rangle)-\operatorname{ReLU}(-\langle e_n,x\rangle)]e_n.

Lean code for Definition6.4.5●13 definitions

abbrevdefined in OperatorRidgelet/Examples/Defs.lean

complete

abbrev OperatorRidgelet.UnitOpenInterval : Type

abbrev OperatorRidgelet.UnitOpenInterval : Type

The open interval `(0,1)` as a measure space (Lebesgue measure).

abbrevdefined in OperatorRidgelet/Examples/Defs.lean

complete

abbrev OperatorRidgelet.UnitL2 : Type

abbrev OperatorRidgelet.UnitL2 : Type

`L²(0,1)`, real valued: the input space of the Dirichlet example.

abbrevdefined in OperatorRidgelet/Examples/Defs.lean

complete

abbrev OperatorRidgelet.UnitL2C : Type

abbrev OperatorRidgelet.UnitL2C : Type

`L²(0,1)`, complex valued: the output space of the Dirichlet example.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.dirichletKernel (y t : ℝ) : ℝ

def OperatorRidgelet.dirichletKernel
  (y t : ℝ) : ℝ

The Green kernel `g(y,t) = sinh(min(y,t)) sinh(1 - max(y,t)) / sinh 1` of
`(I - ∂_t²)^{-1}` with Dirichlet boundary conditions.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.dirichletKernelFn (y : ℝ) : OperatorRidgelet.UnitL2

def OperatorRidgelet.dirichletKernelFn
  (y : ℝ) : OperatorRidgelet.UnitL2

`g(y, ·)` as an element of `L²(0,1)`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.dirichletDirection
  (y : OperatorRidgelet.UnitOpenInterval) : OperatorRidgelet.UnitL2

def OperatorRidgelet.dirichletDirection
  (y :
    OperatorRidgelet.UnitOpenInterval) :
  OperatorRidgelet.UnitL2

The direction `a_y = g(y,·)` of the Dirichlet layer, `y ∈ (0,1)`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.dirichletOutput
  (y : OperatorRidgelet.UnitOpenInterval) : OperatorRidgelet.UnitL2C

def OperatorRidgelet.dirichletOutput
  (y :
    OperatorRidgelet.UnitOpenInterval) :
  OperatorRidgelet.UnitL2C

The output `b_y = g(y,·)` of the Dirichlet layer, as an element of `L²(0,1)` (complex).

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.dirichletSolution (x : ℝ → ℝ) (y : ℝ) : ℝ

def OperatorRidgelet.dirichletSolution
  (x : ℝ → ℝ) (y : ℝ) : ℝ

The solution `u(y) = ∫₀¹ g(y,t) x(t) dt` of `-u'' + u = x`, `u(0) = u(1) = 0`, for a
function `x`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.integralOperator.{u_1} {α : Type u_1}
  [MeasurableSpace α] (m : MeasureTheory.Measure α) (k : α → α → ℝ) :
  ↥(MeasureTheory.Lp ℝ 2 m) →L[ℝ] ↥(MeasureTheory.Lp ℝ 2 m)

def OperatorRidgelet.integralOperator.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (m : MeasureTheory.Measure α)
  (k : α → α → ℝ) :
  ↥(MeasureTheory.Lp ℝ 2 m) →L[ℝ]
    ↥(MeasureTheory.Lp ℝ 2 m)

The integral operator on `L²(m)` with kernel `k`: the bounded operator `T` with
`(Tx)(y) = ∫ k(y,t) x(t) m(dt)` a.e. (which determines it; `0` if there is none).

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.dirichletOperator :
  OperatorRidgelet.UnitL2 →L[ℝ] OperatorRidgelet.UnitL2

def OperatorRidgelet.dirichletOperator :
  OperatorRidgelet.UnitL2 →L[ℝ]
    OperatorRidgelet.UnitL2

The Dirichlet solution operator `𝖦 = (I - ∂_t²)^{-1}` on `L²(0,1)`, the integral operator
with kernel `g`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.dirichletEigenvalue (n : ℕ) : ℝ

def OperatorRidgelet.dirichletEigenvalue
  (n : ℕ) : ℝ

The eigenvalues `λ_n = (1 + π²n²)⁻¹` of `𝖦`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.dirichletEigenfunction (n : ℕ) :
  OperatorRidgelet.UnitL2

def OperatorRidgelet.dirichletEigenfunction
  (n : ℕ) : OperatorRidgelet.UnitL2

The eigenfunctions `e_n(t) = √2 sin(nπt)` of `𝖦`, as elements of `L²(0,1)` (`e_0 = 0`).

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.dirichletReLUTruncation (N : ℕ)
  (x : OperatorRidgelet.UnitL2) : OperatorRidgelet.UnitL2

def OperatorRidgelet.dirichletReLUTruncation
  (N : ℕ) (x : OperatorRidgelet.UnitL2) :
  OperatorRidgelet.UnitL2

The `2N`-neuron ReLU truncation
`𝖦_N x = ∑_{n=1}^N λ_n [ReLU(⟨e_n,x⟩) - ReLU(-⟨e_n,x⟩)] e_n` of the exact ReLU network of
`𝖦`.

Proposition6.4.6

Statement uses 5

Statement dependency previews

Preview

Definition 6.1.2

Loading preview

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

used by 0✓L∃∀N

(\mathsf Gx)(y)=\int_0^1g(y,t)x(t)\,\mathrm dt (i) and u=\mathsf Gx solves -u''+u=x, u(0)=u(1)=0 (ii); \mathsf Ge_n=\lambda_ne_n (iii), so \mathsf G is an injective trace-class covariance (iv) of infinite rank (v), and \|A\|_\infty\le\sup_y\|g(y,\cdot)\|_2<\infty (vi). With a_y=b_y=g(y,\cdot) the neural-operator layer example applies (vii) and the layer is \mathcal F(x)=\mathsf G\,\beta(\mathsf Gx) (viii), one Picard step for the semilinear equation -u''+u=\beta(u)+x. The linear operator is an exact ReLU network, \mathsf Gx=\sum_n\lambda_ne_n[\operatorname{ReLU}(\langle e_n,x\rangle)-\operatorname{ReLU}(-\langle e_n,x\rangle)] (ix), whose 2N-neuron truncation has error at most \lambda_{N+1}\|x\| (x) with \lambda_{N+1}\le\pi^{-2}(N+1)^{-2} (xi).

Lean code for Proposition6.4.6●11 theorems

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_dirichlet_i (x : OperatorRidgelet.UnitL2) :
  ↑↑(OperatorRidgelet.dirichletOperator x) =ᵐ[MeasureTheory.volume]
    fun y =>
    ∫ (t : OperatorRidgelet.UnitOpenInterval),
      OperatorRidgelet.dirichletKernel ↑y ↑t * ↑↑x t

theorem OperatorRidgelet.Paper.ex_dirichlet_i
  (x : OperatorRidgelet.UnitL2) :
  ↑↑(OperatorRidgelet.dirichletOperator
          x) =ᵐ[MeasureTheory.volume]
    fun y =>
    ∫ (t :
      OperatorRidgelet.UnitOpenInterval),
      OperatorRidgelet.dirichletKernel ↑y
          ↑t *
        ↑↑x t

**Example [ex:dirichlet]** Dirichlet solution operator with a pointwise nonlinearity.  `𝖦` is
the integral operator with kernel `g`: `(𝖦x)(y) = ∫₀¹ g(y,t) x(t) dt`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_dirichlet_ii (x : ℝ → ℝ) (hx : Continuous x) :
  OperatorRidgelet.dirichletSolution x 0 = 0 ∧
    OperatorRidgelet.dirichletSolution x 1 = 0 ∧
      (∀ y ∈ Set.Ioo 0 1,
          DifferentiableAt ℝ (OperatorRidgelet.dirichletSolution x) y) ∧
        ∀ y ∈ Set.Ioo 0 1,
          HasDerivAt (deriv (OperatorRidgelet.dirichletSolution x))
            (OperatorRidgelet.dirichletSolution x y - x y) y

theorem OperatorRidgelet.Paper.ex_dirichlet_ii
  (x : ℝ → ℝ) (hx : Continuous x) :
  OperatorRidgelet.dirichletSolution x 0 =
      0 ∧
    OperatorRidgelet.dirichletSolution x
          1 =
        0 ∧
      (∀ y ∈ Set.Ioo 0 1,
          DifferentiableAt ℝ
            (OperatorRidgelet.dirichletSolution
              x)
            y) ∧
        ∀ y ∈ Set.Ioo 0 1,
          HasDerivAt
            (deriv
              (OperatorRidgelet.dirichletSolution
                x))
            (OperatorRidgelet.dirichletSolution
                x y -
              x y)
            y

**Example [ex:dirichlet]** Dirichlet solution operator with a pointwise nonlinearity.  For a
continuous source `x`, `u = 𝖦x` solves `-u'' + u = x` on `(0,1)` with `u(0) = u(1) = 0`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_dirichlet_iii (n : ℕ) :
  1 ≤ n →
    OperatorRidgelet.dirichletOperator
        (OperatorRidgelet.dirichletEigenfunction n) =
      OperatorRidgelet.dirichletEigenvalue n •
        OperatorRidgelet.dirichletEigenfunction n

theorem OperatorRidgelet.Paper.ex_dirichlet_iii
  (n : ℕ) :
  1 ≤ n →
    OperatorRidgelet.dirichletOperator
        (OperatorRidgelet.dirichletEigenfunction
          n) =
      OperatorRidgelet.dirichletEigenvalue
          n •
        OperatorRidgelet.dirichletEigenfunction
          n

**Example [ex:dirichlet]** Dirichlet solution operator with a pointwise nonlinearity.  `𝖦` has
the eigenpairs `λ_n = (1 + π²n²)⁻¹`, `e_n(t) = √2 sin(nπt)`, `n ≥ 1`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_dirichlet_iv :
  OperatorRidgelet.IsTraceClassCovariance
    OperatorRidgelet.dirichletOperator

theorem OperatorRidgelet.Paper.ex_dirichlet_iv :
  OperatorRidgelet.IsTraceClassCovariance
    OperatorRidgelet.dirichletOperator

**Example [ex:dirichlet]** Dirichlet solution operator with a pointwise nonlinearity.  `𝖦` is
injective, positive, self-adjoint, and trace class.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_dirichlet_v :
  OperatorRidgelet.HasInfiniteRank ↑OperatorRidgelet.dirichletOperator

theorem OperatorRidgelet.Paper.ex_dirichlet_v :
  OperatorRidgelet.HasInfiniteRank
    ↑OperatorRidgelet.dirichletOperator

**Example [ex:dirichlet]** Dirichlet solution operator with a pointwise nonlinearity.  `𝖦` has
infinite rank.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_dirichlet_vi :
  BddAbove (Set.range fun y => ‖OperatorRidgelet.dirichletDirection y‖)

theorem OperatorRidgelet.Paper.ex_dirichlet_vi :
  BddAbove
    (Set.range fun y =>
      ‖OperatorRidgelet.dirichletDirection
          y‖)

**Example [ex:dirichlet]** Dirichlet solution operator with a pointwise nonlinearity.
`‖A‖_∞ ≤ sup_y ‖g(y,·)‖₂ < ∞`: the directions `a_y = g(y,·)` are bounded in `L²(0,1)`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_dirichlet_vii :
  OperatorRidgelet.IsLayerData MeasureTheory.volume
    OperatorRidgelet.dirichletDirection OperatorRidgelet.dirichletOutput

theorem OperatorRidgelet.Paper.ex_dirichlet_vii :
  OperatorRidgelet.IsLayerData
    MeasureTheory.volume
    OperatorRidgelet.dirichletDirection
    OperatorRidgelet.dirichletOutput

**Example [ex:dirichlet]** Dirichlet solution operator with a pointwise nonlinearity.  With
`a_y = b_y = g(y,·)` the standing hypotheses of the neural-operator layer hold, so Example
`ex:operator-layer` applies.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_dirichlet_viii (β : ℝ → ℝ)
  (hβc : Continuous β) (hβp : OperatorRidgelet.HasPolynomialGrowth β)
  (x : OperatorRidgelet.UnitL2) :
  OperatorRidgelet.operatorLayer MeasureTheory.volume
      OperatorRidgelet.dirichletDirection
      OperatorRidgelet.dirichletOutput β x =
    Complex.ofRealCLM.compLp
      (OperatorRidgelet.dirichletOperator
        (OperatorRidgelet.toLpOrZero 2 MeasureTheory.volume fun t =>
          β (↑↑(OperatorRidgelet.dirichletOperator x) t)))

theorem OperatorRidgelet.Paper.ex_dirichlet_viii
  (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp :
    OperatorRidgelet.HasPolynomialGrowth
      β)
  (x : OperatorRidgelet.UnitL2) :
  OperatorRidgelet.operatorLayer
      MeasureTheory.volume
      OperatorRidgelet.dirichletDirection
      OperatorRidgelet.dirichletOutput β
      x =
    Complex.ofRealCLM.compLp
      (OperatorRidgelet.dirichletOperator
        (OperatorRidgelet.toLpOrZero 2
          MeasureTheory.volume fun t =>
          β
            (↑↑(OperatorRidgelet.dirichletOperator
                    x)
              t)))

**Example [ex:dirichlet]** Dirichlet solution operator with a pointwise nonlinearity.  With
`a_y = b_y = g(y,·)` the layer is `ℱ(x) = 𝖦 β(𝖦x)`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_dirichlet_ix (x : OperatorRidgelet.UnitL2) :
  HasSum
    (fun n =>
      (OperatorRidgelet.dirichletEigenvalue n *
          (LeanRidgelet.relu
              (inner ℝ (OperatorRidgelet.dirichletEigenfunction n) x) -
            LeanRidgelet.relu
              (-inner ℝ (OperatorRidgelet.dirichletEigenfunction n)
                  x))) •
        OperatorRidgelet.dirichletEigenfunction n)
    (OperatorRidgelet.dirichletOperator x)

theorem OperatorRidgelet.Paper.ex_dirichlet_ix
  (x : OperatorRidgelet.UnitL2) :
  HasSum
    (fun n =>
      (OperatorRidgelet.dirichletEigenvalue
            n *
          (LeanRidgelet.relu
              (inner ℝ
                (OperatorRidgelet.dirichletEigenfunction
                  n)
                x) -
            LeanRidgelet.relu
              (-inner ℝ
                  (OperatorRidgelet.dirichletEigenfunction
                    n)
                  x))) •
        OperatorRidgelet.dirichletEigenfunction
          n)
    (OperatorRidgelet.dirichletOperator x)

**Example [ex:dirichlet]** Dirichlet solution operator with a pointwise nonlinearity.  `𝖦` is
the exact ReLU network `𝖦x = ∑_n λ_n e_n [ReLU(⟨e_n,x⟩) - ReLU(-⟨e_n,x⟩)]`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_dirichlet_x (n : ℕ)
  (x : OperatorRidgelet.UnitL2) :
  ‖OperatorRidgelet.dirichletOperator x -
        OperatorRidgelet.dirichletReLUTruncation n x‖ ≤
    OperatorRidgelet.dirichletEigenvalue (n + 1) * ‖x‖

theorem OperatorRidgelet.Paper.ex_dirichlet_x
  (n : ℕ) (x : OperatorRidgelet.UnitL2) :
  ‖OperatorRidgelet.dirichletOperator x -
        OperatorRidgelet.dirichletReLUTruncation
          n x‖ ≤
    OperatorRidgelet.dirichletEigenvalue
        (n + 1) *
      ‖x‖

**Example [ex:dirichlet]** Dirichlet solution operator with a pointwise nonlinearity.  The
`2N`-neuron truncation has error `‖𝖦x - 𝖦_N x‖ ≤ λ_{N+1} ‖x‖`, uniformly on bounded sets.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_dirichlet_xi (n : ℕ) :
  OperatorRidgelet.dirichletEigenvalue (n + 1) ≤
    (Real.pi ^ 2 * (↑n + 1) ^ 2)⁻¹

theorem OperatorRidgelet.Paper.ex_dirichlet_xi
  (n : ℕ) :
  OperatorRidgelet.dirichletEigenvalue
      (n + 1) ≤
    (Real.pi ^ 2 * (↑n + 1) ^ 2)⁻¹

**Example [ex:dirichlet]** Dirichlet solution operator with a pointwise nonlinearity.  The
truncation error is `O(N^{-2})`: `λ_{N+1} ≤ π⁻² (N+1)⁻²`.

Proof for Proposition 6.4.6

uses 0

Direct differentiation shows that g(y,\cdot) solves the boundary value problem with a unit jump of the derivative at t=y, the eigenpairs are checked by -e_n''+e_n=(1+\pi^2n^2)e_n, the kernel is continuous and bounded so Proposition 6.4.2 applies, the ReLU expansion is the spectral theorem with u=\operatorname{ReLU}(u)-\operatorname{ReLU}(-u), and orthogonality gives \|\mathsf Gx-\mathsf G_Nx\|^2=\sum_{n>N}\lambda_n^2\langle e_n,x\rangle^2\le\lambda_{N+1}^2\|x\|^2.