Lean module · Foundations
BanditRLProof.PowerTailIntegral
Exact power-tail integration and balancing identities.
Module map
Imports
No project-local imports.
Imported by
BanditRLProof, BanditRLProof.Algorithms.CUCBPolynomialIntegral, BanditRLProof.PowerCutoffNormalization
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.PowerTailIntegral.integral_power_tail_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.PowerTailIntegral.integral_power_tail_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_power_tail_le (a b q : ℝ) (ha : 0<a) (hab : a≤b) (hq : 1<q) : (∫x in a..b, x^(-q))≤a^(1-q)/(q-1)
theorem
BanditRLProof.PowerTailIntegral.cutoff_balance
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.PowerTailIntegral.cutoff_balanceReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem cutoff_balance (K N q : ℝ) (hK : 0<K) (hN : 0<N) (hq : 0<q) : K*((K/N)^(1/q))^(-q)=N
theorem
BanditRLProof.PowerTailIntegral.cutoff_objective
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.PowerTailIntegral.cutoff_objectiveReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem cutoff_objective (K N q : ℝ) (hK : 0<K) (hN : 0<N) (hq : 1<q) : N*(K/N)^(1/q)+K*((K/N)^(1/q))^(1-q)/(q-1)= q/(q-1)*(N*(K/N)^(1/q))