Lean module · Foundations
BanditRLProof.Algorithms.MOSSConstants
Generated source map for this Lean module.
Module map
Imports
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.MOSS.log_sixtyFour_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.MOSS.log_sixtyFour_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem log_sixtyFour_le : log (64 : ℝ) ≤ 17/4
theorem
BanditRLProof.MOSS.largeGap_constant_fifteen
Compiled
Dimensionless large-gap numerical estimate used in source Theorem 9.1.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.MOSS.largeGap_constant_fifteenReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem largeGap_constant_fifteen (q : ℝ) (hq : 64 ≤ q) : (1+8*(2*log q+sqrt (Real.pi*(2*log q))+1))/sqrt q ≤ 15
theorem
BanditRLProof.MOSS.largeGap_scaled_constant_fifteen
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.MOSS.largeGap_scaled_constant_fifteenReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem largeGap_scaled_constant_fifteen (δ gap : ℝ) (hδ : 0 < δ) (hg : 0 < gap) (hlarge : 8*sqrt δ ≤ gap) : gap*(1/gap^2+1+(8/gap^2)*(2*logPlus (gap^2/δ)+ sqrt (Real.pi*(2*logPlus (gap^2/δ)))+1)) ≤ gap+15/sqrt δ