1.2. Operator-valued parameters🔗

Networks on function spaces are often written with operator-valued parameters: for an activation \sigma:H\to H, a bounded operator A, and \ell,b\in H, the neuron is \mathrm n_{\ell,A,b}(x)=\langle\ell,\sigma(Ax+b)\rangle. For the rank-one activation \sigma_\beta(y)=\beta(\langle\psi,y\rangle)z the neuron equals \langle\ell,z\rangle\beta(\langle A^*\psi,x\rangle+\langle\psi,b\rangle), so the effective parameter is the scalar ridge parameter \pi_\psi(A,b)=(A^*\psi,\langle\psi,b\rangle). In Lean the projection \pi_\psi is OperatorRidgelet.operatorParameterMap, and the section J_\psi(a,c)=(A_a,b_c) with A_a=\|\psi\|^{-2}\psi\otimes a and b_c=c\|\psi\|^{-2}\psi is OperatorRidgelet.operatorRidgeletSection, built from OperatorRidgelet.rankOneLift and OperatorRidgelet.biasLift.

Definition1.2.1

uses 0

Used by 3

Reverse dependency previews

Preview

Definition 1.2.2

Loading preview

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

✓L∃∀N

The squared Hilbert–Schmidt norm of a bounded operator A on H is the supremum \|A\|_{\mathcal L_2}^2=\sup\{\sum_{e\in s}\|Ae\|^2\} over finite orthonormal families s, and \mathcal L_2(H) is the set of bounded operators with finite Hilbert–Schmidt norm. Mathlib has no Hilbert–Schmidt class; the definition is intrinsic, and the equality with \sum_n\|Ae_n\|^2 along a Hilbert basis is a later obligation.

Lean code for Definition1.2.1●3 definitions

defdefined in OperatorRidgelet/Architecture/Defs.lean

complete

def OperatorRidgelet.hsNormSq.{u_1} {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (A : H →L[ℝ] H) : ENNReal

def OperatorRidgelet.hsNormSq.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  (A : H →L[ℝ] H) : ENNReal

The squared Hilbert–Schmidt norm `‖A‖²_{𝓛₂}` of a bounded operator, in `ℝ≥0∞`: the
supremum over finite orthonormal families `s ⊆ H` of `∑_{e ∈ s} ‖A e‖²`.

defdefined in OperatorRidgelet/Architecture/Defs.lean

complete

def OperatorRidgelet.IsHilbertSchmidt.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (A : H →L[ℝ] H) : Prop

def OperatorRidgelet.IsHilbertSchmidt.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  (A : H →L[ℝ] H) : Prop

`A ∈ 𝓛₂(H)`: the bounded operator `A` is Hilbert–Schmidt.

defdefined in OperatorRidgelet/Architecture/Defs.lean

complete

def OperatorRidgelet.hsNorm.{u_1} {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (A : H →L[ℝ] H) : ℝ

def OperatorRidgelet.hsNorm.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  (A : H →L[ℝ] H) : ℝ

The Hilbert–Schmidt norm `‖A‖_{𝓛₂}` as a real number; it is `0` (junk) when `A` is not
Hilbert–Schmidt.

Definition1.2.2

Statement uses 3

Statement dependency previews

Preview

Definition 1.1.1

Loading preview

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

Used by 5

Reverse dependency previews

Preview

Lemma 1.2.3

Loading preview

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

✓L∃∀N

The operator neuron \mathrm n_{\ell,A,b}(x)=\langle\ell,\sigma(Ax+b)\rangle, the sets of neurons with operator parameter in a given subset of \mathcal L(H) and of scalar ridges x\mapsto\beta(\langle a,x\rangle+c), both as subsets of C(H;\mathbb R) with the compact-open topology, the rank-one activation \sigma_\beta(y)=\beta(\langle\psi,y\rangle)z, the finite-width operator network x\mapsto\sum_jv_j\,\mathrm n_{\ell,A_j,b_j}(x), and the operator synthesis S_{\mathrm{op}}\Gamma_{\mathrm{op}}(x)=\int\mathrm n_{\ell,A,b}(x)\,\Gamma_{\mathrm{op}}(\mathrm dA,\mathrm db) of a finite complex measure on \mathcal L(H)\times H.

Lean code for Definition1.2.2●6 definitions

defdefined in OperatorRidgelet/Architecture/Defs.lean

complete

def OperatorRidgelet.operatorNeuron.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (σ : H → H) (ℓ : H)
  (A : H →L[ℝ] H) (b x : H) : ℝ

def OperatorRidgelet.operatorNeuron.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (σ : H → H)
  (ℓ : H) (A : H →L[ℝ] H) (b x : H) : ℝ

The operator neuron `n_{ℓ,A,b}(x) = ⟪ℓ, σ(A x + b)⟫` with activation `σ : H → H`, readout
`ℓ`, operator parameter `A`, and bias `b`.

defdefined in OperatorRidgelet/Architecture/Defs.lean

complete

def OperatorRidgelet.operatorNeuronSet.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (σ : H → H)
  (P : Set (H →L[ℝ] H)) : Set C(H, ℝ)

def OperatorRidgelet.operatorNeuronSet.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (σ : H → H)
  (P : Set (H →L[ℝ] H)) : Set C(H, ℝ)

The continuous operator neurons `n_{ℓ,A,b}` with operator parameter `A ∈ P`, as a subset of
`C(H, ℝ)`; `P = Set.univ` is `𝓛(H)` and `P = {A | IsHilbertSchmidt A}` is `𝓛₂(H)`.

defdefined in OperatorRidgelet/Architecture/Defs.lean

complete

def OperatorRidgelet.ridgeSet.{u_1} {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (β : ℝ → ℝ) : Set C(H, ℝ)

def OperatorRidgelet.ridgeSet.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (β : ℝ → ℝ) :
  Set C(H, ℝ)

The continuous real ridge functions `x ↦ β(⟪a, x⟫ + c)` with `(a, c) ∈ H × ℝ`, as a subset
of `C(H, ℝ)`.

defdefined in OperatorRidgelet/Architecture/Defs.lean

complete

def OperatorRidgelet.rankOneActivation.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (β : ℝ → ℝ)
  (ψ z y : H) : H

def OperatorRidgelet.rankOneActivation.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (β : ℝ → ℝ)
  (ψ z y : H) : H

The rank-one activation `σ_β(y) = β(⟪ψ, y⟫) z` built from a real scalar activation `β` and
fixed vectors `ψ, z ∈ H`.

defdefined in OperatorRidgelet/Architecture/Defs.lean

complete

def OperatorRidgelet.operatorFiniteNetwork.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] {N : ℕ} (σ : H → H) (ℓ : H)
  (v : Fin N → Y) (A : Fin N → H →L[ℝ] H) (b : Fin N → H) (x : H) : Y

def OperatorRidgelet.operatorFiniteNetwork.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  {N : ℕ} (σ : H → H) (ℓ : H)
  (v : Fin N → Y) (A : Fin N → H →L[ℝ] H)
  (b : Fin N → H) (x : H) : Y

The finite-width operator network `x ↦ ∑_j n_{ℓ,A_j,b_j}(x) • v_j` with values in `Y`.

defdefined in OperatorRidgelet/Architecture/Defs.lean

complete

def OperatorRidgelet.operatorSynthesis.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (σ : H → H) (ℓ : H)
  (Γ :
    MeasureTheory.ComplexMeasure
      (OperatorRidgelet.OperatorRidgeParameter H))
  (x : H) : ℂ

def OperatorRidgelet.operatorSynthesis.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] (σ : H → H) (ℓ : H)
  (Γ :
    MeasureTheory.ComplexMeasure
      (OperatorRidgelet.OperatorRidgeParameter
        H))
  (x : H) : ℂ

The operator synthesis `S_op Γ_op(x) = ∫ n_{ℓ,A,b}(x) Γ_op(dA, db)` of a complex measure
`Γ_op` on operator parameters `(A, b)`: the real neuron is integrated as a complex-valued
function against `Γ_op`, with the same convention as `integralNetwork`.

Lemma1.2.3

Statement uses 2

Statement dependency previews

Preview

Definition 1.2.1

Loading preview

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

used by 0✓L∃∀N

Suppose \sigma:H\to H is globally Lipschitz. The finite linear spans of the neurons \mathrm n_{\ell,A,b} with A\in\mathcal L(H) and with A\in\mathcal L_2(H) have the same compact-open closure in C(H;\mathbb R).

Lean code for Lemma1.2.3●1 theorem

theoremdefined in OperatorRidgelet/Paper/Networks.lean

complete

theorem OperatorRidgelet.Paper.lem_hs_reduction.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] {σ : H → H} {L : NNReal}
  (hσ : LipschitzWith L σ) :
  closure
      ↑(Submodule.span ℝ
          (OperatorRidgelet.operatorNeuronSet σ Set.univ)) =
    closure
      ↑(Submodule.span ℝ
          (OperatorRidgelet.operatorNeuronSet σ
            {A | OperatorRidgelet.IsHilbertSchmidt A}))

theorem OperatorRidgelet.Paper.lem_hs_reduction.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H] {σ : H → H}
  {L : NNReal} (hσ : LipschitzWith L σ) :
  closure
      ↑(Submodule.span ℝ
          (OperatorRidgelet.operatorNeuronSet
            σ Set.univ)) =
    closure
      ↑(Submodule.span ℝ
          (OperatorRidgelet.operatorNeuronSet
            σ
            {A |
              OperatorRidgelet.IsHilbertSchmidt
                A}))

**Lemma [lem:hs-reduction]** Hilbert–Schmidt reduction.  For globally Lipschitz `σ`, the
spans of the operator neurons with `A ∈ 𝓛(H)` and with `A ∈ 𝓛₂(H)` have the same compact-open
closure in `C(H; ℝ)`.

Proof for Lemma 1.2.3

uses 0

Replace A_j by A_j\Pi_n with \Pi_n the projection onto the first n basis vectors; each A_j\Pi_n has finite rank, and strong convergence \Pi_nx\to x is uniform on compact sets by a finite-net argument, so the Lipschitz bound gives convergence in C(K).

Lemma1.2.4

Statement uses 4

Statement dependency previews

Preview

Definition 1.1.1

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Proposition 1.2.5

Loading preview

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

✓L∃∀N

For \psi\ne0 put A_a=\|\psi\|^{-2}\psi\otimes a and b_c=c\|\psi\|^{-2}\psi. Then A_a\in\mathcal L_2(H) (i), \|A_a\|_{\mathcal L_2}=\|a\|/\|\psi\| (ii), \|b_c\|=|c|/\|\psi\| (iii), and \pi_\psi(A_a,b_c)=(a,c) (iv). The section J_\psi(a,c)=(A_a,b_c) is continuous into \mathcal L_2(H)\times H (v), and every scalar integral network (vi) or finite-width network (vii) with activation \beta lifts exactly to the operator architecture with activation \sigma_\beta and readout normalized by \langle\ell,z\rangle=1.

Lean code for Lemma1.2.4●7 theorems

theoremdefined in OperatorRidgelet/Paper/Networks.lean

complete

theorem OperatorRidgelet.Paper.lem_rank_one_lift_i.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] (ψ a : H) :
  OperatorRidgelet.IsHilbertSchmidt (OperatorRidgelet.rankOneLift ψ a)

theorem OperatorRidgelet.Paper.lem_rank_one_lift_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] (ψ a : H) :
  OperatorRidgelet.IsHilbertSchmidt
    (OperatorRidgelet.rankOneLift ψ a)

**Lemma [lem:rank-one-lift]** Exact rank-one lift.  `A_a = ‖ψ‖⁻² ψ ⊗ a` is
Hilbert–Schmidt.

theoremdefined in OperatorRidgelet/Paper/Networks.lean

complete

theorem OperatorRidgelet.Paper.lem_rank_one_lift_ii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {ψ : H} (hψ : ψ ≠ 0)
  (a : H) :
  OperatorRidgelet.hsNorm (OperatorRidgelet.rankOneLift ψ a) = ‖a‖ / ‖ψ‖

theorem OperatorRidgelet.Paper.lem_rank_one_lift_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {ψ : H}
  (hψ : ψ ≠ 0) (a : H) :
  OperatorRidgelet.hsNorm
      (OperatorRidgelet.rankOneLift ψ a) =
    ‖a‖ / ‖ψ‖

**Lemma [lem:rank-one-lift]** Exact rank-one lift.  `‖A_a‖_{𝓛₂} = ‖a‖ / ‖ψ‖`.

theoremdefined in OperatorRidgelet/Paper/Networks.lean

complete

theorem OperatorRidgelet.Paper.lem_rank_one_lift_iii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {ψ : H} (hψ : ψ ≠ 0)
  (c : ℝ) : ‖OperatorRidgelet.biasLift ψ c‖ = |c| / ‖ψ‖

theorem OperatorRidgelet.Paper.lem_rank_one_lift_iii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {ψ : H}
  (hψ : ψ ≠ 0) (c : ℝ) :
  ‖OperatorRidgelet.biasLift ψ c‖ =
    |c| / ‖ψ‖

**Lemma [lem:rank-one-lift]** Exact rank-one lift.  `‖b_c‖ = |c| / ‖ψ‖`.

theoremdefined in OperatorRidgelet/Paper/Networks.lean

complete

theorem OperatorRidgelet.Paper.lem_rank_one_lift_iv.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  {ψ : H} (hψ : ψ ≠ 0) (a : H) (c : ℝ) :
  OperatorRidgelet.operatorParameterMap ψ
      (OperatorRidgelet.operatorRidgeletSection ψ (a, c)) =
    (a, c)

theorem OperatorRidgelet.Paper.lem_rank_one_lift_iv.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] {ψ : H} (hψ : ψ ≠ 0)
  (a : H) (c : ℝ) :
  OperatorRidgelet.operatorParameterMap ψ
      (OperatorRidgelet.operatorRidgeletSection
        ψ (a, c)) =
    (a, c)

**Lemma [lem:rank-one-lift]** Exact rank-one lift.  `π_ψ(A_a, b_c) = (a, c)`.

theoremdefined in OperatorRidgelet/Paper/Networks.lean

complete

theorem OperatorRidgelet.Paper.lem_rank_one_lift_v.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {ψ : H} (hψ : ψ ≠ 0)
  (a : H) (c : ℝ) :
  Filter.Tendsto
    (fun p =>
      OperatorRidgelet.hsNorm
          (OperatorRidgelet.rankOneLift ψ p.1 -
            OperatorRidgelet.rankOneLift ψ a) +
        ‖OperatorRidgelet.biasLift ψ p.2 -
            OperatorRidgelet.biasLift ψ c‖)
    (nhds (a, c)) (nhds 0)

theorem OperatorRidgelet.Paper.lem_rank_one_lift_v.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {ψ : H}
  (hψ : ψ ≠ 0) (a : H) (c : ℝ) :
  Filter.Tendsto
    (fun p =>
      OperatorRidgelet.hsNorm
          (OperatorRidgelet.rankOneLift ψ
              p.1 -
            OperatorRidgelet.rankOneLift ψ
              a) +
        ‖OperatorRidgelet.biasLift ψ p.2 -
            OperatorRidgelet.biasLift ψ
              c‖)
    (nhds (a, c)) (nhds 0)

**Lemma [lem:rank-one-lift]** Exact rank-one lift.  The section `J_ψ(a, c) = (A_a, b_c)` is
continuous into `𝓛₂(H) × H`: the Hilbert–Schmidt distance of the operator components plus the
distance of the biases tends to `0` at every `(a, c)`.

theoremdefined in OperatorRidgelet/Paper/Networks.lean

complete

theorem OperatorRidgelet.Paper.lem_rank_one_lift_vi.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (β : ℝ → ℝ) {ψ z ℓ : H} (hψ : ψ ≠ 0) (hℓz : inner ℝ ℓ z = 1)
  (Γ :
    MeasureTheory.ComplexMeasure
      (OperatorRidgelet.ScalarRidgeParameter H)) :
  OperatorRidgelet.operatorSynthesis
      (OperatorRidgelet.rankOneActivation β ψ z) ℓ
      (MeasureTheory.VectorMeasure.map Γ
        (OperatorRidgelet.operatorRidgeletSection ψ)) =
    OperatorRidgelet.integralNetwork (fun t => ↑(β t)) Γ

theorem OperatorRidgelet.Paper.lem_rank_one_lift_vi.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (β : ℝ → ℝ) {ψ z ℓ : H} (hψ : ψ ≠ 0)
  (hℓz : inner ℝ ℓ z = 1)
  (Γ :
    MeasureTheory.ComplexMeasure
      (OperatorRidgelet.ScalarRidgeParameter
        H)) :
  OperatorRidgelet.operatorSynthesis
      (OperatorRidgelet.rankOneActivation
        β ψ z)
      ℓ
      (MeasureTheory.VectorMeasure.map Γ
        (OperatorRidgelet.operatorRidgeletSection
          ψ)) =
    OperatorRidgelet.integralNetwork
      (fun t => ↑(β t)) Γ

**Lemma [lem:rank-one-lift]** Exact rank-one lift.  Every scalar integral network with
activation `β` lifts exactly to the operator architecture with activation `σ_β` and readout
normalized by `⟪ℓ, z⟫ = 1`: `S_op[(J_ψ)_# Γ] = S_β[Γ]`.

theoremdefined in OperatorRidgelet/Paper/Networks.lean

complete

theorem OperatorRidgelet.Paper.lem_rank_one_lift_vii.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] (β : ℝ → ℝ) {ψ z ℓ : H} (hψ : ψ ≠ 0)
  (hℓz : inner ℝ ℓ z = 1) {N : ℕ} (v : Fin N → Y) (a : Fin N → H)
  (c : Fin N → ℝ) :
  (OperatorRidgelet.operatorFiniteNetwork
      (OperatorRidgelet.rankOneActivation β ψ z) ℓ v
      (fun j => OperatorRidgelet.rankOneLift ψ (a j)) fun j =>
      OperatorRidgelet.biasLift ψ (c j)) =
    OperatorRidgelet.finiteNetwork (fun t => ↑(β t)) v a c

theorem OperatorRidgelet.Paper.lem_rank_one_lift_vii.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] (β : ℝ → ℝ)
  {ψ z ℓ : H} (hψ : ψ ≠ 0)
  (hℓz : inner ℝ ℓ z = 1) {N : ℕ}
  (v : Fin N → Y) (a : Fin N → H)
  (c : Fin N → ℝ) :
  (OperatorRidgelet.operatorFiniteNetwork
      (OperatorRidgelet.rankOneActivation
        β ψ z)
      ℓ v
      (fun j =>
        OperatorRidgelet.rankOneLift ψ
          (a j))
      fun j =>
      OperatorRidgelet.biasLift ψ (c j)) =
    OperatorRidgelet.finiteNetwork
      (fun t => ↑(β t)) v a c

**Lemma [lem:rank-one-lift]** Exact rank-one lift.  Every scalar finite-width network with
activation `β` lifts exactly to the operator architecture with activation `σ_β`, parameters
`(A_{a_j}, b_{c_j})`, and readout normalized by `⟪ℓ, z⟫ = 1`.

Proof for Lemma 1.2.4

uses 0

A_a has rank at most one and A_a^*y=\|\psi\|^{-2}\langle y,\psi\rangle a, so A_a^*\psi=a; the norms are computed directly, and pushing a coefficient measure forward by J_\psi preserves its synthesis because the neuron at J_\psi(a,c) is the scalar ridge at (a,c).

Proposition1.2.5

Statement uses 4

Statement dependency previews

Preview

Definition 1.2.2

Loading preview

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

used by 0✓L∃∀N

Let \beta:\mathbb R\to\mathbb R be continuous and not a polynomial. Finite linear combinations of \beta(\langle a,x\rangle+c) are dense in C(H;\mathbb R) for uniform convergence on compact sets (i); the same holds for the rank-one operator activation \sigma_\beta with Hilbert–Schmidt parameters (ii).

Lean code for Proposition1.2.5●2 theorems

theoremdefined in OperatorRidgelet/Paper/Networks.lean

complete

theorem OperatorRidgelet.Paper.prop_scalar_universality_i.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] {β : ℝ → ℝ} (hβ : Continuous β)
  (hpoly : ¬OperatorRidgelet.IsPolynomialFun β) :
  Dense ↑(Submodule.span ℝ (OperatorRidgelet.ridgeSet β))

theorem OperatorRidgelet.Paper.prop_scalar_universality_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H] {β : ℝ → ℝ}
  (hβ : Continuous β)
  (hpoly :
    ¬OperatorRidgelet.IsPolynomialFun β) :
  Dense
    ↑(Submodule.span ℝ
        (OperatorRidgelet.ridgeSet β))

**Proposition [prop:scalar-universality]** Compact-open universality by finite-dimensional
reduction.  For continuous non-polynomial `β : ℝ → ℝ`, finite linear combinations of
`β(⟪a, x⟫ + c)` are dense in `C(H; ℝ)` for uniform convergence on compact sets.

theoremdefined in OperatorRidgelet/Paper/Networks.lean

complete

theorem OperatorRidgelet.Paper.prop_scalar_universality_ii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] {β : ℝ → ℝ} (hβ : Continuous β)
  (hpoly : ¬OperatorRidgelet.IsPolynomialFun β) {ψ z : H} (hψ : ψ ≠ 0)
  (hz : z ≠ 0) :
  Dense
    ↑(Submodule.span ℝ
        (OperatorRidgelet.operatorNeuronSet
          (OperatorRidgelet.rankOneActivation β ψ z)
          {A | OperatorRidgelet.IsHilbertSchmidt A}))

theorem OperatorRidgelet.Paper.prop_scalar_universality_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H] {β : ℝ → ℝ}
  (hβ : Continuous β)
  (hpoly :
    ¬OperatorRidgelet.IsPolynomialFun β)
  {ψ z : H} (hψ : ψ ≠ 0) (hz : z ≠ 0) :
  Dense
    ↑(Submodule.span ℝ
        (OperatorRidgelet.operatorNeuronSet
          (OperatorRidgelet.rankOneActivation
            β ψ z)
          {A |
            OperatorRidgelet.IsHilbertSchmidt
              A}))

**Proposition [prop:scalar-universality]** Compact-open universality by finite-dimensional
reduction.  For continuous non-polynomial `β : ℝ → ℝ` and nonzero `ψ, z`, finite linear
combinations of the operator neurons with the rank-one activation `σ_β` and Hilbert–Schmidt
parameters are dense in `C(H; ℝ)` for uniform convergence on compact sets.

Proof for Proposition 1.2.5

uses 0

For finite-rank projections \Pi_m\to I, f\circ\Pi_m\to f uniformly on compact sets; the finite-dimensional universal approximation theorem approximates f on \Pi_mK by scalar ridges, which compose with \Pi_m to ridges on H, and the rank-one lift gives (ii). This reduction gives no information on the parameters; the constructive statement is Theorem 5.3.1.

Lemma1.2.6

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 1✓L∃∀N

Each part carries only the hypotheses it needs. For every \psi and every finite complex Borel measure \Gamma_{\mathrm{op}} on \mathcal L_2(H)\times H, |(\pi_\psi)_\#\Gamma_{\mathrm{op}}|\le(\pi_\psi)_\#|\Gamma_{\mathrm{op}}| (ii). If moreover \beta is real and globally Lipschitz, \langle\ell,z\rangle=1, and \int(1+\|A\|_{\mathcal L_2}+\|b\|)\,\mathrm d|\Gamma_{\mathrm{op}}|<\infty, then S_{\mathrm{op}}\Gamma_{\mathrm{op}}=S_\beta[(\pi_\psi)_\#\Gamma_{\mathrm{op}}] (i) and, for compact K with r_K=\sup_K\|x\|, \|S_{\mathrm{op}}\Gamma_{\mathrm{op}}\|_{C(K)}\le\int[|\beta(0)|+\operatorname{Lip}(\beta)\|\psi\|(r_K\|A\|_{\mathcal L_2}+\|b\|)]\,\mathrm d|\Gamma_{\mathrm{op}}| (iii); \psi\ne0 is not needed for any of these. Conversely, for \psi\ne0 and \langle\ell,z\rangle=1, (\pi_\psi)_\#(J_\psi)_\#\Gamma=\Gamma (iv) and S_{\mathrm{op}}(J_\psi)_\#\Gamma=S_\beta[\Gamma] (v) for every activation \beta and every finite complex Borel measure \Gamma on H\times\mathbb R, with no Lipschitz and no moment condition.

Lean code for Lemma1.2.6●5 theorems

theoremdefined in OperatorRidgelet/Paper/Networks.lean

complete

theorem OperatorRidgelet.Paper.lem_measure_transport_i.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {β : ℝ → ℝ} {L : NNReal} (hβ : LipschitzWith L β) (ψ : H)
  (Γop :
    MeasureTheory.ComplexMeasure
      (OperatorRidgelet.OperatorRidgeParameter H))
  [MeasureTheory.IsFiniteMeasure
      (MeasureTheory.VectorMeasure.variation Γop)]
  (hHS :
    ∀ᵐ (p :
      OperatorRidgelet.OperatorRidgeParameter
        H) ∂MeasureTheory.VectorMeasure.variation Γop,
      OperatorRidgelet.IsHilbertSchmidt p.1)
  (hmom :
    MeasureTheory.Integrable
      (fun p => 1 + OperatorRidgelet.hsNorm p.1 + ‖p.2‖)
      (MeasureTheory.VectorMeasure.variation Γop))
  {ℓ z : H} (hℓz : inner ℝ ℓ z = 1) :
  OperatorRidgelet.operatorSynthesis
      (OperatorRidgelet.rankOneActivation β ψ z) ℓ Γop =
    OperatorRidgelet.integralNetwork (fun t => ↑(β t))
      (MeasureTheory.VectorMeasure.map Γop
        (OperatorRidgelet.operatorParameterMap ψ))

theorem OperatorRidgelet.Paper.lem_measure_transport_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {β : ℝ → ℝ} {L : NNReal}
  (hβ : LipschitzWith L β) (ψ : H)
  (Γop :
    MeasureTheory.ComplexMeasure
      (OperatorRidgelet.OperatorRidgeParameter
        H))
  [MeasureTheory.IsFiniteMeasure
      (MeasureTheory.VectorMeasure.variation
        Γop)]
  (hHS :
    ∀ᵐ (p :
      OperatorRidgelet.OperatorRidgeParameter
        H) ∂MeasureTheory.VectorMeasure.variation
        Γop,
      OperatorRidgelet.IsHilbertSchmidt
        p.1)
  (hmom :
    MeasureTheory.Integrable
      (fun p =>
        1 + OperatorRidgelet.hsNorm p.1 +
          ‖p.2‖)
      (MeasureTheory.VectorMeasure.variation
        Γop))
  {ℓ z : H} (hℓz : inner ℝ ℓ z = 1) :
  OperatorRidgelet.operatorSynthesis
      (OperatorRidgelet.rankOneActivation
        β ψ z)
      ℓ Γop =
    OperatorRidgelet.integralNetwork
      (fun t => ↑(β t))
      (MeasureTheory.VectorMeasure.map Γop
        (OperatorRidgelet.operatorParameterMap
          ψ))

**Lemma [lem:measure-transport]** Bounded synthesis and exact transport of measures.  For
real globally Lipschitz `β`, `ψ ≠ 0`, a finite complex Borel measure `Γ_op` on `𝓛₂(H) × H`
with `∫ (1 + ‖A‖_{𝓛₂} + ‖b‖) d|Γ_op| < ∞`, and readout normalized by `⟪ℓ, z⟫ = 1`,
`S_op Γ_op = S_β[(π_ψ)_# Γ_op]`.

theoremdefined in OperatorRidgelet/Paper/Networks.lean

complete

theorem OperatorRidgelet.Paper.lem_measure_transport_ii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [MeasurableSpace H] [BorelSpace H] (ψ : H)
  (Γop :
    MeasureTheory.ComplexMeasure
      (OperatorRidgelet.OperatorRidgeParameter H)) :
  (MeasureTheory.VectorMeasure.map Γop
        (OperatorRidgelet.operatorParameterMap ψ)).variation ≤
    MeasureTheory.Measure.map (OperatorRidgelet.operatorParameterMap ψ)
      (MeasureTheory.VectorMeasure.variation Γop)

theorem OperatorRidgelet.Paper.lem_measure_transport_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] [MeasurableSpace H]
  [BorelSpace H] (ψ : H)
  (Γop :
    MeasureTheory.ComplexMeasure
      (OperatorRidgelet.OperatorRidgeParameter
        H)) :
  (MeasureTheory.VectorMeasure.map Γop
        (OperatorRidgelet.operatorParameterMap
          ψ)).variation ≤
    MeasureTheory.Measure.map
      (OperatorRidgelet.operatorParameterMap
        ψ)
      (MeasureTheory.VectorMeasure.variation
        Γop)

**Lemma [lem:measure-transport]** Bounded synthesis and exact transport of measures.  The
variation of the pushforward is dominated by the pushforward of the variation:
`|(π_ψ)_# Γ_op| ≤ (π_ψ)_# |Γ_op|`.

theoremdefined in OperatorRidgelet/Paper/Networks.lean

complete

theorem OperatorRidgelet.Paper.lem_measure_transport_iii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {β : ℝ → ℝ} {L : NNReal} (hβ : LipschitzWith L β) (ψ : H)
  (Γop :
    MeasureTheory.ComplexMeasure
      (OperatorRidgelet.OperatorRidgeParameter H))
  [MeasureTheory.IsFiniteMeasure
      (MeasureTheory.VectorMeasure.variation Γop)]
  (hHS :
    ∀ᵐ (p :
      OperatorRidgelet.OperatorRidgeParameter
        H) ∂MeasureTheory.VectorMeasure.variation Γop,
      OperatorRidgelet.IsHilbertSchmidt p.1)
  (hmom :
    MeasureTheory.Integrable
      (fun p => 1 + OperatorRidgelet.hsNorm p.1 + ‖p.2‖)
      (MeasureTheory.VectorMeasure.variation Γop))
  {ℓ z : H} (hℓz : inner ℝ ℓ z = 1) {K : Set H} (hK : IsCompact K)
  (x : H) :
  x ∈ K →
    ‖OperatorRidgelet.operatorSynthesis
          (OperatorRidgelet.rankOneActivation β ψ z) ℓ Γop x‖ ≤
      ∫ (p : OperatorRidgelet.OperatorRidgeParameter H),
        |β 0| +
          ↑L * ‖ψ‖ *
            (sSup ((fun y => ‖y‖) '' K) * OperatorRidgelet.hsNorm p.1 +
              ‖p.2‖) ∂MeasureTheory.VectorMeasure.variation Γop

theorem OperatorRidgelet.Paper.lem_measure_transport_iii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {β : ℝ → ℝ} {L : NNReal}
  (hβ : LipschitzWith L β) (ψ : H)
  (Γop :
    MeasureTheory.ComplexMeasure
      (OperatorRidgelet.OperatorRidgeParameter
        H))
  [MeasureTheory.IsFiniteMeasure
      (MeasureTheory.VectorMeasure.variation
        Γop)]
  (hHS :
    ∀ᵐ (p :
      OperatorRidgelet.OperatorRidgeParameter
        H) ∂MeasureTheory.VectorMeasure.variation
        Γop,
      OperatorRidgelet.IsHilbertSchmidt
        p.1)
  (hmom :
    MeasureTheory.Integrable
      (fun p =>
        1 + OperatorRidgelet.hsNorm p.1 +
          ‖p.2‖)
      (MeasureTheory.VectorMeasure.variation
        Γop))
  {ℓ z : H} (hℓz : inner ℝ ℓ z = 1)
  {K : Set H} (hK : IsCompact K) (x : H) :
  x ∈ K →
    ‖OperatorRidgelet.operatorSynthesis
          (OperatorRidgelet.rankOneActivation
            β ψ z)
          ℓ Γop x‖ ≤
      ∫ (p :
        OperatorRidgelet.OperatorRidgeParameter
          H),
        |β 0| +
          ↑L * ‖ψ‖ *
            (sSup ((fun y => ‖y‖) '' K) *
                OperatorRidgelet.hsNorm
                  p.1 +
              ‖p.2‖) ∂MeasureTheory.VectorMeasure.variation
          Γop

**Lemma [lem:measure-transport]** Bounded synthesis and exact transport of measures.  For
compact `K` with `r_K = sup_K ‖x‖`,
`‖S_op Γ_op‖_{C(K)} ≤ ∫ [|β(0)| + Lip(β) ‖ψ‖ (r_K ‖A‖_{𝓛₂} + ‖b‖)] d|Γ_op|`.

theoremdefined in OperatorRidgelet/Paper/Networks.lean

complete

theorem OperatorRidgelet.Paper.lem_measure_transport_iv.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [MeasurableSpace H] [BorelSpace H] {ψ : H} (hψ : ψ ≠ 0)
  (Γ :
    MeasureTheory.ComplexMeasure
      (OperatorRidgelet.ScalarRidgeParameter H)) :
  (MeasureTheory.VectorMeasure.map Γ
          (OperatorRidgelet.operatorRidgeletSection ψ)).map
      (OperatorRidgelet.operatorParameterMap ψ) =
    Γ

theorem OperatorRidgelet.Paper.lem_measure_transport_iv.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] [MeasurableSpace H]
  [BorelSpace H] {ψ : H} (hψ : ψ ≠ 0)
  (Γ :
    MeasureTheory.ComplexMeasure
      (OperatorRidgelet.ScalarRidgeParameter
        H)) :
  (MeasureTheory.VectorMeasure.map Γ
          (OperatorRidgelet.operatorRidgeletSection
            ψ)).map
      (OperatorRidgelet.operatorParameterMap
        ψ) =
    Γ

**Lemma [lem:measure-transport]** Bounded synthesis and exact transport of measures.
Conversely, `(π_ψ)_# (J_ψ)_# Γ = Γ`.

theoremdefined in OperatorRidgelet/Paper/Networks.lean

complete

theorem OperatorRidgelet.Paper.lem_measure_transport_v.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (β : ℝ → ℝ) {ψ z ℓ : H} (hψ : ψ ≠ 0) (hℓz : inner ℝ ℓ z = 1)
  (Γ :
    MeasureTheory.ComplexMeasure
      (OperatorRidgelet.ScalarRidgeParameter H)) :
  OperatorRidgelet.operatorSynthesis
      (OperatorRidgelet.rankOneActivation β ψ z) ℓ
      (MeasureTheory.VectorMeasure.map Γ
        (OperatorRidgelet.operatorRidgeletSection ψ)) =
    OperatorRidgelet.integralNetwork (fun t => ↑(β t)) Γ

theorem OperatorRidgelet.Paper.lem_measure_transport_v.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (β : ℝ → ℝ) {ψ z ℓ : H} (hψ : ψ ≠ 0)
  (hℓz : inner ℝ ℓ z = 1)
  (Γ :
    MeasureTheory.ComplexMeasure
      (OperatorRidgelet.ScalarRidgeParameter
        H)) :
  OperatorRidgelet.operatorSynthesis
      (OperatorRidgelet.rankOneActivation
        β ψ z)
      ℓ
      (MeasureTheory.VectorMeasure.map Γ
        (OperatorRidgelet.operatorRidgeletSection
          ψ)) =
    OperatorRidgelet.integralNetwork
      (fun t => ↑(β t)) Γ

**Lemma [lem:measure-transport]** Bounded synthesis and exact transport of measures.
Conversely, `S_op (J_ψ)_# Γ = S_β Γ` with readout normalized by `⟪ℓ, z⟫ = 1`.

Proof for Lemma 1.2.6

uses 0

The variation inequality is the definition of the variation as a supremum over partitions, applied to the preimages of a partition. The atom identity is the rank-one reduction, \|A^*\psi\|\le\|A\|_{\mathcal L_2}\|\psi\| supplies the integrable envelope, and the change of variables for finite complex measures proves the synthesis identity. Finally \pi_\psi\circ J_\psi=\mathrm{id}, and J_\psi is a homeomorphism onto its closed range, so the last change of variables holds atomwise.