BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Lean module · Foundations

BanditRLProof.Algorithms.MOSSExpectedOccupancy

Generated source map for this Lean module.

Module map

Declarations
7
Placeholders
0

Imports

BanditRLProof.Algorithms.MOSSOccupancy, BanditRLProof.ConcentrationIndexOccupancy, BanditRLProof.Algorithms.MOSSConstants

Imported by

BanditRLProof, BanditRLProof.Algorithms.MOSSStream

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.MOSS.streamMean Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.MOSS.streamMean

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

def streamMean (X : ℕ → Ω → ℝ) (ω : Ω) (s : ℕ) : ℝ
Source line 10 Chapter context: Foundations
theorem BanditRLProof.MOSS.fixedLogExceedanceCount_eq_fixedRadiusCount Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.MOSS.fixedLogExceedanceCount_eq_fixedRadiusCount

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem fixedLogExceedanceCount_eq_fixedRadiusCount (X : ℕ → Ω → ℝ) (δ gap : ℝ) (n : ℕ) (ω : Ω) : fixedLogExceedanceCount (streamMean X ω) δ gap n = Concentration.fixedRadiusCount X (2*logPlus (gap^2/δ)) (gap/2) n ω
Source line 12 Chapter context: Foundations
theorem BanditRLProof.MOSS.integrable_indexExceedanceCount Compiled

Finite measurable indicator counts are integrable, without tail assumptions.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.MOSS.integrable_indexExceedanceCount

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem integrable_indexExceedanceCount (X : ℕ → Ω → ℝ) (hXm : ∀ i, StronglyMeasurable (X i)) (δ gap : ℝ) (n : ℕ) : Integrable (fun ω => indexExceedanceCount (streamMean X ω) δ gap n) μ
Source line 25 Chapter context: Foundations
theorem BanditRLProof.MOSS.integral_indexExceedanceCount_le_sharp Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.MOSS.integral_indexExceedanceCount_le_sharp

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem integral_indexExceedanceCount_le_sharp (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) (hlarge : δ < gap^2) (n : ℕ) : (∫ ω, indexExceedanceCount (streamMean X ω) δ gap n ∂μ) ≤ 1/gap^2 + (8/gap^2)*(2*logPlus (gap^2/δ)+sqrt (Real.pi*(2*logPlus (gap^2/δ)))+1)
Source line 37 Chapter context: Foundations
theorem BanditRLProof.MOSS.integral_indexExceedanceCount_le Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.MOSS.integral_indexExceedanceCount_le

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem integral_indexExceedanceCount_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) (hlarge : δ < gap^2) (n : ℕ) : (∫ ω, indexExceedanceCount (streamMean X ω) δ gap n ∂μ) ≤ 1/gap^2 + 1 + (8/gap^2)*(2*logPlus (gap^2/δ)+sqrt (Real.pi*(2*logPlus (gap^2/δ)))+1)
Source line 68 Chapter context: Foundations
theorem BanditRLProof.MOSS.gap_mul_integral_indexExceedanceCount_le_sharp Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.MOSS.gap_mul_integral_indexExceedanceCount_le_sharp

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem gap_mul_integral_indexExceedanceCount_le_sharp (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) (hlarge : 8*sqrt δ ≤ gap) (n : ℕ) : gap*(∫ ω, indexExceedanceCount (streamMean X ω) δ gap n ∂μ) ≤ 15/sqrt δ
Source line 77 Chapter context: Foundations
theorem BanditRLProof.MOSS.gap_mul_integral_indexExceedanceCount_le Compiled

Source large-gap weighted occupancy bound, before selected-count transport.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identitydeclaration:BanditRLProof.MOSS.gap_mul_integral_indexExceedanceCount_le

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem gap_mul_integral_indexExceedanceCount_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) (hlarge : 8*sqrt δ ≤ gap) (n : ℕ) : gap*(∫ ω, indexExceedanceCount (streamMean X ω) δ gap n ∂μ) ≤ gap+15/sqrt δ
Source line 90 Chapter context: Foundations