Lean module · Foundations
BanditRLProof.LowerBounds.SubgaussianMinimax
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.Algorithms.MOSSHistoryRegret, BanditRLProof.LowerBounds.GaussianHypothesisTesting
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
structure
BanditRLProof.LowerBounds.UnitSubgaussianBanditEnvironment
Compiled
The class in Chapter 13's main prose: gaps, not means, lie in [0,1].
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.UnitSubgaussianBanditEnvironmentReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
structure UnitSubgaussianBanditEnvironment (k : ℕ) where
def
BanditRLProof.LowerBounds.UnitGaussianBanditEnvironment.toSubgaussian
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 identity
declaration:BanditRLProof.LowerBounds.UnitGaussianBanditEnvironment.toSubgaussianReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def UnitGaussianBanditEnvironment.toSubgaussian {k : ℕ} (e : UnitGaussianBanditEnvironment k) : UnitSubgaussianBanditEnvironment k where
def
BanditRLProof.LowerBounds.subgaussianExpectedPseudoRegret
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 identity
declaration:BanditRLProof.LowerBounds.subgaussianExpectedPseudoRegretReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def subgaussianExpectedPseudoRegret {k : ℕ} (algorithm : Thompson.HistoryAlgorithm (Fin k) ℝ) (e : UnitSubgaussianBanditEnvironment k) (t : ℕ) : ℝ≥0∞
def
BanditRLProof.LowerBounds.subgaussianWorstCaseExpectedPseudoRegret
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 identity
declaration:BanditRLProof.LowerBounds.subgaussianWorstCaseExpectedPseudoRegretReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def subgaussianWorstCaseExpectedPseudoRegret (k : ℕ) (algorithm : Thompson.HistoryAlgorithm (Fin k) ℝ) (t : ℕ) : ℝ≥0∞
def
BanditRLProof.LowerBounds.subgaussianMinimaxExpectedPseudoRegret
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 identity
declaration:BanditRLProof.LowerBounds.subgaussianMinimaxExpectedPseudoRegretReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def subgaussianMinimaxExpectedPseudoRegret (k t : ℕ) : ℝ≥0∞
theorem
BanditRLProof.LowerBounds.subgaussianExpectedPseudoRegret_gaussian
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 identity
declaration:BanditRLProof.LowerBounds.subgaussianExpectedPseudoRegret_gaussianReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem subgaussianExpectedPseudoRegret_gaussian {k : ℕ} (algorithm : Thompson.HistoryAlgorithm (Fin k) ℝ) (e : UnitGaussianBanditEnvironment k) (t : ℕ) : subgaussianExpectedPseudoRegret algorithm e.toSubgaussian t = gaussianExpectedPseudoRegret algorithm e t
theorem
BanditRLProof.LowerBounds.unitGaussianMinimax_le_subgaussianMinimax
Compiled
Gaussian subclass inclusion is on the identical policy and regret functional.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.LowerBounds.unitGaussianMinimax_le_subgaussianMinimaxReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem unitGaussianMinimax_le_subgaussianMinimax (k t : ℕ) : unitGaussianMinimaxExpectedPseudoRegret k t ≤ subgaussianMinimaxExpectedPseudoRegret k t
theorem
BanditRLProof.LowerBounds.moss_subgaussianExpectedPseudoRegret_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 identity
declaration:BanditRLProof.LowerBounds.moss_subgaussianExpectedPseudoRegret_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem moss_subgaussianExpectedPseudoRegret_le {k : ℕ} [NeZero k] (hk : 0 < k) (t : ℕ) (hkt : k ≤ t+1) (e : UnitSubgaussianBanditEnvironment k) : subgaussianExpectedPseudoRegret (MOSS.historyAlgorithm hk (t+1)) e t ≤ ENNReal.ofReal (40*Real.sqrt ((k : ℝ)*(t+1)))
theorem
BanditRLProof.LowerBounds.subgaussianMinimax_sandwich
Compiled
Chapter 13's broader-class minimax sandwich with universal constants.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret · Chapter 13: Lower Bounds: Basic Ideas
Canonical node identity
declaration:BanditRLProof.LowerBounds.subgaussianMinimax_sandwichReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem subgaussianMinimax_sandwich {k : ℕ} [NeZero k] (hk : 1 < k) (t : ℕ) (hkt : k ≤ t+1) : ENNReal.ofReal ((1/54 : ℝ)*Real.sqrt ((k : ℝ)*(t+1))) ≤ subgaussianMinimaxExpectedPseudoRegret k t ∧ subgaussianMinimaxExpectedPseudoRegret k t ≤ subgaussianWorstCaseExpectedPseudoRegret k (MOSS.historyAlgorithm (by omega) (t+1)) t ∧ subgaussianWorstCaseExpectedPseudoRegret k (MOSS.historyAlgorithm (by omega) (t+1)) t ≤ ENNReal.ofReal (40*Real.sqrt ((k : ℝ)*(t+1)))
theorem
BanditRLProof.LowerBounds.moss_nearMinimax
Compiled
Algorithm 7 is minimax optimal up to one universal multiplicative factor.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret · Chapter 13: Lower Bounds: Basic Ideas
Canonical node identity
declaration:BanditRLProof.LowerBounds.moss_nearMinimaxReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem moss_nearMinimax {k : ℕ} [NeZero k] (hk : 1 < k) (t : ℕ) (hkt : k ≤ t+1) : subgaussianWorstCaseExpectedPseudoRegret k (MOSS.historyAlgorithm (by omega) (t+1)) t ≤ 2160 * subgaussianMinimaxExpectedPseudoRegret k t