Concentration for bounded parameters🔗

CorollaryC.1

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

Under the hypotheses of Theorem 6.5, 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 CorollaryC.1●1 theorem

theoremdefined in OperatorRidgelet/Paper/Sampling.lean

complete

theorem OperatorRidgelet.Paper.cor_C_1.{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_C_1.{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:C.1]** Concentration for bounded parameters.  Under the
hypotheses of Theorem `thm:6.5`, 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 C.1

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.