Lean module · Probability layer
BanditRLProof.ConcentrationIndexOccupancy
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.ConcentrationGaussianOccupancy, BanditRLProof.ConcentrationMartingaleMaximal, BanditRLProof.ConcentrationCappedOccupancy
Imported by
BanditRLProof, BanditRLProof.Algorithms.MOSSExpectedOccupancy
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Concentration.fixedRadiusMeanEvent
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.Concentration.fixedRadiusMeanEventReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def fixedRadiusMeanEvent (X : ℕ → Ω → ℝ) (a ε : ℝ) (s : ℕ) : Set Ω
theorem
BanditRLProof.Concentration.measure_fixedRadiusMeanEvent_le
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.Concentration.measure_fixedRadiusMeanEvent_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measure_fixedRadiusMeanEvent_le (X : ℕ → Ω → ℝ) (hXm : ∀ i, StronglyMeasurable (X i)) (hind : iIndepFun X μ) (hmean : ∀ i, ∫ ω, X i ω ∂μ = 0) (hsubG : ∀ i, HasSubgaussianMGF (X i) 1 μ) (a ε : ℝ) (ha : 0 < a) (hε : 0 < ε) (s : ℕ) (hs : 2*a/ε^2 < (s : ℝ)) : μ (fixedRadiusMeanEvent X a ε s) ≤ ENNReal.ofReal (occupancyTail a ε s)
theorem
BanditRLProof.Concentration.sum_measureReal_fixedRadiusMeanEvent_le
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.Concentration.sum_measureReal_fixedRadiusMeanEvent_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sum_measureReal_fixedRadiusMeanEvent_le (X : ℕ → Ω → ℝ) (hXm : ∀ i, StronglyMeasurable (X i)) (hind : iIndepFun X μ) (hmean : ∀ i, ∫ ω, X i ω ∂μ = 0) (hsubG : ∀ i, HasSubgaussianMGF (X i) 1 μ) (a ε : ℝ) (ha : 0 < a) (hε : 0 < ε) (n : ℕ) : (∑ i ∈ range n, μ.real (fixedRadiusMeanEvent X a ε (i+1))) ≤ 1+(2/ε^2)*(a+sqrt (Real.pi*a)+1)
theorem
BanditRLProof.Concentration.measurableSet_fixedRadiusMeanEvent
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.Concentration.measurableSet_fixedRadiusMeanEventReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurableSet_fixedRadiusMeanEvent (X : ℕ → Ω → ℝ) (hXm : ∀ i, StronglyMeasurable (X i)) (a ε : ℝ) (s : ℕ) : MeasurableSet (fixedRadiusMeanEvent X a ε s)
def
BanditRLProof.Concentration.fixedRadiusCount
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.Concentration.fixedRadiusCountReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def fixedRadiusCount (X : ℕ → Ω → ℝ) (a ε : ℝ) (n : ℕ) (ω : Ω) : ℝ
theorem
BanditRLProof.Concentration.integrable_fixedRadiusCount
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.Concentration.integrable_fixedRadiusCountReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrable_fixedRadiusCount (X : ℕ → Ω → ℝ) (hXm : ∀ i, StronglyMeasurable (X i)) (a ε : ℝ) (n : ℕ) : Integrable (fixedRadiusCount X a ε n) μ
theorem
BanditRLProof.Concentration.integral_fixedRadiusCount_le
Compiled
Source Lemma 8.2 expected-count conclusion for centered unit-subgaussian coordinates.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.Concentration.integral_fixedRadiusCount_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_fixedRadiusCount_le (X : ℕ → Ω → ℝ) (hXm : ∀ i, StronglyMeasurable (X i)) (hind : iIndepFun X μ) (hmean : ∀ i, ∫ ω, X i ω ∂μ = 0) (hsubG : ∀ i, HasSubgaussianMGF (X i) 1 μ) (a ε : ℝ) (ha : 0 < a) (hε : 0 < ε) (n : ℕ) : (∫ ω, fixedRadiusCount X a ε n ω ∂μ) ≤ 1+(2/ε^2)*(a+sqrt (Real.pi*a)+1)
theorem
BanditRLProof.Concentration.integral_fixedRadiusCount_le_sharp
Compiled
Sharper count bound: the removed additive one pays for MOSS initialization.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.Concentration.integral_fixedRadiusCount_le_sharpReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_fixedRadiusCount_le_sharp (X : ℕ → Ω → ℝ) (hXm : ∀ i, StronglyMeasurable (X i)) (hind : iIndepFun X μ) (hmean : ∀ i, ∫ ω, X i ω ∂μ = 0) (hsubG : ∀ i, HasSubgaussianMGF (X i) 1 μ) (a ε : ℝ) (ha : 0 < a) (hε : 0 < ε) (n : ℕ) : (∫ ω, fixedRadiusCount X a ε n ω ∂μ) ≤ (2/ε^2)*(a+sqrt (Real.pi*a)+1)