5.4. Vector-valued sampling🔗

Corollary5.4.1

Statement uses 5

Statement dependency previews

Preview

Definition 5.1.1

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Theorem 5.3.1

Loading preview

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

✓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 Corollary5.4.1●5 theorems

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.cor_vector_rates_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_vector_rates_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:vector-rates]** 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_vector_rates_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_vector_rates_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:vector-rates]** 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_vector_rates_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_vector_rates_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:vector-rates]** 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_vector_rates_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_vector_rates_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:vector-rates]** 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_vector_rates_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_vector_rates_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:vector-rates](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 5.4.1

uses 0

Apply Lemma 5.1.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 5.1.3 in C(K;Y).