Lean module · Foundations
BanditRLProof.Algorithms.CUCBPolynomialThreshold
Exact polynomial-modulus inverse and source threshold expressions.
Module map
Imports
BanditRLProof.Algorithms.CUCBGapCutoff
Imported by
BanditRLProof, BanditRLProof.Algorithms.CUCBPolynomialIntegral
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.CUCB.SourceModel.inverseAt_polynomial
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.inverseAt_polynomialReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem inverseAt_polynomial (γ ω : ℝ) (hγ : 0<γ) (hω : 0<ω) (hf : ∀u, 0≤u → S.modulus u=γ*u^ω) {d : ℝ} (hd : d∈S.gapDomain) : S.inverseAt d=(d/γ)^(1/ω)
theorem
BanditRLProof.CUCB.SourceModel.inverseAt_polynomial_square
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.inverseAt_polynomial_squareReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem inverseAt_polynomial_square (γ ω : ℝ) (hγ : 0<γ) (hω : 0<ω) (hf : ∀u, 0≤u → S.modulus u=γ*u^ω) {d : ℝ} (hd : d∈S.gapDomain) : (S.inverseAt d)^2=(d/γ)^(2/ω)
theorem
BanditRLProof.CUCB.SourceModel.inverseAt_polynomial_reciprocal
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.inverseAt_polynomial_reciprocalReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem inverseAt_polynomial_reciprocal (γ ω : ℝ) (hγ : 0<γ) (hω : 0<ω) (hf : ∀u, 0≤u → S.modulus u=γ*u^ω) {d : ℝ} (hd : d∈S.gapDomain) : ((S.inverseAt d)^2)⁻¹=γ^(2/ω)*d^(-(2/ω))
theorem
BanditRLProof.CUCB.SourceModel.gapThreshold_polynomial_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.gapThreshold_polynomial_deterministicReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem gapThreshold_polynomial_deterministic (H : ℕ) (γ ω : ℝ) (hγ : 0<γ) (hω : 0<ω) (hf : ∀u, 0≤u → S.modulus u=γ*u^ω) {d : ℝ} (hd : d∈S.gapDomain) : S.gapThreshold H 1 d=6*Real.log (H:ℝ)*γ^(2/ω)*d^(-(2/ω))
theorem
BanditRLProof.CUCB.SourceModel.gapThreshold_polynomial_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.gapThreshold_polynomial_probabilisticReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem gapThreshold_polynomial_probabilistic (H : ℕ) (hH : 1≤H) (γ ω p : ℝ) (hγ : 0<γ) (hω : 0<ω) (hp : p≠1) (hf : ∀u, 0≤u → S.modulus u=γ*u^ω) {d : ℝ} (hd : d∈S.gapDomain) : S.gapThreshold H p d=max (12*Real.log (H:ℝ)/p*γ^(2/ω)*d^(-(2/ω))) (24*Real.log (H:ℝ)/p)
theorem
BanditRLProof.CUCB.SourceModel.gapThreshold_polynomial_upper
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.gapThreshold_polynomial_upperReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem gapThreshold_polynomial_upper (H : ℕ) (hH : 1≤H) (i : Fin m) (γ ω : ℝ) (hγ : 0<γ) (hω : 0<ω) (hf : ∀u, 0≤u → S.modulus u=γ*u^ω) {d : ℝ} (hd : d∈S.gapDomain) : S.gapThreshold H (M.minTrigger i) d≤ 12*Real.log (H:ℝ)/M.globalMinTrigger*γ^(2/ω)*d^(-(2/ω))+ 24*Real.log (H:ℝ)/M.minTrigger i