Lean module · Foundations
BanditRLProof.Algorithms.CUCBPolynomialIntegral
Integration of the actual source thresholds under a polynomial modulus.
Module map
Imports
BanditRLProof.Algorithms.CUCBPolynomialThreshold, BanditRLProof.PowerTailIntegral
Imported by
BanditRLProof, BanditRLProof.Algorithms.CUCBPolynomialRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.CUCB.SourceModel.threshold_integral_le_power
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.CUCB.SourceModel.threshold_integral_le_powerReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem threshold_integral_le_power (H : ℕ) (hH : 1≤H) (i : Fin m) (a : ℝ) (ha : a∈S.gapDomain) (q B c : ℝ) (hq : 1<q) (hB : 0≤B) (hc : 0≤c) (he : ∀x∈Set.Icc a (maxPositiveGap S.score M.trueInput S.alpha), S.gapThreshold H (M.minTrigger i) x≤B*x^(-q)+c) : (∫x in a..maxPositiveGap S.score M.trueInput S.alpha, S.gapThreshold H (M.minTrigger i) x)≤ B*a^(1-q)/(q-1)+c*maxPositiveGap S.score M.trueInput S.alpha
theorem
BanditRLProof.CUCB.SourceModel.polynomial_threshold_integral_deterministic
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.CUCB.SourceModel.polynomial_threshold_integral_deterministicReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem polynomial_threshold_integral_deterministic (H : ℕ) (hH : 1≤H) (i : Fin m) (hp : M.minTrigger i=1) (γ ω : ℝ) (hγ : 0<γ) (hω : 0<ω) (hω1 : ω≤1) (hf : ∀u, 0≤u → S.modulus u=γ*u^ω) (a : ℝ) (ha : a∈S.gapDomain) : (∫x in a..maxPositiveGap S.score M.trueInput S.alpha, S.gapThreshold H (M.minTrigger i) x)≤ (6*Real.log (H:ℝ)*γ^(2/ω))*a^(1-2/ω)/(2/ω-1)
theorem
BanditRLProof.CUCB.SourceModel.polynomial_threshold_integral_probabilistic
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
Indexed settings: Combinatorial bandits
Canonical node identity
declaration:BanditRLProof.CUCB.SourceModel.polynomial_threshold_integral_probabilisticReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem polynomial_threshold_integral_probabilistic (H : ℕ) (hH : 1≤H) (i : Fin m) (γ ω : ℝ) (hγ : 0<γ) (hω : 0<ω) (hω1 : ω≤1) (hf : ∀u, 0≤u → S.modulus u=γ*u^ω) (a : ℝ) (ha : a∈S.gapDomain) : (∫x in a..maxPositiveGap S.score M.trueInput S.alpha, S.gapThreshold H (M.minTrigger i) x)≤ (12*Real.log (H:ℝ)/M.globalMinTrigger*γ^(2/ω))*a^(1-2/ω)/(2/ω-1)+ (24*Real.log (H:ℝ)/M.minTrigger i)*maxPositiveGap S.score M.trueInput S.alpha
theorem
BanditRLProof.CUCB.SourceModel.polynomial_cutoff_regret_deterministic
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.CUCB.SourceModel.polynomial_cutoff_regret_deterministicReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem polynomial_cutoff_regret_deterministic (H : ℕ) (hH : 1≤H) (hp : M.globalMinTrigger=1) (γ ω : ℝ) (hγ : 0<γ) (hω : 0<ω) (hω1 : ω≤1) (hf : ∀u, 0≤u → S.modulus u=γ*u^ω) (a : ℝ) (ha : a∈S.gapDomain) : S.approximationRegret H≤(H:ℝ)*a+ ((m:ℝ)*(6*Real.log (H:ℝ)*γ^(2/ω)))*a^(1-2/ω)/(2/ω-1)+ (1+Real.pi^2/3)*(m:ℝ)*maxPositiveGap S.score M.trueInput S.alpha
theorem
BanditRLProof.CUCB.SourceModel.polynomial_cutoff_regret_probabilistic
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.CUCB.SourceModel.polynomial_cutoff_regret_probabilisticReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem polynomial_cutoff_regret_probabilistic (H : ℕ) (hH : 1≤H) (hp : M.globalMinTrigger<1) (γ ω : ℝ) (hγ : 0<γ) (hω : 0<ω) (hω1 : ω≤1) (hf : ∀u, 0≤u → S.modulus u=γ*u^ω) (a : ℝ) (ha : a∈S.gapDomain) : S.approximationRegret H≤(H:ℝ)*a+ ((m:ℝ)*(12*Real.log (H:ℝ)/M.globalMinTrigger*γ^(2/ω)))*a^(1-2/ω)/(2/ω-1)+ (1+Real.pi^2/2)*(m:ℝ)*maxPositiveGap S.score M.trueInput S.alpha+ ∑i:Fin m, (24*Real.log (H:ℝ)/M.minTrigger i)*maxPositiveGap S.score M.trueInput S.alpha