Input truncation and finite-width approximation🔗

CorollaryC.2

Statement uses 2

Statement dependency previews

Preview

Definition Aux.9

Loading preview

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

used by 0✓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 6.5 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 CorollaryC.2●2 theorems

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.cor_C_2_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_C_2_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:C.2]** Input truncation and finite-width approximation 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_C_2_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_C_2_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:C.2]** Input truncation and finite-width approximation errors.  If
`f = S_β Γ` satisfies the hypotheses of Theorem `thm:6.5` 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 C.2

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.