Hoeffding Empirical-Mean Bound for the Bounded View-Loss

Formal statements

Auto-generated from the Lean extractor — edit the page’s notation: frontmatter and regenerate; do not edit this block.

bounded_view_loss_empirical_mean_upper_tail

Context: Ω : Type u_1 _ : MeasurableSpace Ω μ : MeasureTheory.Measure Ω loss : ℕ → Ω → ℝ a : ℝ b : ℝ ε : ℝ n : ℕ _ : MeasureTheory.IsProbabilityMeasure μ

Given

• \mathtt{h\_indep} : \mathtt{ProbabilityTheory.iIndepFun}\,\lambda i : \mathtt{Nat},\ \lambda ω : Ω,\ \mathtt{loss}\,i\,ω - \mathtt{MeasureTheory.integral}\,μ\,\lambda : Ω,\ \mathtt{loss}\,i\,_\,μ
• $h\_meas:\forall i:\mathtt{Nat},\mathtt{AEMeasurable}\mathtt{loss}i\mu$
• $h\_bounded:\forall i:\mathtt{Nat},Filter.Eventually\lambda \omega :\Omega ,\mathtt{loss}i\omega \in Set.IccabMeasureTheory.ae\mu$
• $\mathtt{hn}:0<n$
• $\mathtt{h}\epsilon :0\le \epsilon$

then

\mathtt{MeasureTheory.Measure.real}\,μ\,\mathtt{setOf}\,\lambda ω : Ω,\ ε \le \mathtt{HDiv.hDiv}\,\mathtt{Finset.sum}\,\mathtt{Finset.range}\,n\,\lambda i : \mathtt{Nat},\ \mathtt{loss}\,i\,ω - \mathtt{MeasureTheory.integral}\,μ\,\lambda : Ω,\ \mathtt{loss}\,i\,_\,\mathtt{Nat.cast}\,n \le \mathtt{Real.exp}\,\mathtt{HDiv.hDiv}\,\mathtt{Neg.neg}\,\mathtt{HPow.hPow}\,\mathtt{Nat.cast}\,n \cdot ε\,2\,2 \cdot \mathtt{Nat.cast}\,n \cdot \mathtt{HPow.hPow}\,\mathtt{HDiv.hDiv}\,\mathtt{NNReal.toReal}\,\mathtt{NNNorm.nnnorm}\,b - a\,2\,2

centered_view_loss_hasSubgaussianMGF_of_mem_Icc

Context: Ω : Type u_1 _ : MeasurableSpace Ω μ : MeasureTheory.Measure Ω loss : Ω → ℝ a : ℝ b : ℝ _ : MeasureTheory.IsProbabilityMeasure μ

Given

• $h\_meas:\mathtt{AEMeasurable}\mathtt{loss}\mu$
• $h\_bounded:Filter.Eventually\lambda \omega :\Omega ,\mathtt{loss}\omega \in Set.IccabMeasureTheory.ae\mu$

then

\mathtt{ProbabilityTheory.HasSubgaussianMGF}\,\lambda ω : Ω,\ \mathtt{loss}\,ω - \mathtt{MeasureTheory.integral}\,μ\,\lambda : Ω,\ \mathtt{loss}\,_\,\mathtt{HPow.hPow}\,\mathtt{HDiv.hDiv}\,\mathtt{NNNorm.nnnorm}\,b - a\,2\,2\,μ

Status: STUB — statements type-check, bodies are sorry. This module is the growth-loop deliverable for the reachable half of risk obligation A6 (board card, note tasks/streams/ctrllib/risk_a6_hoeffding.md): a concentration bound on the empirical mean of a bounded view-loss. The quantile/DKW half of A6 is a documented WALL (Dvoretzky–Kiefer–Wolfowitz absent from Mathlib) and is deliberately not stated here.

Statements

• centered_view_loss_hasSubgaussianMGF_of_mem_Icc — a loss a.e. in Set.Icc a b under a probability measure, once centered, has sub-Gaussian moment-generating-function parameter (‖b − a‖₊ / 2)². Shape of Mathlib’s ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc (Probability/Moments/SubGaussian.lean:860).
• bounded_view_loss_empirical_mean_upper_tail — for an independent centered family of bounded losses, the upper tail of the empirical mean decays as exp(−(nε)²/(2n(‖b−a‖₊/2)²)), riding ProbabilityTheory.measure_sum_range_ge_le_of_iIndepFun (SubGaussian.lean:787). No identical-distribution hypothesis is used.

Honest boundary

• Both bodies are sorry — nothing here is sealed; the recorded seal set is empty, [], and the page’s status: planned is the claim, no more. Sealing is rung work under the lean-proof skill (SymPy-first, seal ceremony).
• Independence is assumed of the centered family — exactly the family Mathlib’s sum theorem consumes; the payload showed no API transporting raw-loss independence through centering, and none was invented.
• The 0 < n rescaling wrapper is a convention of this statement, not of the Mathlib source.

Provenance

Drafted by the growth-loop pilot lane (.pi/workbench/lanes/tree_node_a6/ — sources.md, evidence.md, RESULT.md), harness-gated: declaration signatures verified against the pinned Mathlib source, compile gate lake build Ctrllib.HoeffdingViewLoss green (3079 jobs, two expected sorry warnings; one deprecated ∑ i in token modernized to ∑ i ∈ at the gate). Build copy ~/lean/ctrllib/Ctrllib/HoeffdingViewLoss.lean; this tracked mirror is the source of truth.