6.2. Explicit Lipschitz approximation rate🔗

Lemma6.4

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 Lemma6.4●1 theorem

theoremdefined in OperatorRidgelet/Paper/SamplingRevision.lean

complete

theorem OperatorRidgelet.Paper.lem_6_4.{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_6_4.{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:6.4]** 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 6.4

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.

Theorem6.5

uses 1

Used by 6

Reverse dependency previews

Preview

Theorem 6.6

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 Theorem6.5●3 theorems

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.thm_6_5_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_6_5_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:6.5]** 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_6_5_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_6_5_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:6.5]** 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_6_5_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_6_5_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:6.5]** 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 6.5

Proof uses 2

Proof dependency previews

Preview

Theorem 6.3

Loading preview

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

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