BanditRLProof.Algorithms.MOSSPeeling

No declaration docstring is present; use the chapter context and exact statement below.

theorem logPlus_mono {x y : ℝ} (hxy : x ≤ y) : logPlus x ≤ logPlus y

No declaration docstring is present; use the chapter context and exact statement below.

theorem exp_neg_logPlus_inv_le (x : ℝ) (hx : 0 < x) : exp (-logPlus (1 / x)) ≤ x

Scaled source confidence barrier, avoiding division by the sample count.

noncomputable def peelingBarrier (δ gap s : ℝ) : ℝ

Lower barrier common to one dyadic block m<=s<=2m.

noncomputable def blockBarrier (δ gap m : ℝ) : ℝ

No declaration docstring is present; use the chapter context and exact statement below.

theorem blockBarrier_pos (δ gap m : ℝ) (hm : 0 < m) (hg : 0 < gap) : 0 < blockBarrier δ gap m

No declaration docstring is present; use the chapter context and exact statement below.

theorem blockBarrier_le_peelingBarrier (δ gap m s : ℝ) (hδ : 0 < δ) (hg : 0 ≤ gap) (hm : 0 < m) (hms : m ≤ s) (hsm : s ≤ 2*m) : blockBarrier δ gap m ≤ peelingBarrier δ gap s

Scalar exponential bound used after Doob on one dyadic block.

theorem exp_neg_blockBarrier_sq_le (δ gap m : ℝ) (hδ : 0 < δ) (hg : 0 ≤ gap) (hm : 0 < m) : exp (-(blockBarrier δ gap m)^2 / (4*m)) ≤ (2*m*δ) * exp (-(m*gap^2/4))

Centered partial sum in the source's one-based sample convention.

noncomputable def peelingSum {Ω : Type*} (X : ℕ → Ω → ℝ) (s : ℕ) (ω : Ω) : ℝ

Maximal partial-sum event dominating one dyadic block.

def blockBadEvent {Ω : Type*} (X : ℕ → Ω → ℝ) (δ gap : ℝ) (m : ℕ) : Set Ω

No declaration docstring is present; use the chapter context and exact statement below.

theorem measure_blockBadEvent_le (X : ℕ → Ω → ℝ) (hXm : ∀ i, StronglyMeasurable (X i)) (hind : iIndepFun X μ) (hmean : ∀ i, ∫ ω, X i ω ∂μ = 0) (hsubG : ∀ i, HasSubgaussianMGF (X i) 1 μ) (δ gap : ℝ) (hδ : 0 < δ) (hg : 0 < gap) (m : ℕ) (hm : 0 < m) : μ (blockBadEvent X δ gap m) ≤ ENNReal.ofReal ((2*(m : ℝ)*δ) * exp (-((m : ℝ)*gap^2/4)))

All positive-sample source bad events, in scaled partial-sum form.

def scaledBadEvent (X : ℕ → Ω → ℝ) (δ gap : ℝ) : Set Ω

Countable dyadic peeling with the printed constant 15.

theorem measure_scaledBadEvent_le_fifteen (X : ℕ → Ω → ℝ) (hXm : ∀ i, StronglyMeasurable (X i)) (hind : iIndepFun X μ) (hmean : ∀ i, ∫ ω, X i ω ∂μ = 0) (hsubG : ∀ i, HasSubgaussianMGF (X i) 1 μ) (δ gap : ℝ) (hδ : 0 < δ) (hg : 0 < gap) : μ (scaledBadEvent X δ gap) ≤ ENNReal.ofReal (15*δ/gap^2)

The actual empirical-mean bad event appearing in source Lemma 9.3.

def meanBadEvent (X : ℕ → Ω → ℝ) (δ gap : ℝ) : Set Ω

No declaration docstring is present; use the chapter context and exact statement below.

theorem meanBadEvent_subset_scaledBadEvent (X : ℕ → Ω → ℝ) (δ gap : ℝ) : meanBadEvent X δ gap ⊆ scaledBadEvent X δ gap

Source Lemma 9.3, with the printed constant and actual mean/radius event. The proof works for every positive delta, hence in particular delta in (0,1). The explicit centered-coordinate contracts are later instantiated by MOSS.

theorem measure_meanBadEvent_le_fifteen (X : ℕ → Ω → ℝ) (hXm : ∀ i, StronglyMeasurable (X i)) (hind : iIndepFun X μ) (hmean : ∀ i, ∫ ω, X i ω ∂μ = 0) (hsubG : ∀ i, HasSubgaussianMGF (X i) 1 μ) (δ gap : ℝ) (hδ : 0 < δ) (hg : 0 < gap) : μ (meanBadEvent X δ gap) ≤ ENNReal.ofReal (15*δ/gap^2)