Lean module · Foundations
BanditRLProof.Algorithms.HOORegretAlgebra
Explicit geometric reduction of the source's three regret sums.
Module map
Imports
BanditRLProof.Algorithms.HOOExpectedRegret
Imported by
BanditRLProof, BanditRLProof.Algorithms.HOODepthOptimization
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.HOO.regretSumConstant
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.HOO.regretSumConstantReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def regretSumConstant (ν₁ ν₂ ρ d K : ℝ) : ℝ
theorem
BanditRLProof.HOO.regretSumConstant_pos
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.HOO.regretSumConstant_posReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem regretSumConstant_pos {ν₁ ν₂ ρ d K : ℝ} (h1 : 0<ν₁) (h2 : 0<ν₂) (hr : 0<ρ) (hK : 0<K) : 0<regretSumConstant ν₁ ν₂ ρ d K
theorem
BanditRLProof.HOO.nat_pow_rpow
Compiled Internal helper
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.HOO.nat_pow_rpowReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
private theorem nat_pow_rpow (r z : ℝ) (hr : 0≤r) (h : ℕ) : (r^h)^z=(r^z)^h
theorem
BanditRLProof.HOO.regret_level_le
Compiled
The single-level algebra keeps the child's depth h+1 in the visit bound, and only then reduces both contributions to one geometric sequence.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.regret_level_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem regret_level_le {ν₁ ν₂ ρ d K L : ℝ} (h1 : 0<ν₁) (h2 : 0<ν₂) (hr : 0<ρ) (hr1 : ρ≤1) (hK : 0<K) (hL : Real.log 2≤L) (h : ℕ) : 4*(ν₁*ρ^h)*(K*(ν₂*ρ^h)^(-d)) + 8*(ν₁*ρ^h)*(K*(ν₂*ρ^h)^(-d))*(8*L/(ν₁*ρ^(h+1))^2+4) ≤ regretSumConstant ν₁ ν₂ ρ d K * L * (ρ^(-(1+d)))^h
theorem
BanditRLProof.HOO.regret_sums_le
Compiled
Finite sums are reduced with an explicit environment-only constant.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.regret_sums_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem regret_sums_le {ν₁ ν₂ ρ d K L : ℝ} (h1 : 0<ν₁) (h2 : 0<ν₂) (hr : 0<ρ) (hr1 : ρ<1) (hd : 0<d) (hK : 0<K) (hL : Real.log 2≤L) (H : ℕ) : (∑ h ∈ Finset.range H, 4*(ν₁*ρ^h)*(K*(ν₂*ρ^h)^(-d))) + (∑ h ∈ Finset.range H, 8*(ν₁*ρ^h)*(K*(ν₂*ρ^h)^(-d)) * (8*L/(ν₁*ρ^(h+1))^2+4)) ≤ (regretSumConstant ν₁ ν₂ ρ d K / (ρ^(-(1+d))-1))*L*(ρ^H)^(-(1+d))