Lean module · Foundations
BanditRLProof.Algorithms.HOODepthOptimization
Integer depth optimization with positive logarithms, including horizon one.
Module map
Imports
BanditRLProof.Algorithms.HOORegretAlgebra
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.HOO.balance_identities
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.balance_identitiesReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
private theorem balance_identities {N L d : ℝ} (hN : 0<N) (hL : 0<L) (hd : 0<d) : N*(L/N)^(1/(d+2)) = N^((d+1)/(d+2))*L^(1/(d+2)) ∧ L*((L/N)^(1/(d+2)))^(-(1+d)) = N^((d+1)/(d+2))*L^(1/(d+2))
theorem
BanditRLProof.HOO.exists_regret_depth
Compiled
Chooses a genuine integer H>=1; no real-valued cutoff or asymptotic rounding assumption is used. The same estimate works when L=N.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.HOO.exists_regret_depthReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem exists_regret_depth {ρ d A B N L : ℝ} (hr : 0<ρ) (hr1 : ρ<1) (hd : 0<d) (hA : 0≤A) (hB : 0≤B) (hN : 0<N) (hL : 0<L) (hLN : L≤N) : ∃ H : ℕ, 1≤H ∧ A*N*ρ^H+B*L*(ρ^H)^(-(1+d)) ≤ (A+B*ρ^(-(1+d)))*N^((d+1)/(d+2))*L^(1/(d+2))
theorem
BanditRLProof.HOO.log_horizon_pos_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.HOO.log_horizon_pos_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem log_horizon_pos_le (N : ℕ) (hN : 1≤N) : 0<Real.log (max (N:ℝ) 2) ∧ Real.log (max (N:ℝ) 2)≤(N:ℝ)