6.3. Gaussian-parameter networks on the sequence space🔗

Let H=\ell^2(\mathbb N) with standard basis (e_j) and Qe_j=q_je_j, q_j>0, \sum_jq_j<\infty; in Lean, H is abstract with a Hilbert basis on which Q is diagonal.

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

Lean code for Definition6.3.1●3 definitions

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

Proposition6.3.2

Statement uses 4

Statement dependency previews

Preview

Definition 2.1.1

Loading preview

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

used by 1✓L∃∀N

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 Proposition6.3.2●8 theorems

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_gaussian_parameter_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_gaussian_parameter_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:gaussian-parameter]** 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_gaussian_parameter_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_gaussian_parameter_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:gaussian-parameter]** 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_gaussian_parameter_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_gaussian_parameter_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:gaussian-parameter]** 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_gaussian_parameter_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_gaussian_parameter_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:gaussian-parameter]** ReLU and Gaussian networks with Gaussian parameters.
`F_Q` is not cylindrical.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_gaussian_parameter_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_gaussian_parameter_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:gaussian-parameter]** ReLU and Gaussian networks with Gaussian parameters.
`Φ_Q` is not cylindrical.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_gaussian_parameter_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_gaussian_parameter_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:gaussian-parameter]** 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_gaussian_parameter_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_gaussian_parameter_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:gaussian-parameter]** 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_gaussian_parameter_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_gaussian_parameter_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:gaussian-parameter]** 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.

Proof for Proposition 6.3.2

uses 0

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

Corollary6.3.3

Statement uses 4

Statement dependency previews

Preview

Theorem 5.1.6

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 Corollary6.3.3●1 theorem

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.cor_relu_discretization.{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_relu_discretization.{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:relu-discretization]** 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 6.3.3

uses 0

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