7.2. Gaussian-parameter networks on l2🔗

DefinitionAux.13

uses 0

Used by 3

Reverse dependency previews

Preview

Lemma 7.3

Loading preview

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

✓L∃∀N

These are the elementary ReLU identities used in Lemma 7.3 and the truncation in Example 7.9.

\operatorname{ReLU}(x)=\max(x,0) and its odd part is the identity, \operatorname{ReLU}(x)-\operatorname{ReLU}(-x)=x. For a finite spectral index set, the paired-ReLU network \sum_i\lambda_i[\operatorname{ReLU}(\langle e_i,x\rangle)-\operatorname{ReLU}(-\langle e_i,x\rangle)]e_i therefore equals the spectral truncation \sum_i\lambda_i\langle e_i,x\rangle e_i exactly.

Lean code for DefinitionAux.13●4 declarations

defdefined in LeanRidgelet/Activation/ReLU.lean

complete

def LeanRidgelet.relu (x : ℝ) : ℝ

def LeanRidgelet.relu (x : ℝ) : ℝ

The classical rectified linear unit.

theoremdefined in OperatorRidgelet/Activation.lean

complete

theorem OperatorRidgelet.relu_sub_relu_neg (x : ℝ) :
  LeanRidgelet.relu x - LeanRidgelet.relu (-x) = x

theorem OperatorRidgelet.relu_sub_relu_neg
  (x : ℝ) :
  LeanRidgelet.relu x -
      LeanRidgelet.relu (-x) =
    x

The difference of the two signed ReLU neurons is the identity.

defdefined in OperatorRidgelet/Activation.lean

complete

def OperatorRidgelet.spectralReLUNetwork.{u_1, u_2} {ι : Type u_1}
  {E : Type u_2} [DecidableEq ι] [AddCommMonoid E] [Module ℝ E]
  (s : Finset ι) (coeff coordinate : ι → ℝ) (basis : ι → E) : E

def OperatorRidgelet.spectralReLUNetwork.{u_1,
    u_2}
  {ι : Type u_1} {E : Type u_2}
  [DecidableEq ι] [AddCommMonoid E]
  [Module ℝ E] (s : Finset ι)
  (coeff coordinate : ι → ℝ)
  (basis : ι → E) : E

A finite signed-pair ReLU network with spectral coefficients.

theoremdefined in OperatorRidgelet/Activation.lean

complete

theorem OperatorRidgelet.spectralReLUNetwork_eq.{u_1, u_2} {ι : Type u_1}
  {E : Type u_2} [DecidableEq ι] [AddCommMonoid E] [Module ℝ E]
  (s : Finset ι) (coeff coordinate : ι → ℝ) (basis : ι → E) :
  OperatorRidgelet.spectralReLUNetwork s coeff coordinate basis =
    ∑ i ∈ s, (coeff i * coordinate i) • basis i

theorem OperatorRidgelet.spectralReLUNetwork_eq.{u_1,
    u_2}
  {ι : Type u_1} {E : Type u_2}
  [DecidableEq ι] [AddCommMonoid E]
  [Module ℝ E] (s : Finset ι)
  (coeff coordinate : ι → ℝ)
  (basis : ι → E) :
  OperatorRidgelet.spectralReLUNetwork s
      coeff coordinate basis =
    ∑ i ∈ s,
      (coeff i * coordinate i) • basis i

Each signed ReLU pair reduces the spectral network to its linear spectral sum.

Lemma7.3

Statement uses 2

Statement dependency previews

Preview

Definition Aux.12

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Example 7.4

Loading preview

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

✓L∃∀N

For \phi(u)=e^{-u^2/2}, the integral \int_{\mathbb R}(u-b)_+\phi''(b)\,\mathrm db converges absolutely for each u (i a) and equals \phi(u) (i b), and \int_{\mathbb R}(1+|b|^k)|\phi''(b)|\,\mathrm db<\infty for every k\ge0 (ii).

Lean code for Lemma7.3●3 theorems

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.lem_7_3_i_a (u : ℝ) :
  MeasureTheory.Integrable
    (fun b =>
      LeanRidgelet.relu (u - b) * OperatorRidgelet.gaussianActDeriv2 b)
    MeasureTheory.volume

theorem OperatorRidgelet.Paper.lem_7_3_i_a
  (u : ℝ) :
  MeasureTheory.Integrable
    (fun b =>
      LeanRidgelet.relu (u - b) *
        OperatorRidgelet.gaussianActDeriv2
          b)
    MeasureTheory.volume

**Lemma [lem:7.3]** Absolute hinge representation of the Gaussian.  For
`φ(u) = e^{-u²/2}` the integral `∫ (u-b)_+ φ''(b) db` converges absolutely for each `u`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.lem_7_3_i_b (u : ℝ) :
  ∫ (b : ℝ),
      LeanRidgelet.relu (u - b) * OperatorRidgelet.gaussianActDeriv2 b =
    OperatorRidgelet.gaussianFun u

theorem OperatorRidgelet.Paper.lem_7_3_i_b
  (u : ℝ) :
  ∫ (b : ℝ),
      LeanRidgelet.relu (u - b) *
        OperatorRidgelet.gaussianActDeriv2
          b =
    OperatorRidgelet.gaussianFun u

**Lemma [lem:7.3]** Absolute hinge representation of the Gaussian.  For
`φ(u) = e^{-u²/2}`, `φ(u) = ∫ (u-b)_+ φ''(b) db` for each `u`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.lem_7_3_ii (k : ℕ) :
  MeasureTheory.Integrable
    (fun b => (1 + |b| ^ k) * |OperatorRidgelet.gaussianActDeriv2 b|)
    MeasureTheory.volume

theorem OperatorRidgelet.Paper.lem_7_3_ii
  (k : ℕ) :
  MeasureTheory.Integrable
    (fun b =>
      (1 + |b| ^ k) *
        |OperatorRidgelet.gaussianActDeriv2
            b|)
    MeasureTheory.volume

**Lemma [lem:7.3]** Absolute hinge representation of the Gaussian.
`∫ (1 + |b|^k) |φ''(b)| db < ∞` for every `k ≥ 0`.

Proof for Lemma 7.3

uses 0

\phi''(b)=(b^2-1)e^{-b^2/2} has all polynomially weighted absolute integrals finite, and integrating by parts on (-L,u) gives \int_{-L}^u(u-b)\phi''(b)\mathrm db=\phi(u)-\phi(-L)-(u+L)\phi'(-L)\to\phi(u).

Example7.4

Statement uses 4

Statement dependency previews

Preview

Definition 2.2

Loading preview

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

used by 1✓L∃∀N

The integral networks F_Q(x)=\int_H\operatorname{ReLU}(\langle a,x\rangle)\,\mathcal N(0,Q)(\mathrm da) and \Phi_Q(x)=\int_H\Phi(\langle a,x\rangle)\,\mathcal N(0,Q)(\mathrm da), and the ReLU coefficient measure of a Gaussian-activation network with coefficient density \gamma: the pushforward of \phi''(b)\gamma(a,c)\,\lambda(\mathrm da,\mathrm dc)\,\mathrm db under (a,c,b)\mapsto(a,c-b).

F_Q(x)=\sqrt{\langle Qx,x\rangle/2\pi} (i) and \Phi_Q(x)=(1+\langle Qx,x\rangle)^{-1/2} (ii), which also equals \int_{H\times\mathbb R}\operatorname{ReLU}(\langle a,x\rangle-b)\,\phi''(b)\,\mathcal N(0,Q)(\mathrm da)\,\mathrm db (iii). Neither F_Q (iv) nor \Phi_Q (v) is cylindrical. A Gaussian-activation network with finite coefficient measure is also a ReLU network with the hinge coefficient measure (vi a), which is finite (vi b) with all parameter moments finite (vi c).

Lean code for Example7.4●11 declarations

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_4_i.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H} (e : HilbertBasis ℕ ℝ H) (q : ℕ → ℝ)
  (hq : ∀ (j : ℕ), 0 < q j) (hqs : Summable q)
  (hQe : ∀ (j : ℕ), Q (e j) = q j • e j) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (x : H) :
  OperatorRidgelet.gaussianParameterReLU μ x =
    √(inner ℝ (Q x) x / (2 * Real.pi))

theorem OperatorRidgelet.Paper.ex_7_4_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H} (e : HilbertBasis ℕ ℝ H)
  (q : ℕ → ℝ) (hq : ∀ (j : ℕ), 0 < q j)
  (hqs : Summable q)
  (hQe : ∀ (j : ℕ), Q (e j) = q j • e j)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (x : H) :
  OperatorRidgelet.gaussianParameterReLU μ
      x =
    √(inner ℝ (Q x) x / (2 * Real.pi))

**Example [ex:7.4]** ReLU and Gaussian networks with Gaussian parameters.
`F_Q(x) = ∫ ReLU(⟨a,x⟩) 𝒩(0,Q)(da) = √(⟨Qx,x⟩/2π)`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_4_ii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H} (e : HilbertBasis ℕ ℝ H) (q : ℕ → ℝ)
  (hq : ∀ (j : ℕ), 0 < q j) (hqs : Summable q)
  (hQe : ∀ (j : ℕ), Q (e j) = q j • e j) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (x : H) :
  OperatorRidgelet.gaussianParameterGauss μ x =
    (√(1 + inner ℝ (Q x) x))⁻¹

theorem OperatorRidgelet.Paper.ex_7_4_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H} (e : HilbertBasis ℕ ℝ H)
  (q : ℕ → ℝ) (hq : ∀ (j : ℕ), 0 < q j)
  (hqs : Summable q)
  (hQe : ∀ (j : ℕ), Q (e j) = q j • e j)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (x : H) :
  OperatorRidgelet.gaussianParameterGauss
      μ x =
    (√(1 + inner ℝ (Q x) x))⁻¹

**Example [ex:7.4]** ReLU and Gaussian networks with Gaussian parameters.
`Φ_Q(x) = ∫ Φ(⟨a,x⟩) 𝒩(0,Q)(da) = (1 + ⟨Qx,x⟩)^{-1/2}`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_4_iii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H} (e : HilbertBasis ℕ ℝ H) (q : ℕ → ℝ)
  (hq : ∀ (j : ℕ), 0 < q j) (hqs : Summable q)
  (hQe : ∀ (j : ℕ), Q (e j) = q j • e j) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (x : H) :
  OperatorRidgelet.gaussianParameterGauss μ x =
    ∫ (p : H × ℝ),
      LeanRidgelet.relu (inner ℝ p.1 x - p.2) *
        OperatorRidgelet.gaussianActDeriv2
          p.2 ∂μ.prod MeasureTheory.volume

theorem OperatorRidgelet.Paper.ex_7_4_iii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H} (e : HilbertBasis ℕ ℝ H)
  (q : ℕ → ℝ) (hq : ∀ (j : ℕ), 0 < q j)
  (hqs : Summable q)
  (hQe : ∀ (j : ℕ), Q (e j) = q j • e j)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (x : H) :
  OperatorRidgelet.gaussianParameterGauss
      μ x =
    ∫ (p : H × ℝ),
      LeanRidgelet.relu
          (inner ℝ p.1 x - p.2) *
        OperatorRidgelet.gaussianActDeriv2
          p.2 ∂μ.prod MeasureTheory.volume

**Example [ex:7.4]** ReLU and Gaussian networks with Gaussian parameters.
`Φ_Q(x) = ∫∫ ReLU(⟨a,x⟩ - b) φ''(b) 𝒩(0,Q)(da) db` with `φ''(b) = (b² - 1) e^{-b²/2}`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_4_iv.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H} (e : HilbertBasis ℕ ℝ H) (q : ℕ → ℝ)
  (hq : ∀ (j : ℕ), 0 < q j) (hqs : Summable q)
  (hQe : ∀ (j : ℕ), Q (e j) = q j • e j) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) :
  ¬OperatorRidgelet.IsCylindrical
      (OperatorRidgelet.gaussianParameterReLU μ)

theorem OperatorRidgelet.Paper.ex_7_4_iv.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H} (e : HilbertBasis ℕ ℝ H)
  (q : ℕ → ℝ) (hq : ∀ (j : ℕ), 0 < q j)
  (hqs : Summable q)
  (hQe : ∀ (j : ℕ), Q (e j) = q j • e j)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ) :
  ¬OperatorRidgelet.IsCylindrical
      (OperatorRidgelet.gaussianParameterReLU
        μ)

**Example [ex:7.4]** ReLU and Gaussian networks with Gaussian parameters.
`F_Q` is not cylindrical.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_4_v.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H} (e : HilbertBasis ℕ ℝ H) (q : ℕ → ℝ)
  (hq : ∀ (j : ℕ), 0 < q j) (hqs : Summable q)
  (hQe : ∀ (j : ℕ), Q (e j) = q j • e j) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) :
  ¬OperatorRidgelet.IsCylindrical
      (OperatorRidgelet.gaussianParameterGauss μ)

theorem OperatorRidgelet.Paper.ex_7_4_v.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H} (e : HilbertBasis ℕ ℝ H)
  (q : ℕ → ℝ) (hq : ∀ (j : ℕ), 0 < q j)
  (hqs : Summable q)
  (hQe : ∀ (j : ℕ), Q (e j) = q j • e j)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ) :
  ¬OperatorRidgelet.IsCylindrical
      (OperatorRidgelet.gaussianParameterGauss
        μ)

**Example [ex:7.4]** ReLU and Gaussian networks with Gaussian parameters.
`Φ_Q` is not cylindrical.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_4_vi_a.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y]
  (lam : MeasureTheory.Measure (H × ℝ)) [MeasureTheory.SigmaFinite lam]
  (γ : H × ℝ → Y) (hγ : MeasureTheory.Integrable γ lam)
  (hmom :
    ∀ (k : ℕ),
      MeasureTheory.Integrable
        (fun θ => (1 + ‖θ.1‖ + |θ.2|) ^ k * ‖γ θ‖) lam) :
  OperatorRidgelet.integralNetworkDensity
      (fun t => ↑(OperatorRidgelet.gaussianFun t)) lam γ =
    OperatorRidgelet.integralNetwork (fun t => ↑(LeanRidgelet.relu t))
      (OperatorRidgelet.hingeCoefficientMeasure lam γ)

theorem OperatorRidgelet.Paper.ex_7_4_vi_a.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (lam : MeasureTheory.Measure (H × ℝ))
  [MeasureTheory.SigmaFinite lam]
  (γ : H × ℝ → Y)
  (hγ : MeasureTheory.Integrable γ lam)
  (hmom :
    ∀ (k : ℕ),
      MeasureTheory.Integrable
        (fun θ =>
          (1 + ‖θ.1‖ + |θ.2|) ^ k * ‖γ θ‖)
        lam) :
  OperatorRidgelet.integralNetworkDensity
      (fun t =>
        ↑(OperatorRidgelet.gaussianFun t))
      lam γ =
    OperatorRidgelet.integralNetwork
      (fun t => ↑(LeanRidgelet.relu t))
      (OperatorRidgelet.hingeCoefficientMeasure
        lam γ)

**Example [ex:7.4]** ReLU and Gaussian networks with Gaussian parameters.  A
Gaussian-activation network with finite coefficient measure `γ λ` (with all parameter moments
finite) is the ReLU network with the coefficient measure `Γ' = (a,c,b) ↦ (a, c-b)`-pushforward
of `φ''(b) γ(a,c) λ(da,dc) db`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_4_vi_b.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] (lam : MeasureTheory.Measure (H × ℝ))
  [MeasureTheory.SigmaFinite lam] (γ : H × ℝ → Y)
  (hγ : MeasureTheory.Integrable γ lam)
  (hmom :
    ∀ (k : ℕ),
      MeasureTheory.Integrable
        (fun θ => (1 + ‖θ.1‖ + |θ.2|) ^ k * ‖γ θ‖) lam) :
  MeasureTheory.IsFiniteMeasure
    (OperatorRidgelet.hingeCoefficientMeasure lam γ).variation

theorem OperatorRidgelet.Paper.ex_7_4_vi_b.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (lam : MeasureTheory.Measure (H × ℝ))
  [MeasureTheory.SigmaFinite lam]
  (γ : H × ℝ → Y)
  (hγ : MeasureTheory.Integrable γ lam)
  (hmom :
    ∀ (k : ℕ),
      MeasureTheory.Integrable
        (fun θ =>
          (1 + ‖θ.1‖ + |θ.2|) ^ k * ‖γ θ‖)
        lam) :
  MeasureTheory.IsFiniteMeasure
    (OperatorRidgelet.hingeCoefficientMeasure
        lam γ).variation

**Example [ex:7.4]** ReLU and Gaussian networks with Gaussian parameters.  The
ReLU coefficient measure `Γ'` of a Gaussian-activation network with finite coefficient measure
is finite.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_4_vi_c.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] (lam : MeasureTheory.Measure (H × ℝ))
  [MeasureTheory.SigmaFinite lam] (γ : H × ℝ → Y)
  (hγ : MeasureTheory.Integrable γ lam)
  (hmom :
    ∀ (k : ℕ),
      MeasureTheory.Integrable
        (fun θ => (1 + ‖θ.1‖ + |θ.2|) ^ k * ‖γ θ‖) lam)
  (k : ℕ) :
  ∫⁻ (θ : H × ℝ),
      ENNReal.ofReal
        ((1 + ‖θ.1‖ + |θ.2|) ^
          k) ∂(OperatorRidgelet.hingeCoefficientMeasure lam
          γ).variation <
    ⊤

theorem OperatorRidgelet.Paper.ex_7_4_vi_c.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  (lam : MeasureTheory.Measure (H × ℝ))
  [MeasureTheory.SigmaFinite lam]
  (γ : H × ℝ → Y)
  (hγ : MeasureTheory.Integrable γ lam)
  (hmom :
    ∀ (k : ℕ),
      MeasureTheory.Integrable
        (fun θ =>
          (1 + ‖θ.1‖ + |θ.2|) ^ k * ‖γ θ‖)
        lam)
  (k : ℕ) :
  ∫⁻ (θ : H × ℝ),
      ENNReal.ofReal
        ((1 + ‖θ.1‖ + |θ.2|) ^
          k) ∂(OperatorRidgelet.hingeCoefficientMeasure
          lam γ).variation <
    ⊤

**Example [ex:7.4]** ReLU and Gaussian networks with Gaussian parameters.  The
ReLU coefficient measure `Γ'` of a Gaussian-activation network with finite coefficient measure
has all parameter moments finite.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.gaussianParameterReLU.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (μ : MeasureTheory.Measure H) (x : H) : ℝ

def OperatorRidgelet.gaussianParameterReLU.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  (μ : MeasureTheory.Measure H) (x : H) :
  ℝ

The ReLU network with Gaussian parameters, `F_Q(x) = ∫ ReLU(⟨a,x⟩) 𝒩(0,Q)(da)`, for the
parameter law `μ = 𝒩(0,Q)` (`eq:gaussian-parameter-networks`).

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.gaussianParameterGauss.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  (μ : MeasureTheory.Measure H) (x : H) : ℝ

def OperatorRidgelet.gaussianParameterGauss.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  (μ : MeasureTheory.Measure H) (x : H) :
  ℝ

The Gaussian-activation network with Gaussian parameters,
`Φ_Q(x) = ∫ Φ(⟨a,x⟩) 𝒩(0,Q)(da)` (`eq:gaussian-parameter-networks`).

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.hingeCoefficientMeasure.{u_1, u_2} {H : Type u_1}
  [MeasurableSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] (lam : MeasureTheory.Measure (H × ℝ))
  (γ : H × ℝ → Y) : MeasureTheory.VectorMeasure (H × ℝ) Y

def OperatorRidgelet.hingeCoefficientMeasure.{u_1,
    u_2}
  {H : Type u_1} [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y]
  (lam : MeasureTheory.Measure (H × ℝ))
  (γ : H × ℝ → Y) :
  MeasureTheory.VectorMeasure (H × ℝ) Y

The ReLU coefficient measure of a Gaussian-activation network with coefficient density `γ`
with respect to `λ`: the pushforward of `φ''(b) γ(a,c) λ(da,dc) db` under
`(a,c,b) ↦ (a, c - b)`.

Proof for Example 7.4

uses 1

For fixed x, \langle a,x\rangle is centred Gaussian with variance v=\langle Qx,x\rangle, and \mathbb EZ_+=\sqrt{v/2\pi}, \mathbb Ee^{-Z^2/2}=(1+v)^{-1/2} for Z\sim\mathcal N(0,v); the hinge representation of Lemma 7.3 with Fubini gives (iii) and (vi), and a nonzero vector in the kernel of a finite-rank map would give the same value as x=0, contradicting injectivity of Q.

Corollary7.5

Statement uses 2

Statement dependency previews

Preview

Definition Aux.11

Loading preview

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

used by 0✓L∃∀N

Let a_1,\dots,a_N be independent with law \mathcal N(0,Q) and F_{Q,N}(x)=\frac1N\sum_{j=1}^N\operatorname{ReLU}(\langle a_j,x\rangle). Then for every compact K\subset H, \mathbb E\|F_{Q,N}-F_Q\|_{C(K)}\le8R_K\sqrt{\operatorname{tr}Q}/\sqrt N.

Lean code for Corollary7.5●1 theorem

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.cor_7_5.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H} (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  (μ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (K : Set H)
  (hK : IsCompact K) (n : ℕ) (hn : 0 < n) :
  ∫ (θ : Fin n → H × ℝ),
      OperatorRidgelet.compactSupNorm K fun x =>
        OperatorRidgelet.sampledNetwork
            (fun t => ↑(LeanRidgelet.relu t)) 1 (fun x => 1) θ x -
          ↑(OperatorRidgelet.gaussianParameterReLU μ
              x) ∂OperatorRidgelet.sampleLaw n
        (MeasureTheory.Measure.map (fun a => (a, 0)) μ) ≤
    8 * OperatorRidgelet.compactRadius K *
        √(OperatorRidgelet.traceOf Q) /
      √↑n

theorem OperatorRidgelet.Paper.cor_7_5.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Q : H →L[ℝ] H}
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (K : Set H) (hK : IsCompact K) (n : ℕ)
  (hn : 0 < n) :
  ∫ (θ : Fin n → H × ℝ),
      OperatorRidgelet.compactSupNorm K
        fun x =>
        OperatorRidgelet.sampledNetwork
            (fun t =>
              ↑(LeanRidgelet.relu t))
            1 (fun x => 1) θ x -
          ↑(OperatorRidgelet.gaussianParameterReLU
              μ
              x) ∂OperatorRidgelet.sampleLaw
        n
        (MeasureTheory.Measure.map
          (fun a => (a, 0)) μ) ≤
    8 * OperatorRidgelet.compactRadius K *
        √(OperatorRidgelet.traceOf Q) /
      √↑n

**Corollary [cor:7.5]** Discretization of the Gaussian-parameter ReLU
network.  For `a_1, …, a_n` independent with law `𝒩(0,Q)` (the samples `θ_j = (a_j, 0)` of the
law `ι_# 𝒩(0,Q)`, `ι(a) = (a, 0)`) and `F_{Q,n}(x) = n⁻¹ ∑_j ReLU(⟨a_j,x⟩)` (the sampled network
`eq:polar-network` with `V = 1` and phase `1`), every compact `K ⊆ H` satisfies
`E‖F_{Q,n} - F_Q‖_{C(K)} ≤ 8 R_K √(tr Q) / √n`.

Proof for Corollary 7.5

Proof uses 2

Proof dependency previews

Preview

Theorem 6.5

Loading preview

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

Apply Theorem 6.5 with V=1, c=0, \beta(0)=0, \operatorname{Lip}(\beta)=1, and M_2^2=\mathbb E\|a\|^2=\operatorname{tr}Q.