BanditRLProof.Algorithms.MOSSOptimism

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

def centeredIndex (X : ℕ → Ω → ℝ) (δ : ℝ) (s : ℕ) (ω : Ω) : ℝ

Positive part of the worst centered index through sample count n.

def optimismDeficit (X : ℕ → Ω → ℝ) (δ : ℝ) : ℕ → Ω → ℝ | 0, _ => 0 | n+1, ω => max (optimismDeficit X δ n ω) (-centeredIndex X δ (n+1) ω) theorem optimismDeficit_nonneg (X : ℕ → Ω → ℝ) (δ : ℝ) (n : ℕ) (ω : Ω) : 0 ≤ optimismDeficit X δ n ω

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

theorem optimismDeficit_nonneg (X : ℕ → Ω → ℝ) (δ : ℝ) (n : ℕ) (ω : Ω) : 0 ≤ optimismDeficit X δ n ω

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

theorem le_optimismDeficit_iff (X : ℕ → Ω → ℝ) (δ gap : ℝ) (hg : 0 < gap) (n : ℕ) (ω : Ω) : gap ≤ optimismDeficit X δ n ω ↔ ∃ s : ℕ, 0 < s ∧ s ≤ n ∧ centeredIndex X δ s ω + gap ≤ 0

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

theorem stronglyMeasurable_centeredIndex (X : ℕ → Ω → ℝ) (hX : ∀ i, StronglyMeasurable (X i)) (δ : ℝ) (s : ℕ) : StronglyMeasurable (centeredIndex X δ s)

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

theorem integrable_centeredIndex [IsFiniteMeasure μ] (X : ℕ → Ω → ℝ) (hX : ∀ i, Integrable (X i) μ) (δ : ℝ) (s : ℕ) : Integrable (centeredIndex X δ s) μ

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

theorem stronglyMeasurable_optimismDeficit (X : ℕ → Ω → ℝ) (hX : ∀ i, StronglyMeasurable (X i)) (δ : ℝ) (n : ℕ) : StronglyMeasurable (optimismDeficit X δ n)

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

theorem integrable_optimismDeficit [IsFiniteMeasure μ] (X : ℕ → Ω → ℝ) (hX : ∀ i, Integrable (X i) μ) (δ : ℝ) (n : ℕ) : Integrable (optimismDeficit X δ n) μ

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

theorem measure_optimismDeficit_ge_le [IsProbabilityMeasure μ] (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) (n : ℕ) : μ {ω | gap ≤ optimismDeficit X δ n ω} ≤ ENNReal.ofReal (15*δ/gap^2)

Layer-cake identity with integrability derived from the coordinate MGF contracts.

theorem integral_optimismDeficit_eq_integral_tail [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hsubG : ∀ i, HasSubgaussianMGF (X i) 1 μ) (δ : ℝ) (n : ℕ) : ∫ ω, optimismDeficit X δ n ω ∂μ = ∫ gap in Set.Ioi 0, μ.real {ω | gap ≤ optimismDeficit X δ n ω}

Source expected optimism-deficit bound, derived from the uniform tail.

theorem integral_optimismDeficit_le_two_sqrt [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hXm : ∀ i, StronglyMeasurable (X i)) (hind : iIndepFun X μ) (hmean : ∀ i, ∫ ω, X i ω ∂μ = 0) (hsubG : ∀ i, HasSubgaussianMGF (X i) 1 μ) (δ : ℝ) (hδ : 0 < δ) (n : ℕ) : ∫ ω, optimismDeficit X δ n ω ∂μ ≤ 2*sqrt (15*δ)

The printed 16*sqrt(n*k) optimism contribution in Theorem 9.1.

theorem twice_horizon_mul_integral_optimismDeficit_le [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hXm : ∀ i, StronglyMeasurable (X i)) (hind : iIndepFun X μ) (hmean : ∀ i, ∫ ω, X i ω ∂μ = 0) (hsubG : ∀ i, HasSubgaussianMGF (X i) 1 μ) (n k : ℕ) (hn : 0 < n) (hk : 0 < k) : 2*(n : ℝ)*(∫ ω, optimismDeficit X ((k : ℝ)/n) n ω ∂μ) ≤ 16*sqrt ((n : ℝ)*k)