6.5. Vector-valued approximation🔗

Lemma6.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 Lemma6.9●3 theorems

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.lem_6_9_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_6_9_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:6.9]** Mean-square error identity for Hilbert-valued averages.
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_6_9_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_6_9_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:6.9]** Mean-square error identity for Hilbert-valued averages.
`𝔼‖f_N − f‖² ≤ (V²/N) 𝔼‖Y‖²`.

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.lem_6_9_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_6_9_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:6.9]** Mean-square error identity for Hilbert-valued averages.
A deterministic sample satisfies the same upper bound `‖f_N − f‖² ≤ (V²/N) 𝔼‖Y‖²`.

Proof for Lemma 6.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.

Corollary6.10

Statement uses 2

Statement dependency previews

Preview

Definition 6.1

Loading preview

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

used by 1✓L∃∀N

Let \Gamma be a Y-valued measure of bounded variation with polar decomposition \Gamma=h|\Gamma|, let \beta be real and globally Lipschitz, and let N\ge1. If V=0, use the zero network; otherwise let p=|\Gamma|/V. (i) Assume the parameter second moment is finite. For every Borel probability measure \zeta with \int\|x\|^2\,\mathrm d\zeta<\infty, \mathbb E\|f_N-f\|_{L^2(\zeta;Y)}^2=\frac1N\left(V^2\int\|\beta(\langle a,\cdot\rangle+c)\|_{L^2(\zeta)}^2\,\mathrm dp-\|f\|_{L^2(\zeta;Y)}^2\right). Consequently this is at most \frac{V^2}N\int\|\beta(\langle a,\cdot\rangle+c)\|_{L^2(\zeta)}^2\,\mathrm dp\le\frac{2V^2}N\left(|\beta(0)|^2+\operatorname{Lip}(\beta)^2(1+\int\|x\|^2\,\mathrm d\zeta)M_2^2\right). (ii) Only the first moment \int(\|a\|+|c|)\,\mathrm dp<\infty is needed for \mathbb E\|f_N-f\|_{C(K;Y)}\le2V\,\mathfrak R_N^Y(K;p,\beta) on compact K, and for \mathfrak R_N^Y(K;p,\beta)\to0.

Lean code for Corollary6.10●5 theorems

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.cor_6_10_i_a.{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 Γ))
  (ζ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure ζ]
  (hζ : MeasureTheory.Integrable (fun x => ‖x‖ ^ 2) ζ) {N : ℕ}
  (hN : 0 < N) :
  ∫ (θ : Fin N → H × ℝ),
      ∫ (x : H),
        ‖OperatorRidgelet.polarSampledNetwork β Γ θ x -
              OperatorRidgelet.integralNetwork β Γ x‖ ^
          2 ∂ζ ∂OperatorRidgelet.sampleLaw N
        (OperatorRidgelet.polarLaw Γ) ≤
    OperatorRidgelet.polarWeight Γ ^ 2 / ↑N *
      ∫ (θ : H × ℝ),
        ∫ (x : H),
          ‖β (inner ℝ θ.1 x + θ.2)‖ ^ 2 ∂ζ ∂OperatorRidgelet.polarLaw Γ

theorem OperatorRidgelet.Paper.cor_6_10_i_a.{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 Γ))
  (ζ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure ζ]
  (hζ :
    MeasureTheory.Integrable
      (fun x => ‖x‖ ^ 2) ζ)
  {N : ℕ} (hN : 0 < N) :
  ∫ (θ : Fin N → H × ℝ),
      ∫ (x : H),
        ‖OperatorRidgelet.polarSampledNetwork
                β Γ θ x -
              OperatorRidgelet.integralNetwork
                β Γ x‖ ^
          2 ∂ζ ∂OperatorRidgelet.sampleLaw
        N (OperatorRidgelet.polarLaw Γ) ≤
    OperatorRidgelet.polarWeight Γ ^ 2 /
        ↑N *
      ∫ (θ : H × ℝ),
        ∫ (x : H),
          ‖β (inner ℝ θ.1 x + θ.2)‖ ^
            2 ∂ζ ∂OperatorRidgelet.polarLaw
          Γ

**Corollary [cor:6.10]** Vector-valued rates.  For globally Lipschitz `β`, a
`Y`-valued `Γ` whose law `p = |Γ|/V` has finite second moment, and every Borel probability
measure `ζ` on `H` with `∫ ‖x‖² dζ < ∞`,
`𝔼‖f_N − f‖²_{L²(ζ;Y)} ≤ (V²/N) ∫ ‖β(⟪a,·⟫ + c)‖²_{L²(ζ)} dp`.

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.cor_6_10_i_b.{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]
  {β : ℝ → ℂ} {L : NNReal} (hβ : LipschitzWith L β)
  (Γ : MeasureTheory.VectorMeasure (H × ℝ) Y)
  [MeasureTheory.IsFiniteMeasure Γ.variation]
  (hM :
    MeasureTheory.Integrable (fun θ => ‖θ.1‖ ^ 2 + |θ.2| ^ 2)
      (OperatorRidgelet.polarLaw Γ))
  (ζ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure ζ]
  (hζ : MeasureTheory.Integrable (fun x => ‖x‖ ^ 2) ζ) {N : ℕ}
  (hN : 0 < N) :
  OperatorRidgelet.polarWeight Γ ^ 2 / ↑N *
      ∫ (θ : H × ℝ),
        ∫ (x : H),
          ‖β (inner ℝ θ.1 x + θ.2)‖ ^
            2 ∂ζ ∂OperatorRidgelet.polarLaw Γ ≤
    2 * OperatorRidgelet.polarWeight Γ ^ 2 / ↑N *
      (‖β 0‖ ^ 2 +
        ↑L ^ 2 * (1 + ∫ (x : H), ‖x‖ ^ 2 ∂ζ) *
          OperatorRidgelet.secondMoment (OperatorRidgelet.polarLaw Γ))

theorem OperatorRidgelet.Paper.cor_6_10_i_b.{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]
  {β : ℝ → ℂ} {L : NNReal}
  (hβ : LipschitzWith L β)
  (Γ :
    MeasureTheory.VectorMeasure (H × ℝ) Y)
  [MeasureTheory.IsFiniteMeasure
      Γ.variation]
  (hM :
    MeasureTheory.Integrable
      (fun θ => ‖θ.1‖ ^ 2 + |θ.2| ^ 2)
      (OperatorRidgelet.polarLaw Γ))
  (ζ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure ζ]
  (hζ :
    MeasureTheory.Integrable
      (fun x => ‖x‖ ^ 2) ζ)
  {N : ℕ} (hN : 0 < N) :
  OperatorRidgelet.polarWeight Γ ^ 2 /
        ↑N *
      ∫ (θ : H × ℝ),
        ∫ (x : H),
          ‖β (inner ℝ θ.1 x + θ.2)‖ ^
            2 ∂ζ ∂OperatorRidgelet.polarLaw
          Γ ≤
    2 *
          OperatorRidgelet.polarWeight Γ ^
            2 /
        ↑N *
      (‖β 0‖ ^ 2 +
        ↑L ^ 2 *
            (1 + ∫ (x : H), ‖x‖ ^ 2 ∂ζ) *
          OperatorRidgelet.secondMoment
            (OperatorRidgelet.polarLaw Γ))

**Corollary [cor:6.10]** Vector-valued rates.  The `L²(ζ;Y)` rate is explicit:
`(V²/N) ∫ ‖β(⟪a,·⟫ + c)‖²_{L²(ζ)} dp ≤ (2V²/N)(|β(0)|² + Lip(β)² (1 + ∫ ‖x‖² dζ) M₂²)`.

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.cor_6_10_ii_a.{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|)
      (OperatorRidgelet.polarLaw Γ))
  {K : Set H} (hK : IsCompact K) {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.cor_6_10_ii_a.{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|)
      (OperatorRidgelet.polarLaw Γ))
  {K : Set H} (hK : IsCompact K) {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 Γ)

**Corollary [cor:6.10]** Vector-valued rates.  For every compact `K`,
`𝔼‖f_N − f‖_{C(K;Y)} ≤ 2V 𝔑^Y_N(K; p, β)`, where `𝔑^Y_N` is the Rademacher complexity with the
absolute value replaced by the norm of `Y`.

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.cor_6_10_ii_b.{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|)
      (OperatorRidgelet.polarLaw Γ))
  {K : Set H} (hK : IsCompact K) :
  Filter.Tendsto
    (fun N =>
      OperatorRidgelet.rademacherComplexity N K
        (OperatorRidgelet.polarLaw Γ) β
        (OperatorRidgelet.polarDensity Γ))
    Filter.atTop (nhds 0)

theorem OperatorRidgelet.Paper.cor_6_10_ii_b.{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|)
      (OperatorRidgelet.polarLaw Γ))
  {K : Set H} (hK : IsCompact K) :
  Filter.Tendsto
    (fun N =>
      OperatorRidgelet.rademacherComplexity
        N K (OperatorRidgelet.polarLaw Γ)
        β
        (OperatorRidgelet.polarDensity Γ))
    Filter.atTop (nhds 0)

**Corollary [cor:6.10]** Vector-valued rates.  For every compact `K`,
`𝔑^Y_N(K; p, β) → 0` as `N → ∞`.

theoremdefined in OperatorRidgelet/Paper/SamplingRevision.lean

complete

theorem OperatorRidgelet.Paper.cor_6_10_i_exact.{u_1, u_2} {H : Type u_1}
  {Y : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H] [SecondCountableTopology H]
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
  {β : ℝ → ℂ} {L : NNReal} (hβ : LipschitzWith L β)
  (Γ : MeasureTheory.VectorMeasure (H × ℝ) Y)
  [MeasureTheory.IsFiniteMeasure Γ.variation]
  (hM :
    MeasureTheory.Integrable (fun θ => ‖θ.1‖ ^ 2 + |θ.2| ^ 2)
      (OperatorRidgelet.polarLaw Γ))
  (ζ : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure ζ]
  (hζ : MeasureTheory.Integrable (fun x => ‖x‖ ^ 2) ζ) {N : ℕ}
  (hN : 0 < N) :
  ∫ (θ : Fin N → H × ℝ),
      ∫ (x : H),
        ‖OperatorRidgelet.polarSampledNetwork β Γ θ x -
              OperatorRidgelet.integralNetwork β Γ x‖ ^
          2 ∂ζ ∂OperatorRidgelet.sampleLaw N
        (OperatorRidgelet.polarLaw Γ) =
    (↑N)⁻¹ *
      (OperatorRidgelet.polarWeight Γ ^ 2 *
          ∫ (θ : H × ℝ),
            ∫ (x : H),
              ‖β (inner ℝ θ.1 x + θ.2)‖ ^
                2 ∂ζ ∂OperatorRidgelet.polarLaw Γ -
        ∫ (x : H), ‖OperatorRidgelet.integralNetwork β Γ x‖ ^ 2 ∂ζ)

theorem OperatorRidgelet.Paper.cor_6_10_i_exact.{u_1,
    u_2}
  {H : Type u_1} {Y : Type u_2}
  [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  [SecondCountableTopology H]
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y] {β : ℝ → ℂ}
  {L : NNReal} (hβ : LipschitzWith L β)
  (Γ :
    MeasureTheory.VectorMeasure (H × ℝ) Y)
  [MeasureTheory.IsFiniteMeasure
      Γ.variation]
  (hM :
    MeasureTheory.Integrable
      (fun θ => ‖θ.1‖ ^ 2 + |θ.2| ^ 2)
      (OperatorRidgelet.polarLaw Γ))
  (ζ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure ζ]
  (hζ :
    MeasureTheory.Integrable
      (fun x => ‖x‖ ^ 2) ζ)
  {N : ℕ} (hN : 0 < N) :
  ∫ (θ : Fin N → H × ℝ),
      ∫ (x : H),
        ‖OperatorRidgelet.polarSampledNetwork
                β Γ θ x -
              OperatorRidgelet.integralNetwork
                β Γ x‖ ^
          2 ∂ζ ∂OperatorRidgelet.sampleLaw
        N (OperatorRidgelet.polarLaw Γ) =
    (↑N)⁻¹ *
      (OperatorRidgelet.polarWeight Γ ^
            2 *
          ∫ (θ : H × ℝ),
            ∫ (x : H),
              ‖β (inner ℝ θ.1 x + θ.2)‖ ^
                2 ∂ζ ∂OperatorRidgelet.polarLaw
              Γ -
        ∫ (x : H),
          ‖OperatorRidgelet.integralNetwork
                β Γ x‖ ^
            2 ∂ζ)

**Corollary [cor:6.10](i).** The exact integrated variance of the sampled network,
including the subtracted squared norm of its target and the zero-variation case.

Proof for Corollary 6.10

Proof uses 3

Proof dependency previews

Preview

Lemma 6.2

Loading preview

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

Apply Lemma 6.9 in L^2(\zeta;Y) to obtain the exact variance. The polar phase has norm one almost everywhere. The elementary bounds |\beta(u)|^2\le2|\beta(0)|^2+2\operatorname{Lip}(\beta)^2u^2 and u^2\le(\|a\|^2+c^2)(\|x\|^2+1) give the second-moment estimate. For (ii), the compact atom map is continuous before composition with the measurable polar phase, hence strongly measurable. Its norm is bounded by |\beta(0)|+\operatorname{Lip}(\beta)R_K\sqrt{\|a\|^2+c^2}, which is integrable under the first-moment hypothesis. Apply Lemma 6.2 in C(K;Y).