Infinite-dimensional operator ridgelet transform

5.1. Sampling bounds🔗

Let \Gamma be a finite complex measure on H\times\mathbb R with polar decomposition \Gamma=h|\Gamma|, |h|=1 |\Gamma|-almost everywhere. If \Gamma=0 take the zero network; otherwise write V=\|\Gamma\|_{\mathrm{TV}} and p=|\Gamma|/V, sample independent \theta_j=(a_j,c_j)\sim p, and form the sampled network f_N(x)=\frac VN\sum_{j=1}^Nh(\theta_j)\,\beta(\langle a_j,x\rangle+c_j), which is unbiased for f=S_\beta[\Gamma].

Definition5.1.1
Statement uses 2
Statement dependency previews
Preview
Definition 1.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 7
Reverse dependency previews
Preview
Definition 5.1.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

For a compact K\subset H, the activation-dependent Rademacher complexity is \mathfrak R_N(K;p,\beta)=\mathbb E_{\theta,\varepsilon}\sup_{x\in K}\bigl|\frac1N\sum_{j=1}^N\varepsilon_jh(\theta_j)\beta(\langle a_j,x\rangle+c_j)\bigr|, where \varepsilon_j are independent Rademacher signs; with Y-valued phases h it is \mathfrak R_N^Y(K;p,\beta). The Lean definition carries the polar data h, V, p of \Gamma, the product law p^{\otimes N} of the sample, the law of the signs, the sampled network, and the compact sup norm \|f\|_{C(K)}=\sup_{x\in K}\|f(x)\|.

Lean code for Definition5.1.1●8 definitions
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.compactSupNorm.{u_1, u_2} {X : Type u_1} {Y : Type u_2}
  [NormedAddCommGroup Y] (K : Set X) (f : X → Y) : ℝ
    def OperatorRidgelet.compactSupNorm.{u_1, u_2}
  {X : Type u_1} {Y : Type u_2}
  [NormedAddCommGroup Y] (K : Set X)
  (f : X → Y) : ℝ
    The compact sup norm `‖f‖_{C(K;Y)} = sup_{x ∈ K} ‖f(x)‖` of a function `f : X → Y` on a
set `K`, as the supremum of the image `{‖f x‖ : x ∈ K}` (`0` when `K` is empty or the norms are
unbounded on `K`).
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.polarDensity.{u_1, u_2} {Θ : Type u_1}
  [MeasurableSpace Θ] {Y : Type u_2} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y] (Γ : MeasureTheory.VectorMeasure Θ Y) : Θ → Y
    def OperatorRidgelet.polarDensity.{u_1, u_2}
  {Θ : Type u_1} [MeasurableSpace Θ]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [NormedSpace ℂ Y]
  (Γ : MeasureTheory.VectorMeasure Θ Y) :
  Θ → Y
    The phase `h` of the polar decomposition `Γ = h |Γ|` of a `Y`-valued measure of bounded
variation: a density of `Γ` with respect to its variation measure `|Γ|` with `‖h‖ = 1`
`|Γ|`-almost everywhere, chosen when one exists, and `0` otherwise.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.polarWeight.{u_1, u_2} {Θ : Type u_1}
  [MeasurableSpace Θ] {Y : Type u_2} [NormedAddCommGroup Y]
  (Γ : MeasureTheory.VectorMeasure Θ Y) : ℝ
    def OperatorRidgelet.polarWeight.{u_1, u_2}
  {Θ : Type u_1} [MeasurableSpace Θ]
  {Y : Type u_2} [NormedAddCommGroup Y]
  (Γ : MeasureTheory.VectorMeasure Θ Y) :
  ℝ
    The weight `V = ‖Γ‖_TV = |Γ|(Θ)` of the polar decomposition, as a real number
(`eq:polar-decomposition`).
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.polarLaw.{u_1, u_2} {Θ : Type u_1} [MeasurableSpace Θ]
  {Y : Type u_2} [NormedAddCommGroup Y]
  (Γ : MeasureTheory.VectorMeasure Θ Y) : MeasureTheory.Measure Θ
    def OperatorRidgelet.polarLaw.{u_1, u_2}
  {Θ : Type u_1} [MeasurableSpace Θ]
  {Y : Type u_2} [NormedAddCommGroup Y]
  (Γ : MeasureTheory.VectorMeasure Θ Y) :
  MeasureTheory.Measure Θ
    The parameter law `p = |Γ| / V` of the polar decomposition (`eq:polar-decomposition`); it
is a probability measure when `Γ ≠ 0` and the zero measure when `Γ = 0`.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.sampleLaw.{u_1} {Θ : Type u_1} [MeasurableSpace Θ]
  (N : ℕ) (p : MeasureTheory.Measure Θ) :
  MeasureTheory.Measure (Fin N → Θ)
    def OperatorRidgelet.sampleLaw.{u_1}
  {Θ : Type u_1} [MeasurableSpace Θ]
  (N : ℕ) (p : MeasureTheory.Measure Θ) :
  MeasureTheory.Measure (Fin N → Θ)
    The law `p^{⊗N}` of `N` independent parameters `θ_1, …, θ_N ∼ p`, on `Fin N → Θ`.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.rademacherMeasure (N : ℕ) :
  MeasureTheory.Measure (Fin N → ℝ)
    def OperatorRidgelet.rademacherMeasure
  (N : ℕ) :
  MeasureTheory.Measure (Fin N → ℝ)
    The law of `N` independent Rademacher signs `ε_1, …, ε_N ∈ {-1, 1}`, represented as real
numbers: the product of `N` copies of `(δ_{-1} + δ_1)/2` on `Fin N → ℝ`.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.sampledNetwork.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] {N : ℕ} (β : ℝ → ℂ) (V : ℝ)
  (h : H × ℝ → Y) (θ : Fin N → H × ℝ) : H → Y
    def OperatorRidgelet.sampledNetwork.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  {N : ℕ} (β : ℝ → ℂ) (V : ℝ)
  (h : H × ℝ → Y) (θ : Fin N → H × ℝ) :
  H → Y
    The sampled network `f_N(x) = (V/N) ∑_j β(⟪a_j, x⟫ + c_j) • h(θ_j)` (`eq:polar-network`)
of the samples `θ_j = (a_j, c_j)`, with weight `V` and phase `h`: a width-`N` network with outer
weights `(V/N) h(θ_j)`.  The scalar case is `Y = ℂ`.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.rademacherComplexity.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y] (N : ℕ)
  (K : Set H) (p : MeasureTheory.Measure (H × ℝ)) (β : ℝ → ℂ)
  (h : H × ℝ → Y) : ℝ
    def OperatorRidgelet.rademacherComplexity.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (N : ℕ) (K : Set H)
  (p : MeasureTheory.Measure (H × ℝ))
  (β : ℝ → ℂ) (h : H × ℝ → Y) : ℝ
    **Definition [def:rademacher-complexity]** The activation-dependent Rademacher complexity
`𝔑_N(K; p, β) = 𝔼_{θ,ε} sup_{x ∈ K} ‖N⁻¹ ∑_j ε_j β(⟪a_j, x⟫ + c_j) h(θ_j)‖`
(`eq:rademacher-complexity`), with `θ_j ∼ p` independent and `ε_j` independent Rademacher
signs; `h` is the phase of the polar decomposition.  The scalar case is `Y = ℂ`, and `Y`-valued
phases give `𝔑^Y_N(K; p, β)` of Corollary `cor:vector-rates`.
Definition5.1.2
Statement uses 2
Statement dependency previews
Preview
Definition 1.2.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 7
Reverse dependency previews
Preview
Theorem 5.1.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The radius R_K=\sup_{x\in K}\sqrt{\|x\|^2+1} of a compact set, the second moment M_2^2=\int_{H\times\mathbb R}(\|a\|^2+|c|^2)\,p(\mathrm da,\mathrm dc), the polar data V=\|\gamma\|_{L^1(\lambda)}, p=|\gamma|\lambda/V, h=\gamma/|\gamma| of a coefficient measure \gamma\lambda and the sampled networks of \Gamma and of \gamma\lambda, the finite atomic measure \sum_jw_j\delta_{\theta_j}, the sampled operator network f_{\mathrm{op},N}(x)=\frac VN\sum_jh_{\mathrm{op}}(A_j,b_j)\,\mathrm n_{\ell,A_j,b_j}(x) with M_{\mathrm{op}}^2=\int(\|A^*\psi\|^2+|\langle\psi,b\rangle|^2)\,\mathrm dp_{\mathrm{op}}, and finite-rank orthogonal projections.

Lean code for Definition5.1.2●11 definitions
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.compactRadius.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] (K : Set H) : ℝ
    def OperatorRidgelet.compactRadius.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  (K : Set H) : ℝ
    The radius `R_K = sup_{x ∈ K} √(‖x‖² + 1)` of a set `K` (Theorem `thm:lipschitz-barron`).
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.densityWeight.{u_1, u_2} {Θ : Type u_1}
  [MeasurableSpace Θ] {Y : Type u_2} [NormedAddCommGroup Y]
  (lam : MeasureTheory.Measure Θ) (γ : Θ → Y) : ℝ
    def OperatorRidgelet.densityWeight.{u_1, u_2}
  {Θ : Type u_1} [MeasurableSpace Θ]
  {Y : Type u_2} [NormedAddCommGroup Y]
  (lam : MeasureTheory.Measure Θ)
  (γ : Θ → Y) : ℝ
    The weight `V = ‖γ‖_{L¹(λ)} = ∫ ‖γ‖ dλ` of a coefficient measure `γ λ` with a density.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.densityLaw.{u_1, u_2} {Θ : Type u_1}
  [MeasurableSpace Θ] {Y : Type u_2} [NormedAddCommGroup Y]
  (lam : MeasureTheory.Measure Θ) (γ : Θ → Y) : MeasureTheory.Measure Θ
    def OperatorRidgelet.densityLaw.{u_1, u_2}
  {Θ : Type u_1} [MeasurableSpace Θ]
  {Y : Type u_2} [NormedAddCommGroup Y]
  (lam : MeasureTheory.Measure Θ)
  (γ : Θ → Y) : MeasureTheory.Measure Θ
    The parameter law `p = |γ| λ / V` of a coefficient measure `γ λ` with a density.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.densityPhase.{u_1, u_2} {Θ : Type u_1} {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] (γ : Θ → Y) (θ : Θ) : Y
    def OperatorRidgelet.densityPhase.{u_1, u_2}
  {Θ : Type u_1} {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (γ : Θ → Y) (θ : Θ) : Y
    The phase `h = γ / ‖γ‖` of a coefficient measure `γ λ` with a density (`0` where `γ`
vanishes).
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.polarSampledNetwork.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y] {N : ℕ}
  (β : ℝ → ℂ) (Γ : MeasureTheory.VectorMeasure (H × ℝ) Y)
  (θ : Fin N → H × ℝ) : H → Y
    def OperatorRidgelet.polarSampledNetwork.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  {N : ℕ} (β : ℝ → ℂ)
  (Γ :
    MeasureTheory.VectorMeasure (H × ℝ) Y)
  (θ : Fin N → H × ℝ) : H → Y
    The sampled network `eq:polar-network` of a measure `Γ` of bounded variation: the weight
`V = ‖Γ‖_TV` and the phase `h` of its polar decomposition, with samples `θ_j ∼ p = |Γ|/V`.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.densitySampledNetwork.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y] {N : ℕ}
  (β : ℝ → ℂ) (lam : MeasureTheory.Measure (H × ℝ)) (γ : H × ℝ → Y)
  (θ : Fin N → H × ℝ) : H → Y
    def OperatorRidgelet.densitySampledNetwork.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  {N : ℕ} (β : ℝ → ℂ)
  (lam : MeasureTheory.Measure (H × ℝ))
  (γ : H × ℝ → Y) (θ : Fin N → H × ℝ) :
  H → Y
    The sampled network `eq:polar-network` of a coefficient measure `γ λ` with a density: the
weight `V = ‖γ‖_{L¹(λ)}` and the phase `h = γ/‖γ‖`, with samples `θ_j ∼ p = |γ| λ / V`.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.secondMoment.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [MeasurableSpace H]
  (p : MeasureTheory.Measure (H × ℝ)) : ℝ
    def OperatorRidgelet.secondMoment.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [MeasurableSpace H]
  (p : MeasureTheory.Measure (H × ℝ)) : ℝ
    The second moment `M₂² = ∫ (‖a‖² + |c|²) p(da, dc)` (`eq:second-moment`) of a parameter
law `p`; `M₂` is its square root.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.atomicMeasure.{u_1, u_2} {H : Type u_1}
  [MeasurableSpace H] {Y : Type u_2} [NormedAddCommGroup Y] {n : ℕ}
  (w : Fin n → Y) (θ : Fin n → H × ℝ) :
  MeasureTheory.VectorMeasure (H × ℝ) Y
    def OperatorRidgelet.atomicMeasure.{u_1, u_2}
  {H : Type u_1} [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  {n : ℕ} (w : Fin n → Y)
  (θ : Fin n → H × ℝ) :
  MeasureTheory.VectorMeasure (H × ℝ) Y
    The finite atomic `Y`-valued measure `∑_j w_j δ_{θ_j}` on `H × ℝ`.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.sampledOperatorNetwork.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {N : ℕ} (σ : H → H)
  (ℓ : H) (V : ℝ) (h : OperatorRidgelet.OperatorRidgeParameter H → ℂ)
  (ω : Fin N → OperatorRidgelet.OperatorRidgeParameter H) : H → ℂ
    def OperatorRidgelet.sampledOperatorNetwork.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {N : ℕ}
  (σ : H → H) (ℓ : H) (V : ℝ)
  (h :
    OperatorRidgelet.OperatorRidgeParameter
        H →
      ℂ)
  (ω :
    Fin N →
      OperatorRidgelet.OperatorRidgeParameter
        H) :
  H → ℂ
    The sampled operator network `f_{op,N}(x) = (V/N) ∑_j h(A_j, b_j) n_{ℓ,A_j,b_j}(x)` of
Corollary `cor:operator-sampling`: a finite-width operator network with the samples
`(A_j, b_j)` and outer weights `(V/N) h(A_j, b_j)`.
  • defdefined in OperatorRidgelet/Sampling/Defs.lean
    complete
    def OperatorRidgelet.operatorSecondMoment.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [MeasurableSpace H] (ψ : H)
  (p :
    MeasureTheory.Measure (OperatorRidgelet.OperatorRidgeParameter H)) :
  ℝ
    def OperatorRidgelet.operatorSecondMoment.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] [MeasurableSpace H]
  (ψ : H)
  (p :
    MeasureTheory.Measure
      (OperatorRidgelet.OperatorRidgeParameter
        H)) :
  ℝ
    The operator second moment `M_op² = ∫ (‖A^*ψ‖² + |⟪ψ, b⟫|²) p_op(dA, db)` of Corollary
`cor:operator-sampling`.
  • structure(2 fields)defined in OperatorRidgelet/Sampling/Defs.lean
    complete
    structure OperatorRidgelet.IsFiniteRankProjection.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  (P : H →L[ℝ] H) : Prop
    structure OperatorRidgelet.IsFiniteRankProjection.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] (P : H →L[ℝ] H) : Prop
    `P` is a finite-rank orthogonal projection: a self-adjoint idempotent with
finite-dimensional range.

    Fields

    isStarProjection : IsStarProjection P
    `P` is an orthogonal projection: `P^* = P = P²`. 
    finiteDimensional_range : FiniteDimensional ℝ ↥(↑P).range
    The range of `P` is finite dimensional.
Lemma5.1.3
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 5.1.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Let X be a separable Banach space, p a probability measure, and \Phi\in L^1(p;X). For independent samples \theta_j\sim p and independent Rademacher signs \varepsilon_j, \mathbb E\|N^{-1}\sum_{j=1}^N\varepsilon_j\Phi(\theta_j)\|_X\to0. Moreover, for N\ge1 and m=\int\Phi\,\mathrm dp, \mathbb E\|N^{-1}\sum_{j=1}^N\Phi(\theta_j)-m\|_X\le2\mathbb E\|N^{-1}\sum_{j=1}^N\varepsilon_j\Phi(\theta_j)\|_X.

Lean code for Lemma5.1.3●2 theorems
  • theoremdefined in OperatorRidgelet/Paper/SamplingRevision.lean
    complete
    theorem OperatorRidgelet.Paper.lem_banach_rademacher_vanishing_i.{u_1, u_2}
  {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω]
  [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
  [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
  (p : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure p]
  {Φ : Ω → E} (hint : MeasureTheory.Integrable Φ p) :
  Filter.Tendsto
    (fun N =>
      ∫ (z : (Fin N → Ω) × (Fin N → ℝ)),
        ‖(↑N)⁻¹ •
            ∑ j,
              z.2 j •
                Φ
                  (z.1
                    j)‖ ∂(MeasureTheory.Measure.pi fun x => p).prod
          (OperatorRidgelet.rademacherMeasure N))
    Filter.atTop (nhds 0)
    theorem OperatorRidgelet.Paper.lem_banach_rademacher_vanishing_i.{u_1,
    u_2}
  {Ω : Type u_1} {E : Type u_2}
  [MeasurableSpace Ω]
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [CompleteSpace E] [MeasurableSpace E]
  [BorelSpace E]
  [SecondCountableTopology E]
  (p : MeasureTheory.Measure Ω)
  [MeasureTheory.IsProbabilityMeasure p]
  {Φ : Ω → E}
  (hint : MeasureTheory.Integrable Φ p) :
  Filter.Tendsto
    (fun N =>
      ∫ (z : (Fin N → Ω) × (Fin N → ℝ)),
        ‖(↑N)⁻¹ •
            ∑ j,
              z.2 j •
                Φ
                  (z.1
                    j)‖ ∂(MeasureTheory.Measure.pi
              fun x => p).prod
          (OperatorRidgelet.rademacherMeasure
            N))
    Filter.atTop (nhds 0)
    **Lemma [lem:banach-rademacher-vanishing](i).** The signed empirical mean of a
Bochner-integrable separable Banach-valued atom tends to zero in expected norm.
  • theoremdefined in OperatorRidgelet/Paper/SamplingRevision.lean
    complete
    theorem OperatorRidgelet.Paper.lem_banach_rademacher_vanishing_ii.{u_1, u_2}
  {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω]
  [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
  (p : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure p]
  {Φ : Ω → E} (hint : MeasureTheory.Integrable Φ p) (N : ℕ) :
  ((↑N)⁻¹ *
      ∫ (ω : Fin N → Ω),
        ‖∑ j, Φ (ω j) -
            ↑N •
              ∫ (x : Ω), Φ x ∂p‖ ∂MeasureTheory.Measure.pi fun x => p) ≤
    2 * (↑N)⁻¹ *
      ∑ σ,
        (2 ^ N)⁻¹ *
          ∫ (ω : Fin N → Ω),
            ‖∑ j,
                (if σ j = true then 1 else -1) •
                  Φ (ω j)‖ ∂MeasureTheory.Measure.pi fun x => p
    theorem OperatorRidgelet.Paper.lem_banach_rademacher_vanishing_ii.{u_1,
    u_2}
  {Ω : Type u_1} {E : Type u_2}
  [MeasurableSpace Ω]
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [CompleteSpace E]
  (p : MeasureTheory.Measure Ω)
  [MeasureTheory.IsProbabilityMeasure p]
  {Φ : Ω → E}
  (hint : MeasureTheory.Integrable Φ p)
  (N : ℕ) :
  ((↑N)⁻¹ *
      ∫ (ω : Fin N → Ω),
        ‖∑ j, Φ (ω j) -
            ↑N •
              ∫ (x : Ω),
                Φ
                  x ∂p‖ ∂MeasureTheory.Measure.pi
          fun x => p) ≤
    2 * (↑N)⁻¹ *
      ∑ σ,
        (2 ^ N)⁻¹ *
          ∫ (ω : Fin N → Ω),
            ‖∑ j,
                (if σ j = true then 1
                  else -1) •
                  Φ
                    (ω
                      j)‖ ∂MeasureTheory.Measure.pi
              fun x => p
    **Lemma [lem:banach-rademacher-vanishing](ii).** Symmetrization of the empirical mean.
The finite sum averages over the uniform Boolean sign vectors; the inverse width outside
the norm is the equivalent normalization of the manuscript's empirical averages.
Proof for Lemma 5.1.3
uses 0

Approximate \Phi in L^1 by a simple function \Psi=\sum_{k=1}^Jx_k\mathbf1_{E_k}. The signed-average error has expected norm at most \|\Phi-\Psi\|_{L^1}. For \Psi, the scalar second-moment identity and Cauchy–Schwarz bound the expected norm by \sum_k\|x_k\|\sqrt{p(E_k)/N}, which tends to zero. For symmetrization, introduce a ghost sample, apply Jensen, and insert independent signs using exchangeability of each pair. The triangle inequality gives the factor two. Bochner integrability justifies every expectation.

Theorem5.1.4
Statement uses 4
Statement dependency previews
Preview
Definition 1.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 5.1.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Whenever the atoms x\mapsto h(\theta)\beta(\langle a,x\rangle+c) are strongly measurable and integrable as C(K)-valued functions, the sampled network satisfies \mathbb E\|f_N-f\|_{C(K)}\le2V\,\mathfrak R_N(K;p,\beta).

Lean code for Theorem5.1.4●1 theorem
  • theoremdefined in OperatorRidgelet/Paper/Sampling.lean
    complete
    theorem OperatorRidgelet.Paper.thm_general_rademacher.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] (β : ℝ → ℂ) (Γ : MeasureTheory.ComplexMeasure (H × ℝ))
  [MeasureTheory.IsFiniteMeasure
      (MeasureTheory.VectorMeasure.variation Γ)]
  {K : Set H} (hK : IsCompact K)
  (Φ : H × ℝ → BoundedContinuousFunction ↑K ℂ)
  (hΦ :
    ∀ (θ : H × ℝ) (x : ↑K),
      (Φ θ) x =
        β (inner ℝ θ.1 ↑x + θ.2) * OperatorRidgelet.polarDensity Γ θ)
  (hint : MeasureTheory.Integrable Φ (OperatorRidgelet.polarLaw Γ))
  {N : ℕ} (hN : 0 < N) :
  ∫ (θ : Fin N → H × ℝ),
      OperatorRidgelet.compactSupNorm K fun x =>
        OperatorRidgelet.polarSampledNetwork β Γ θ x -
          OperatorRidgelet.integralNetwork β Γ
            x ∂OperatorRidgelet.sampleLaw N
        (OperatorRidgelet.polarLaw Γ) ≤
    2 * OperatorRidgelet.polarWeight Γ *
      OperatorRidgelet.rademacherComplexity N K
        (OperatorRidgelet.polarLaw Γ) β
        (OperatorRidgelet.polarDensity Γ)
    theorem OperatorRidgelet.Paper.thm_general_rademacher.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  (β : ℝ → ℂ)
  (Γ :
    MeasureTheory.ComplexMeasure (H × ℝ))
  [MeasureTheory.IsFiniteMeasure
      (MeasureTheory.VectorMeasure.variation
        Γ)]
  {K : Set H} (hK : IsCompact K)
  (Φ :
    H × ℝ →
      BoundedContinuousFunction ↑K ℂ)
  (hΦ :
    ∀ (θ : H × ℝ) (x : ↑K),
      (Φ θ) x =
        β (inner ℝ θ.1 ↑x + θ.2) *
          OperatorRidgelet.polarDensity Γ
            θ)
  (hint :
    MeasureTheory.Integrable Φ
      (OperatorRidgelet.polarLaw Γ))
  {N : ℕ} (hN : 0 < N) :
  ∫ (θ : Fin N → H × ℝ),
      OperatorRidgelet.compactSupNorm K
        fun x =>
        OperatorRidgelet.polarSampledNetwork
            β Γ θ x -
          OperatorRidgelet.integralNetwork
            β Γ
            x ∂OperatorRidgelet.sampleLaw
        N (OperatorRidgelet.polarLaw Γ) ≤
    2 * OperatorRidgelet.polarWeight Γ *
      OperatorRidgelet.rademacherComplexity
        N K (OperatorRidgelet.polarLaw Γ)
        β
        (OperatorRidgelet.polarDensity Γ)
    **Theorem [thm:general-rademacher]** General compact-open sampling bound.  Whenever the
atoms `x ↦ h(θ) β(⟪a, x⟫ + c)` are measurable and integrably bounded in `C(K)` (they are the
values of a Bochner-integrable map `Φ : Θ → C(K)`), the sampled network of the polar
decomposition of `Γ` satisfies `𝔼‖f_N − f‖_{C(K)} ≤ 2V 𝔑_N(K; p, β)`.
Proof for Theorem 5.1.4
uses 0

Apply Lemma 5.1.3 in C(K) and multiply by V. The same lemma gives convergence to zero. This step needs only Bochner integrability.

Lemma5.1.5
uses 1used by 1✓L∃∀N

Let S be a nonempty set and let \psi_i,u_i,v_i:S\to\mathbb R be bounded with |\psi_i(s)-\psi_i(t)|\le|u_i(s)-u_i(t)|+|v_i(s)-v_i(t)| for all s,t. Then \mathbb E\sup_s\sum_i\varepsilon_i\psi_i(s) \le2\mathbb E\sup_s\sum_i(\varepsilon_{i1}u_i(s)+\varepsilon_{i2}v_i(s)) for independent Rademacher signs.

Lean code for Lemma5.1.5●1 theorem
  • theoremdefined in OperatorRidgelet/Paper/SamplingRevision.lean
    complete
    theorem OperatorRidgelet.Paper.lem_two_coordinate_comparison.{u_1}
  {S : Type u_1} [Nonempty S] {N : ℕ} {ψ u v : Fin N → S → ℝ}
  (hψ : ∀ (i : Fin N), ∃ C, ∀ (s : S), |ψ i s| ≤ C)
  (hu : ∀ (i : Fin N), ∃ C, ∀ (s : S), |u i s| ≤ C)
  (hv : ∀ (i : Fin N), ∃ C, ∀ (s : S), |v i s| ≤ C)
  (hincr :
    ∀ (i : Fin N) (s t : S),
      |ψ i s - ψ i t| ≤ |u i s - u i t| + |v i s - v i t|) :
  (2 ^ N)⁻¹ * ∑ ε, ⨆ s, ∑ i, (if ε i = true then 1 else -1) * ψ i s ≤
    2 *
      ((2 ^ N)⁻¹ * (2 ^ N)⁻¹ *
        ∑ ε₁,
          ∑ ε₂,
            ⨆ s,
              ∑ i,
                ((if ε₁ i = true then 1 else -1) * u i s +
                  (if ε₂ i = true then 1 else -1) * v i s))
    theorem OperatorRidgelet.Paper.lem_two_coordinate_comparison.{u_1}
  {S : Type u_1} [Nonempty S] {N : ℕ}
  {ψ u v : Fin N → S → ℝ}
  (hψ :
    ∀ (i : Fin N),
      ∃ C, ∀ (s : S), |ψ i s| ≤ C)
  (hu :
    ∀ (i : Fin N),
      ∃ C, ∀ (s : S), |u i s| ≤ C)
  (hv :
    ∀ (i : Fin N),
      ∃ C, ∀ (s : S), |v i s| ≤ C)
  (hincr :
    ∀ (i : Fin N) (s t : S),
      |ψ i s - ψ i t| ≤
        |u i s - u i t| +
          |v i s - v i t|) :
  (2 ^ N)⁻¹ *
      ∑ ε,
        ⨆ s,
          ∑ i,
            (if ε i = true then 1
              else -1) *
              ψ i s ≤
    2 *
      ((2 ^ N)⁻¹ * (2 ^ N)⁻¹ *
        ∑ ε₁,
          ∑ ε₂,
            ⨆ s,
              ∑ i,
                ((if ε₁ i = true then 1
                    else -1) *
                    u i s +
                  (if ε₂ i = true then 1
                    else -1) *
                    v i s))
    **Lemma [lem:two-coordinate-comparison]** A two-coordinate Rademacher comparison.  For
bounded `ψ_i, u_i, v_i` on a nonempty set `S` whose increments satisfy
`|ψ_i(s) − ψ_i(t)| ≤ |u_i(s) − u_i(t)| + |v_i(s) − v_i(t)|`, the Rademacher average of
`sup_s ∑_i ε_i ψ_i(s)` is at most twice the average of
`sup_s ∑_i (ε_{i1} u_i(s) + ε_{i2} v_i(s))` over two independent sign vectors.  The averages
are the uniform averages over the Boolean sign vectors.
Proof for Lemma 5.1.5
uses 0

Fix all signs but \varepsilon_i. Choosing near-maximizers s_\pm of F\pm\psi_i and using \mathbb E|A+D|\ge\mathbb E|D| for a symmetric D, together with \mathbb E|\eta_1r+\eta_2q|=\max\{|r|,|q|\}\ge(|r|+|q|)/2, gives the one-sign comparison with an arbitrary bounded offset F. Replacing one coordinate at a time and averaging over the remaining signs proves the statement.

Theorem5.1.6
Statement uses 3
Statement dependency previews
Preview
Definition 5.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 7
Reverse dependency previews
Preview
Corollary 5.1.8
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Suppose \beta:\mathbb R\to\mathbb R is globally Lipschitz, \Gamma is a finite-variation Y-valued measure for a separable complex Hilbert space Y, and M_2^2=\int(\|a\|^2+|c|^2)\,\mathrm dp<\infty. For compact K\subset H with R_K=\sup_{x\in K}\sqrt{\|x\|^2+1}, \mathbb E\|f_N-f\|_{C(K;Y)}\le\frac{V}{\sqrt N}\bigl(4|\beta(0)| +8\operatorname{Lip}(\beta)R_KM_2\bigr) (i), at least one deterministic width-N realization satisfies the same bound (ii), and the weaker bound \frac{8V}{\sqrt N}(|\beta(0)|+\operatorname{Lip}(\beta)R_KM_2) follows (iii). The scalar case is Y=\mathbb C.

Lean code for Theorem5.1.6●3 theorems
  • theoremdefined in OperatorRidgelet/Paper/Sampling.lean
    complete
    theorem OperatorRidgelet.Paper.thm_lipschitz_barron_i.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  [SecondCountableTopology Y] [MeasurableSpace H] [BorelSpace H]
  [SecondCountableTopology H] {β : ℝ → ℝ} {L : NNReal}
  (hβ : LipschitzWith L β) (Γ : MeasureTheory.VectorMeasure (H × ℝ) Y)
  [MeasureTheory.IsFiniteMeasure Γ.variation]
  (hM :
    MeasureTheory.Integrable (fun θ => ‖θ.1‖ ^ 2 + |θ.2| ^ 2)
      (OperatorRidgelet.polarLaw Γ))
  {K : Set H} (hK : IsCompact K) {N : ℕ} (hN : 0 < N) :
  ∫ (θ : Fin N → H × ℝ),
      OperatorRidgelet.compactSupNorm K fun x =>
        OperatorRidgelet.polarSampledNetwork (fun t => ↑(β t)) Γ θ x -
          OperatorRidgelet.integralNetwork (fun t => ↑(β t)) Γ
            x ∂OperatorRidgelet.sampleLaw N
        (OperatorRidgelet.polarLaw Γ) ≤
    OperatorRidgelet.polarWeight Γ / √↑N *
      (4 * |β 0| +
        8 * ↑L * OperatorRidgelet.compactRadius K *
          √(OperatorRidgelet.secondMoment
              (OperatorRidgelet.polarLaw Γ)))
    theorem OperatorRidgelet.Paper.thm_lipschitz_barron_i.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  [MeasurableSpace H] [BorelSpace H]
  [SecondCountableTopology H] {β : ℝ → ℝ}
  {L : NNReal} (hβ : LipschitzWith L β)
  (Γ :
    MeasureTheory.VectorMeasure (H × ℝ) Y)
  [MeasureTheory.IsFiniteMeasure
      Γ.variation]
  (hM :
    MeasureTheory.Integrable
      (fun θ => ‖θ.1‖ ^ 2 + |θ.2| ^ 2)
      (OperatorRidgelet.polarLaw Γ))
  {K : Set H} (hK : IsCompact K) {N : ℕ}
  (hN : 0 < N) :
  ∫ (θ : Fin N → H × ℝ),
      OperatorRidgelet.compactSupNorm K
        fun x =>
        OperatorRidgelet.polarSampledNetwork
            (fun t => ↑(β t)) Γ θ x -
          OperatorRidgelet.integralNetwork
            (fun t => ↑(β t)) Γ
            x ∂OperatorRidgelet.sampleLaw
        N (OperatorRidgelet.polarLaw Γ) ≤
    OperatorRidgelet.polarWeight Γ / √↑N *
      (4 * |β 0| +
        8 * ↑L *
            OperatorRidgelet.compactRadius
              K *
          √(OperatorRidgelet.secondMoment
              (OperatorRidgelet.polarLaw
                Γ)))
    **Theorem [thm:lipschitz-barron]** Dimension-free uniform Hilbert-valued Barron bound.  For a
finite-variation `Y`-valued measure `Γ = h|Γ|` with `V = ‖Γ‖_TV` and `p = |Γ|/V`, a real
globally Lipschitz `β`, and `M₂² = ∫ (‖a‖² + |c|²) dp < ∞`, the sampled network
`eq:polar-network` with `Y`-valued weights satisfies
`𝔼‖f_N − f‖_{C(K;Y)} ≤ (V/√N)(4|β(0)| + 8 Lip(β) R_K M₂)`.  The manuscript's conventions
`V = 0` (the zero network) and `K = ∅` (zero error) are instances of the statement.
  • theoremdefined in OperatorRidgelet/Paper/Sampling.lean
    complete
    theorem OperatorRidgelet.Paper.thm_lipschitz_barron_ii.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  [SecondCountableTopology Y] [MeasurableSpace H] [BorelSpace H]
  [SecondCountableTopology H] {β : ℝ → ℝ} {L : NNReal}
  (hβ : LipschitzWith L β) (Γ : MeasureTheory.VectorMeasure (H × ℝ) Y)
  [MeasureTheory.IsFiniteMeasure Γ.variation]
  (hM :
    MeasureTheory.Integrable (fun θ => ‖θ.1‖ ^ 2 + |θ.2| ^ 2)
      (OperatorRidgelet.polarLaw Γ))
  {K : Set H} (hK : IsCompact K) {N : ℕ} (hN : 0 < N) :
  ∃ θ,
    (OperatorRidgelet.compactSupNorm K fun x =>
        OperatorRidgelet.polarSampledNetwork (fun t => ↑(β t)) Γ θ x -
          OperatorRidgelet.integralNetwork (fun t => ↑(β t)) Γ x) ≤
      OperatorRidgelet.polarWeight Γ / √↑N *
        (4 * |β 0| +
          8 * ↑L * OperatorRidgelet.compactRadius K *
            √(OperatorRidgelet.secondMoment
                (OperatorRidgelet.polarLaw Γ)))
    theorem OperatorRidgelet.Paper.thm_lipschitz_barron_ii.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  [MeasurableSpace H] [BorelSpace H]
  [SecondCountableTopology H] {β : ℝ → ℝ}
  {L : NNReal} (hβ : LipschitzWith L β)
  (Γ :
    MeasureTheory.VectorMeasure (H × ℝ) Y)
  [MeasureTheory.IsFiniteMeasure
      Γ.variation]
  (hM :
    MeasureTheory.Integrable
      (fun θ => ‖θ.1‖ ^ 2 + |θ.2| ^ 2)
      (OperatorRidgelet.polarLaw Γ))
  {K : Set H} (hK : IsCompact K) {N : ℕ}
  (hN : 0 < N) :
  ∃ θ,
    (OperatorRidgelet.compactSupNorm K
        fun x =>
        OperatorRidgelet.polarSampledNetwork
            (fun t => ↑(β t)) Γ θ x -
          OperatorRidgelet.integralNetwork
            (fun t => ↑(β t)) Γ x) ≤
      OperatorRidgelet.polarWeight Γ /
          √↑N *
        (4 * |β 0| +
          8 * ↑L *
              OperatorRidgelet.compactRadius
                K *
            √(OperatorRidgelet.secondMoment
                (OperatorRidgelet.polarLaw
                  Γ)))
    **Theorem [thm:lipschitz-barron]** Dimension-free uniform Hilbert-valued Barron bound.  At
least one deterministic width-`N` realization satisfies the same bound
`‖f_N − f‖_{C(K;Y)} ≤ (V/√N)(4|β(0)| + 8 Lip(β) R_K M₂)`.
  • theoremdefined in OperatorRidgelet/Paper/Sampling.lean
    complete
    theorem OperatorRidgelet.Paper.thm_lipschitz_barron_iii.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [SecondCountableTopology Y] [MeasurableSpace H]
  [BorelSpace H] [SecondCountableTopology H] {β : ℝ → ℝ} {L : NNReal}
  (hβ : LipschitzWith L β) (Γ : MeasureTheory.VectorMeasure (H × ℝ) Y)
  [MeasureTheory.IsFiniteMeasure Γ.variation]
  (hM :
    MeasureTheory.Integrable (fun θ => ‖θ.1‖ ^ 2 + |θ.2| ^ 2)
      (OperatorRidgelet.polarLaw Γ))
  {K : Set H} (hK : IsCompact K) {N : ℕ} (hN : 0 < N) :
  ∫ (θ : Fin N → H × ℝ),
      OperatorRidgelet.compactSupNorm K fun x =>
        OperatorRidgelet.polarSampledNetwork (fun t => ↑(β t)) Γ θ x -
          OperatorRidgelet.integralNetwork (fun t => ↑(β t)) Γ
            x ∂OperatorRidgelet.sampleLaw N
        (OperatorRidgelet.polarLaw Γ) ≤
    8 * OperatorRidgelet.polarWeight Γ / √↑N *
      (|β 0| +
        ↑L * OperatorRidgelet.compactRadius K *
          √(OperatorRidgelet.secondMoment
              (OperatorRidgelet.polarLaw Γ)))
    theorem OperatorRidgelet.Paper.thm_lipschitz_barron_iii.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  [MeasurableSpace H] [BorelSpace H]
  [SecondCountableTopology H] {β : ℝ → ℝ}
  {L : NNReal} (hβ : LipschitzWith L β)
  (Γ :
    MeasureTheory.VectorMeasure (H × ℝ) Y)
  [MeasureTheory.IsFiniteMeasure
      Γ.variation]
  (hM :
    MeasureTheory.Integrable
      (fun θ => ‖θ.1‖ ^ 2 + |θ.2| ^ 2)
      (OperatorRidgelet.polarLaw Γ))
  {K : Set H} (hK : IsCompact K) {N : ℕ}
  (hN : 0 < N) :
  ∫ (θ : Fin N → H × ℝ),
      OperatorRidgelet.compactSupNorm K
        fun x =>
        OperatorRidgelet.polarSampledNetwork
            (fun t => ↑(β t)) Γ θ x -
          OperatorRidgelet.integralNetwork
            (fun t => ↑(β t)) Γ
            x ∂OperatorRidgelet.sampleLaw
        N (OperatorRidgelet.polarLaw Γ) ≤
    8 * OperatorRidgelet.polarWeight Γ /
        √↑N *
      (|β 0| +
        ↑L *
            OperatorRidgelet.compactRadius
              K *
          √(OperatorRidgelet.secondMoment
              (OperatorRidgelet.polarLaw
                Γ)))
    **Theorem [thm:lipschitz-barron]** Dimension-free uniform Hilbert-valued Barron bound, in the
weaker form `𝔼‖f_N − f‖_{C(K;Y)} ≤ (8V/√N)(|β(0)| + Lip(β) R_K M₂)` of the second displayed
inequality.
Proof for Theorem 5.1.6
uses 0

Write the output norm as a supremum of real inner products over the unit ball of Y, so that the signed process is indexed by K\times B_Y. The increments of \psi_j(x,y)=\beta(\langle a_j,x\rangle+c_j)\langle y,h_j\rangle are dominated by those of \operatorname{Lip}(\beta)(\langle a_j,x\rangle+c_j) and of B_j\langle y,h_j\rangle with B_j=|\beta(0)|+\operatorname{Lip}(\beta)R_K\|(a_j,c_j)\|, so Lemma 5.1.5 applies. Hilbert duality and the Khintchine inequality bound the two resulting averages by \operatorname{Lip}(\beta)R_K(\sum_j\|(a_j,c_j)\|^2)^{1/2} and (\sum_jB_j^2)^{1/2}, and symmetrization and Jensen's inequality give (i). An integrable random variable cannot exceed its expectation almost surely, which gives (ii).

Lemma5.1.7
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

Let \beta:\mathbb R\to\mathbb C be continuous, K\subset H compact, and \int\|\beta(\langle a,\cdot\rangle+c)\|_{C(K)}\,\mathrm d|\Gamma|(a,c)<\infty. Then for every \varepsilon>0 there is a finite atomic complex measure \Gamma_\varepsilon with \|S_\beta\Gamma_\varepsilon-S_\beta\Gamma\|_{C(K)}<\varepsilon.

Lean code for Lemma5.1.7●1 theorem
  • theoremdefined in OperatorRidgelet/Paper/Sampling.lean
    complete
    theorem OperatorRidgelet.Paper.lem_qualitative_sampling.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] {β : ℝ → ℂ} (hβ : Continuous β)
  (Γ : MeasureTheory.ComplexMeasure (H × ℝ))
  [MeasureTheory.IsFiniteMeasure
      (MeasureTheory.VectorMeasure.variation Γ)]
  {K : Set H} (hK : IsCompact K)
  (hint :
    MeasureTheory.Integrable
      (fun θ =>
        OperatorRidgelet.compactSupNorm K fun x =>
          β (inner ℝ θ.1 x + θ.2))
      (MeasureTheory.VectorMeasure.variation Γ))
  {ε : ℝ} (hε : 0 < ε) :
  ∃ n w θ,
    (OperatorRidgelet.compactSupNorm K fun x =>
        OperatorRidgelet.integralNetwork β
            (OperatorRidgelet.atomicMeasure w θ) x -
          OperatorRidgelet.integralNetwork β Γ x) <
      ε
    theorem OperatorRidgelet.Paper.lem_qualitative_sampling.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {β : ℝ → ℂ} (hβ : Continuous β)
  (Γ :
    MeasureTheory.ComplexMeasure (H × ℝ))
  [MeasureTheory.IsFiniteMeasure
      (MeasureTheory.VectorMeasure.variation
        Γ)]
  {K : Set H} (hK : IsCompact K)
  (hint :
    MeasureTheory.Integrable
      (fun θ =>
        OperatorRidgelet.compactSupNorm K
          fun x =>
          β (inner ℝ θ.1 x + θ.2))
      (MeasureTheory.VectorMeasure.variation
        Γ))
  {ε : ℝ} (hε : 0 < ε) :
  ∃ n w θ,
    (OperatorRidgelet.compactSupNorm K
        fun x =>
        OperatorRidgelet.integralNetwork β
            (OperatorRidgelet.atomicMeasure
              w θ)
            x -
          OperatorRidgelet.integralNetwork
            β Γ x) <
      ε
    **Lemma [lem:qualitative-sampling]** Qualitative finite-atomic approximation.  For
continuous `β`, compact `K`, and `∫ ‖β(⟪a,·⟫ + c)‖_{C(K)} d|Γ| < ∞`, for every `ε > 0` there
is a finite atomic complex measure `Γ_ε = ∑_j w_j δ_{θ_j}` with
`‖S_β Γ_ε − S_β Γ‖_{C(K)} < ε`.
Proof for Lemma 5.1.7
uses 0

The atom map is continuous into the separable Banach space C(K), so Y(a,c)=h(a,c)\beta(\langle a,\cdot\rangle+c)|_K is Bochner integrable and its mean lies in the closed convex hull of its essential range by Hahn–Banach separation; approximate the mean by a finite convex combination of essential-range values.

Corollary5.1.8
Statement uses 2
Statement dependency previews
Preview
Definition 5.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

Under the hypotheses of Theorem 5.1.6, suppose \|a\|^2+|c|^2\le B^2 almost surely and put M_K=|\beta(0)|+\operatorname{Lip}(\beta)R_KB. With probability at least 1-\delta, \|f_N-f\|_{C(K)}\le\frac{8V}{\sqrt N}(|\beta(0)|+\operatorname{Lip}(\beta)R_KM_2)+VM_K\sqrt{2\log(1/\delta)/N}.

Lean code for Corollary5.1.8●1 theorem
  • theoremdefined in OperatorRidgelet/Paper/Sampling.lean
    complete
    theorem OperatorRidgelet.Paper.cor_sampling_concentration.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] {β : ℝ → ℝ} {L : NNReal} (hβ : LipschitzWith L β)
  (Γ : MeasureTheory.ComplexMeasure (H × ℝ))
  [MeasureTheory.IsFiniteMeasure
      (MeasureTheory.VectorMeasure.variation Γ)]
  (hM :
    MeasureTheory.Integrable (fun θ => ‖θ.1‖ ^ 2 + |θ.2| ^ 2)
      (OperatorRidgelet.polarLaw Γ))
  {B : ℝ} (hB0 : 0 ≤ B)
  (hB :
    ∀ᵐ (θ : H × ℝ) ∂OperatorRidgelet.polarLaw Γ,
      ‖θ.1‖ ^ 2 + |θ.2| ^ 2 ≤ B ^ 2)
  {K : Set H} (hK : IsCompact K) {N : ℕ} (hN : 0 < N) {δ : ℝ}
  (hδ : 0 < δ) :
  (OperatorRidgelet.sampleLaw N (OperatorRidgelet.polarLaw Γ))
      {θ |
        8 * OperatorRidgelet.polarWeight Γ / √↑N *
              (|β 0| +
                ↑L * OperatorRidgelet.compactRadius K *
                  √(OperatorRidgelet.secondMoment
                      (OperatorRidgelet.polarLaw Γ))) +
            OperatorRidgelet.polarWeight Γ *
                (|β 0| + ↑L * OperatorRidgelet.compactRadius K * B) *
              √(2 * Real.log (1 / δ) / ↑N) <
          OperatorRidgelet.compactSupNorm K fun x =>
            OperatorRidgelet.polarSampledNetwork (fun t => ↑(β t)) Γ θ
                x -
              OperatorRidgelet.integralNetwork (fun t => ↑(β t)) Γ x} ≤
    ENNReal.ofReal δ
    theorem OperatorRidgelet.Paper.cor_sampling_concentration.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {β : ℝ → ℝ} {L : NNReal}
  (hβ : LipschitzWith L β)
  (Γ :
    MeasureTheory.ComplexMeasure (H × ℝ))
  [MeasureTheory.IsFiniteMeasure
      (MeasureTheory.VectorMeasure.variation
        Γ)]
  (hM :
    MeasureTheory.Integrable
      (fun θ => ‖θ.1‖ ^ 2 + |θ.2| ^ 2)
      (OperatorRidgelet.polarLaw Γ))
  {B : ℝ} (hB0 : 0 ≤ B)
  (hB :
    ∀ᵐ (θ :
      H × ℝ) ∂OperatorRidgelet.polarLaw Γ,
      ‖θ.1‖ ^ 2 + |θ.2| ^ 2 ≤ B ^ 2)
  {K : Set H} (hK : IsCompact K) {N : ℕ}
  (hN : 0 < N) {δ : ℝ} (hδ : 0 < δ) :
  (OperatorRidgelet.sampleLaw N
        (OperatorRidgelet.polarLaw Γ))
      {θ |
        8 *
                  OperatorRidgelet.polarWeight
                    Γ /
                √↑N *
              (|β 0| +
                ↑L *
                    OperatorRidgelet.compactRadius
                      K *
                  √(OperatorRidgelet.secondMoment
                      (OperatorRidgelet.polarLaw
                        Γ))) +
            OperatorRidgelet.polarWeight
                  Γ *
                (|β 0| +
                  ↑L *
                      OperatorRidgelet.compactRadius
                        K *
                    B) *
              √(2 * Real.log (1 / δ) /
                  ↑N) <
          OperatorRidgelet.compactSupNorm
            K fun x =>
            OperatorRidgelet.polarSampledNetwork
                (fun t => ↑(β t)) Γ θ x -
              OperatorRidgelet.integralNetwork
                (fun t => ↑(β t)) Γ x} ≤
    ENNReal.ofReal δ
    **Corollary [cor:sampling-concentration]** Concentration for bounded parameters.  Under the
hypotheses of Theorem `thm:lipschitz-barron`, if `‖a‖² + |c|² ≤ B²` almost surely for some
`B ≥ 0` and `M_K = |β(0)| + Lip(β) R_K B`, then with probability at least `1 − δ`,
`‖f_N − f‖_{C(K)} ≤ (8V/√N)(|β(0)| + Lip(β) R_K M₂) + V M_K √(2 log(1/δ)/N)`.
Proof for Corollary 5.1.8
uses 0

Each atom has norm at most M_K, so replacing one sample changes \|f_N-f\|_{C(K)} by at most 2VM_K/N; the bounded-difference inequality bounds the excess over the expectation.

Lemma5.1.9
uses 1used by 1✓L∃∀N

Let X be a separable Hilbert space and Y\in L^2(p;X). For independent copies Y_j, f=V\,\mathbb EY, and f_N=VN^{-1}\sum_jY_j, \mathbb E\|f_N-f\|_X^2=\frac{V^2}N(\mathbb E\|Y\|_X^2-\|\mathbb EY\|_X^2) (i), which is at most \frac{V^2}N\mathbb E\|Y\|_X^2 (ii), and a deterministic sample satisfies the same upper bound (iii).

Lean code for Lemma5.1.9●3 theorems
  • theoremdefined in OperatorRidgelet/Paper/Sampling.lean
    complete
    theorem OperatorRidgelet.Paper.lem_hilbert_sampling_i.{u_2, u_3} {Ω : Type u_2}
  [MeasurableSpace Ω] {X : Type u_3} [NormedAddCommGroup X]
  [InnerProductSpace ℝ X] [CompleteSpace X] [SecondCountableTopology X]
  (p : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure p]
  {Y : Ω → X} (hY : MeasureTheory.MemLp Y 2 p) (V : ℝ) {N : ℕ}
  (hN : 0 < N) :
  ∫ (ω : Fin N → Ω),
      ‖(V / ↑N) • ∑ j, Y (ω j) - V • ∫ (ω' : Ω), Y ω' ∂p‖ ^
        2 ∂OperatorRidgelet.sampleLaw N p =
    V ^ 2 / ↑N * (∫ (ω' : Ω), ‖Y ω'‖ ^ 2 ∂p - ‖∫ (ω' : Ω), Y ω' ∂p‖ ^ 2)
    theorem OperatorRidgelet.Paper.lem_hilbert_sampling_i.{u_2,
    u_3}
  {Ω : Type u_2} [MeasurableSpace Ω]
  {X : Type u_3} [NormedAddCommGroup X]
  [InnerProductSpace ℝ X]
  [CompleteSpace X]
  [SecondCountableTopology X]
  (p : MeasureTheory.Measure Ω)
  [MeasureTheory.IsProbabilityMeasure p]
  {Y : Ω → X}
  (hY : MeasureTheory.MemLp Y 2 p) (V : ℝ)
  {N : ℕ} (hN : 0 < N) :
  ∫ (ω : Fin N → Ω),
      ‖(V / ↑N) • ∑ j, Y (ω j) -
            V • ∫ (ω' : Ω), Y ω' ∂p‖ ^
        2 ∂OperatorRidgelet.sampleLaw N
        p =
    V ^ 2 / ↑N *
      (∫ (ω' : Ω), ‖Y ω'‖ ^ 2 ∂p -
        ‖∫ (ω' : Ω), Y ω' ∂p‖ ^ 2)
    **Lemma [lem:hilbert-sampling]** Hilbert-valued sampling identity.  For `Y ∈ L²(p; X)` with
values in a separable Hilbert space, independent copies `Y_j`, `f = V 𝔼Y`, and
`f_N = V N⁻¹ ∑_j Y_j`: `𝔼‖f_N − f‖² = (V²/N)(𝔼‖Y‖² − ‖𝔼Y‖²)`.
  • theoremdefined in OperatorRidgelet/Paper/Sampling.lean
    complete
    theorem OperatorRidgelet.Paper.lem_hilbert_sampling_ii.{u_2, u_3} {Ω : Type u_2}
  [MeasurableSpace Ω] {X : Type u_3} [NormedAddCommGroup X]
  [InnerProductSpace ℝ X] [CompleteSpace X] [SecondCountableTopology X]
  (p : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure p]
  {Y : Ω → X} (hY : MeasureTheory.MemLp Y 2 p) (V : ℝ) {N : ℕ}
  (hN : 0 < N) :
  ∫ (ω : Fin N → Ω),
      ‖(V / ↑N) • ∑ j, Y (ω j) - V • ∫ (ω' : Ω), Y ω' ∂p‖ ^
        2 ∂OperatorRidgelet.sampleLaw N p ≤
    V ^ 2 / ↑N * ∫ (ω' : Ω), ‖Y ω'‖ ^ 2 ∂p
    theorem OperatorRidgelet.Paper.lem_hilbert_sampling_ii.{u_2,
    u_3}
  {Ω : Type u_2} [MeasurableSpace Ω]
  {X : Type u_3} [NormedAddCommGroup X]
  [InnerProductSpace ℝ X]
  [CompleteSpace X]
  [SecondCountableTopology X]
  (p : MeasureTheory.Measure Ω)
  [MeasureTheory.IsProbabilityMeasure p]
  {Y : Ω → X}
  (hY : MeasureTheory.MemLp Y 2 p) (V : ℝ)
  {N : ℕ} (hN : 0 < N) :
  ∫ (ω : Fin N → Ω),
      ‖(V / ↑N) • ∑ j, Y (ω j) -
            V • ∫ (ω' : Ω), Y ω' ∂p‖ ^
        2 ∂OperatorRidgelet.sampleLaw N
        p ≤
    V ^ 2 / ↑N * ∫ (ω' : Ω), ‖Y ω'‖ ^ 2 ∂p
    **Lemma [lem:hilbert-sampling]** Hilbert-valued sampling identity.
`𝔼‖f_N − f‖² ≤ (V²/N) 𝔼‖Y‖²`.
  • theoremdefined in OperatorRidgelet/Paper/Sampling.lean
    complete
    theorem OperatorRidgelet.Paper.lem_hilbert_sampling_iii.{u_2, u_3}
  {Ω : Type u_2} [MeasurableSpace Ω] {X : Type u_3}
  [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X]
  [SecondCountableTopology X] (p : MeasureTheory.Measure Ω)
  [MeasureTheory.IsProbabilityMeasure p] {Y : Ω → X}
  (hY : MeasureTheory.MemLp Y 2 p) (V : ℝ) {N : ℕ} (hN : 0 < N) :
  ∃ ω,
    ‖(V / ↑N) • ∑ j, Y (ω j) - V • ∫ (ω' : Ω), Y ω' ∂p‖ ^ 2 ≤
      V ^ 2 / ↑N * ∫ (ω' : Ω), ‖Y ω'‖ ^ 2 ∂p
    theorem OperatorRidgelet.Paper.lem_hilbert_sampling_iii.{u_2,
    u_3}
  {Ω : Type u_2} [MeasurableSpace Ω]
  {X : Type u_3} [NormedAddCommGroup X]
  [InnerProductSpace ℝ X]
  [CompleteSpace X]
  [SecondCountableTopology X]
  (p : MeasureTheory.Measure Ω)
  [MeasureTheory.IsProbabilityMeasure p]
  {Y : Ω → X}
  (hY : MeasureTheory.MemLp Y 2 p) (V : ℝ)
  {N : ℕ} (hN : 0 < N) :
  ∃ ω,
    ‖(V / ↑N) • ∑ j, Y (ω j) -
            V • ∫ (ω' : Ω), Y ω' ∂p‖ ^
        2 ≤
      V ^ 2 / ↑N *
        ∫ (ω' : Ω), ‖Y ω'‖ ^ 2 ∂p
    **Lemma [lem:hilbert-sampling]** Hilbert-valued sampling identity.  A deterministic sample
satisfies the same upper bound `‖f_N − f‖² ≤ (V²/N) 𝔼‖Y‖²`.
Proof for Lemma 5.1.9
uses 0

With Z_j=Y_j-\mathbb EY, independence and zero means make \mathbb E\langle Z_j,Z_k\rangle=0 for j\ne k, so the expanded squared norm leaves N\,\mathbb E\|Z_1\|^2.

Corollary5.1.10
Statement uses 3
Statement dependency previews
Preview
Lemma 1.2.6
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

Let \Gamma_{\mathrm{op}} be a finite complex measure on \mathcal L_2(H)\times H with polar decomposition h_{\mathrm{op}}|\Gamma_{\mathrm{op}}|, V_{\mathrm{op}}>0, p_{\mathrm{op}}=|\Gamma_{\mathrm{op}}|/V_{\mathrm{op}}, let \beta be real and globally Lipschitz, and assume M_{\mathrm{op}}^2<\infty. Sampling (A_j,b_j) from p_{\mathrm{op}} with the weights h_{\mathrm{op}} gives \mathbb E\|f_{\mathrm{op},N}-S_{\mathrm{op}}\Gamma_{\mathrm{op}}\|_{C(K)}\le8V_{\mathrm{op}}N^{-1/2}(|\beta(0)|+\operatorname{Lip}(\beta)R_KM_{\mathrm{op}}) (i), and M_{\mathrm{op}}^2\le\|\psi\|^2\int(\|A\|_{\mathcal L_2}^2+\|b\|^2)\,\mathrm dp_{\mathrm{op}} (ii).

Lean code for Corollary5.1.10●2 theorems
  • theoremdefined in OperatorRidgelet/Paper/Sampling.lean
    complete
    theorem OperatorRidgelet.Paper.cor_operator_sampling_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 :
    ∀ᵐ (q :
      OperatorRidgelet.OperatorRidgeParameter
        H) ∂MeasureTheory.VectorMeasure.variation Γop,
      OperatorRidgelet.IsHilbertSchmidt q.1)
  (hM :
    MeasureTheory.Integrable
      (fun q =>
        ‖(ContinuousLinearMap.adjoint q.1) ψ‖ ^ 2 + |inner ℝ ψ q.2| ^ 2)
      (OperatorRidgelet.polarLaw Γop))
  {ℓ z : H} (hℓz : inner ℝ ℓ z = 1) {K : Set H} (hK : IsCompact K)
  {N : ℕ} (hN : 0 < N) :
  ∫ (ω : Fin N → OperatorRidgelet.OperatorRidgeParameter H),
      OperatorRidgelet.compactSupNorm K fun x =>
        OperatorRidgelet.sampledOperatorNetwork
            (OperatorRidgelet.rankOneActivation β ψ z) ℓ
            (OperatorRidgelet.polarWeight Γop)
            (OperatorRidgelet.polarDensity Γop) ω x -
          OperatorRidgelet.operatorSynthesis
            (OperatorRidgelet.rankOneActivation β ψ z) ℓ Γop
            x ∂OperatorRidgelet.sampleLaw N
        (OperatorRidgelet.polarLaw Γop) ≤
    8 * OperatorRidgelet.polarWeight Γop / √↑N *
      (|β 0| +
        ↑L * OperatorRidgelet.compactRadius K *
          √(OperatorRidgelet.operatorSecondMoment ψ
              (OperatorRidgelet.polarLaw Γop)))
    theorem OperatorRidgelet.Paper.cor_operator_sampling_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 :
    ∀ᵐ (q :
      OperatorRidgelet.OperatorRidgeParameter
        H) ∂MeasureTheory.VectorMeasure.variation
        Γop,
      OperatorRidgelet.IsHilbertSchmidt
        q.1)
  (hM :
    MeasureTheory.Integrable
      (fun q =>
        ‖(ContinuousLinearMap.adjoint q.1)
                ψ‖ ^
            2 +
          |inner ℝ ψ q.2| ^ 2)
      (OperatorRidgelet.polarLaw Γop))
  {ℓ z : H} (hℓz : inner ℝ ℓ z = 1)
  {K : Set H} (hK : IsCompact K) {N : ℕ}
  (hN : 0 < N) :
  ∫ (ω :
      Fin N →
        OperatorRidgelet.OperatorRidgeParameter
          H),
      OperatorRidgelet.compactSupNorm K
        fun x =>
        OperatorRidgelet.sampledOperatorNetwork
            (OperatorRidgelet.rankOneActivation
              β ψ z)
            ℓ
            (OperatorRidgelet.polarWeight
              Γop)
            (OperatorRidgelet.polarDensity
              Γop)
            ω x -
          OperatorRidgelet.operatorSynthesis
            (OperatorRidgelet.rankOneActivation
              β ψ z)
            ℓ Γop
            x ∂OperatorRidgelet.sampleLaw
        N
        (OperatorRidgelet.polarLaw Γop) ≤
    8 * OperatorRidgelet.polarWeight Γop /
        √↑N *
      (|β 0| +
        ↑L *
            OperatorRidgelet.compactRadius
              K *
          √(OperatorRidgelet.operatorSecondMoment
              ψ
              (OperatorRidgelet.polarLaw
                Γop)))
    **Corollary [cor:operator-sampling]** Sampling in operator parameters.  For a finite
complex measure `Γ_op` on `𝓛₂(H) × H` with polar decomposition `h_op |Γ_op|`,
`V_op = ‖Γ_op‖_TV`, `p_op = |Γ_op|/V_op`, real globally Lipschitz `β`, readout normalized by
`⟪ℓ, z⟫ = 1`, and `M_op² = ∫ (‖A^*ψ‖² + |⟪ψ, b⟫|²) dp_op < ∞`, sampling `(A_j, b_j)` from
`p_op` with the weights `h_op` gives
`𝔼‖f_{op,N} − S_op Γ_op‖_{C(K)} ≤ 8 V_op N^{-1/2} (|β(0)| + Lip(β) R_K M_op)`.
  • theoremdefined in OperatorRidgelet/Paper/Sampling.lean
    complete
    theorem OperatorRidgelet.Paper.cor_operator_sampling_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.IsFiniteMeasure
      (MeasureTheory.VectorMeasure.variation Γop)]
  (hHS :
    ∀ᵐ (q :
      OperatorRidgelet.OperatorRidgeParameter
        H) ∂MeasureTheory.VectorMeasure.variation Γop,
      OperatorRidgelet.IsHilbertSchmidt q.1) :
  ∫⁻ (q : OperatorRidgelet.OperatorRidgeParameter H),
      ‖(ContinuousLinearMap.adjoint q.1) ψ‖ₑ ^ 2 +
        ‖inner ℝ ψ q.2‖ₑ ^ 2 ∂OperatorRidgelet.polarLaw Γop ≤
    ‖ψ‖ₑ ^ 2 *
      ∫⁻ (q : OperatorRidgelet.OperatorRidgeParameter H),
        OperatorRidgelet.hsNormSq q.1 +
          ‖q.2‖ₑ ^ 2 ∂OperatorRidgelet.polarLaw Γop
    theorem OperatorRidgelet.Paper.cor_operator_sampling_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.IsFiniteMeasure
      (MeasureTheory.VectorMeasure.variation
        Γop)]
  (hHS :
    ∀ᵐ (q :
      OperatorRidgelet.OperatorRidgeParameter
        H) ∂MeasureTheory.VectorMeasure.variation
        Γop,
      OperatorRidgelet.IsHilbertSchmidt
        q.1) :
  ∫⁻ (q :
      OperatorRidgelet.OperatorRidgeParameter
        H),
      ‖(ContinuousLinearMap.adjoint q.1)
              ψ‖ₑ ^
          2 +
        ‖inner ℝ ψ q.2‖ₑ ^
          2 ∂OperatorRidgelet.polarLaw
        Γop ≤
    ‖ψ‖ₑ ^ 2 *
      ∫⁻ (q :
        OperatorRidgelet.OperatorRidgeParameter
          H),
        OperatorRidgelet.hsNormSq q.1 +
          ‖q.2‖ₑ ^
            2 ∂OperatorRidgelet.polarLaw
          Γop
    **Corollary [cor:operator-sampling]** Sampling in operator parameters.
`M_op² ≤ ‖ψ‖² ∫ (‖A‖²_{𝓛₂} + ‖b‖²) dp_op`.
Proof for Corollary 5.1.10
uses 0

The atom is the scalar ridge with parameter \pi_\psi(A,b), so the proof of Theorem 5.1.6 applies on the operator probability space with M_2 replaced by M_{\mathrm{op}}; Cauchy–Schwarz and \|A\|_{\mathrm{op}}\le\|A\|_{\mathcal L_2} give the last estimate.

Corollary5.1.11
Statement uses 2
Statement dependency previews
Preview
Definition 5.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

Let \Pi_m be finite-rank orthogonal projections converging strongly to the identity. For f\in C(H) and compact K, \|f-f\circ\Pi_m\|_{C(K)}\to0 (i). If f=S_\beta\Gamma satisfies the hypotheses of Theorem 5.1.6 and the same samples are used with directions \Pi_ma_j, then \mathbb E\|f-f_{m,N}\|_{C(K)}\le\operatorname{Lip}(\beta)\bigl(\int\|a\|\,\mathrm d|\Gamma|\bigr)\sup_K\|x-\Pi_mx\|+\frac{8V}{\sqrt N}(|\beta(0)|+\operatorname{Lip}(\beta)R_KM_2) (ii).

Lean code for Corollary5.1.11●2 theorems
  • theoremdefined in OperatorRidgelet/Paper/Sampling.lean
    complete
    theorem OperatorRidgelet.Paper.cor_two_stage_error_i.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  (P : ℕ → H →L[ℝ] H)
  (hP : ∀ (m : ℕ), OperatorRidgelet.IsFiniteRankProjection (P m))
  (hlim :
    ∀ (x : H), Filter.Tendsto (fun m => (P m) x) Filter.atTop (nhds x))
  {f : H → ℂ} (hf : Continuous f) {K : Set H} (hK : IsCompact K) :
  Filter.Tendsto
    (fun m =>
      OperatorRidgelet.compactSupNorm K fun x => f x - f ((P m) x))
    Filter.atTop (nhds 0)
    theorem OperatorRidgelet.Paper.cor_two_stage_error_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] (P : ℕ → H →L[ℝ] H)
  (hP :
    ∀ (m : ℕ),
      OperatorRidgelet.IsFiniteRankProjection
        (P m))
  (hlim :
    ∀ (x : H),
      Filter.Tendsto (fun m => (P m) x)
        Filter.atTop (nhds x))
  {f : H → ℂ} (hf : Continuous f)
  {K : Set H} (hK : IsCompact K) :
  Filter.Tendsto
    (fun m =>
      OperatorRidgelet.compactSupNorm K
        fun x => f x - f ((P m) x))
    Filter.atTop (nhds 0)
    **Corollary [cor:two-stage-error]** Input truncation and sampling are separate errors.  For
finite-rank orthogonal projections `Π_m` converging strongly to the identity, `f ∈ C(H)`, and
compact `K`, `‖f − f ∘ Π_m‖_{C(K)} → 0`.
  • theoremdefined in OperatorRidgelet/Paper/Sampling.lean
    complete
    theorem OperatorRidgelet.Paper.cor_two_stage_error_ii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [MeasurableSpace H] [BorelSpace H] (P : ℕ → H →L[ℝ] H)
  (hP : ∀ (m : ℕ), OperatorRidgelet.IsFiniteRankProjection (P m))
  (hlim :
    ∀ (x : H), Filter.Tendsto (fun m => (P m) x) Filter.atTop (nhds x))
  {β : ℝ → ℝ} {L : NNReal} (hβ : LipschitzWith L β)
  (Γ : MeasureTheory.ComplexMeasure (H × ℝ))
  [MeasureTheory.IsFiniteMeasure
      (MeasureTheory.VectorMeasure.variation Γ)]
  (hM :
    MeasureTheory.Integrable (fun θ => ‖θ.1‖ ^ 2 + |θ.2| ^ 2)
      (OperatorRidgelet.polarLaw Γ))
  {K : Set H} (hK : IsCompact K) {N : ℕ} (hN : 0 < N) (m : ℕ) :
  ∫ (θ : Fin N → H × ℝ),
      OperatorRidgelet.compactSupNorm K fun x =>
        OperatorRidgelet.integralNetwork (fun t => ↑(β t)) Γ x -
          OperatorRidgelet.finiteNetwork (fun t => ↑(β t))
            (fun j =>
              ↑(OperatorRidgelet.polarWeight Γ / ↑N) •
                OperatorRidgelet.polarDensity Γ (θ j))
            (fun j => (P m) (θ j).1) (fun j => (θ j).2)
            x ∂OperatorRidgelet.sampleLaw N
        (OperatorRidgelet.polarLaw Γ) ≤
    ((↑L *
          ∫ (θ : H × ℝ),
            ‖θ.1‖ ∂MeasureTheory.VectorMeasure.variation Γ) *
        OperatorRidgelet.compactSupNorm K fun x => x - (P m) x) +
      8 * OperatorRidgelet.polarWeight Γ / √↑N *
        (|β 0| +
          ↑L * OperatorRidgelet.compactRadius K *
            √(OperatorRidgelet.secondMoment
                (OperatorRidgelet.polarLaw Γ)))
    theorem OperatorRidgelet.Paper.cor_two_stage_error_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H] [MeasurableSpace H]
  [BorelSpace H] (P : ℕ → H →L[ℝ] H)
  (hP :
    ∀ (m : ℕ),
      OperatorRidgelet.IsFiniteRankProjection
        (P m))
  (hlim :
    ∀ (x : H),
      Filter.Tendsto (fun m => (P m) x)
        Filter.atTop (nhds x))
  {β : ℝ → ℝ} {L : NNReal}
  (hβ : LipschitzWith L β)
  (Γ :
    MeasureTheory.ComplexMeasure (H × ℝ))
  [MeasureTheory.IsFiniteMeasure
      (MeasureTheory.VectorMeasure.variation
        Γ)]
  (hM :
    MeasureTheory.Integrable
      (fun θ => ‖θ.1‖ ^ 2 + |θ.2| ^ 2)
      (OperatorRidgelet.polarLaw Γ))
  {K : Set H} (hK : IsCompact K) {N : ℕ}
  (hN : 0 < N) (m : ℕ) :
  ∫ (θ : Fin N → H × ℝ),
      OperatorRidgelet.compactSupNorm K
        fun x =>
        OperatorRidgelet.integralNetwork
            (fun t => ↑(β t)) Γ x -
          OperatorRidgelet.finiteNetwork
            (fun t => ↑(β t))
            (fun j =>
              ↑(OperatorRidgelet.polarWeight
                      Γ /
                    ↑N) •
                OperatorRidgelet.polarDensity
                  Γ (θ j))
            (fun j => (P m) (θ j).1)
            (fun j => (θ j).2)
            x ∂OperatorRidgelet.sampleLaw
        N (OperatorRidgelet.polarLaw Γ) ≤
    ((↑L *
          ∫ (θ : H × ℝ),
            ‖θ.1‖ ∂MeasureTheory.VectorMeasure.variation
              Γ) *
        OperatorRidgelet.compactSupNorm K
          fun x => x - (P m) x) +
      8 * OperatorRidgelet.polarWeight Γ /
          √↑N *
        (|β 0| +
          ↑L *
              OperatorRidgelet.compactRadius
                K *
            √(OperatorRidgelet.secondMoment
                (OperatorRidgelet.polarLaw
                  Γ)))
    **Corollary [cor:two-stage-error]** Input truncation and sampling are separate errors.  If
`f = S_β Γ` satisfies the hypotheses of Theorem `thm:lipschitz-barron` and the same samples and
weights `(V/N) h(θ_j)` are used with the truncated directions `Π_m a_j` inside the activation,
`f_{m,N}(x) = (V/N) ∑_j h(θ_j) β(⟪Π_m a_j, x⟫ + c_j)`, then
`𝔼‖f − f_{m,N}‖_{C(K)} ≤ Lip(β) (∫ ‖a‖ d|Γ|) sup_K ‖x − Π_m x‖ +
(8V/√N)(|β(0)| + Lip(β) R_K M₂)`.
Proof for Corollary 5.1.11
uses 0

A finite-net argument gives \sup_K\|x-\Pi_mx\|\to0, and uniform convergence of f\circ\Pi_m on K follows by compactness and continuity of f; the triangle inequality separates truncation from sampling, and projecting directions does not increase their second moment.