Lean module · Foundations
BanditRLProof.Algorithms.CUCBGapInverse
Scalar inverse on the full frozen positive-gap interval, and the exact integrable sampling threshold used in the refined source regret integral.
Module map
Imports
BanditRLProof.Algorithms.CUCBSourceModel
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.CUCB.thresholdCoefficient_antitone
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.thresholdCoefficient_antitoneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem thresholdCoefficient_antitone {u v p : ℝ} (hu : 0<u) (huv : u≤v) (hp : 0<p) : thresholdCoefficient v p≤thresholdCoefficient u p
def
BanditRLProof.CUCB.SourceModel.gapDomain
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.gapDomainReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def gapDomain : Set ℝ
def
BanditRLProof.CUCB.SourceModel.inverseAt
Compiled
The value outside the source inverse domain is zero by convention; all inverse and integral claims below explicitly stay inside the domain.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.SourceModel.inverseAtReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def inverseAt (d : ℝ) : ℝ
theorem
BanditRLProof.CUCB.SourceModel.inverseAt_spec
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_specReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem inverseAt_spec {d : ℝ} (hd : d∈S.gapDomain) : 0<S.inverseAt d ∧ S.modulus (S.inverseAt d)=d
theorem
BanditRLProof.CUCB.SourceModel.inverseAt_unique
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_uniqueReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem inverseAt_unique {d u : ℝ} (hd : d∈S.gapDomain) (hu : 0≤u) (he : S.modulus u=d) : S.inverseAt d=u
theorem
BanditRLProof.CUCB.SourceModel.inverseAt_gap
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_gapReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem inverseAt_gap (a : A) (ha : 0<S.gap a) : S.inverseAt (S.gap a)=S.inverseGap a
theorem
BanditRLProof.CUCB.SourceModel.inverseAt_strictMono
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_strictMonoReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem inverseAt_strictMono : StrictMonoOn S.inverseAt S.gapDomain
def
BanditRLProof.CUCB.SourceModel.gapThreshold
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.gapThresholdReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def gapThreshold (n : ℕ) (p d : ℝ) : ℝ
theorem
BanditRLProof.CUCB.SourceModel.gapThreshold_antitone
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_antitoneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem gapThreshold_antitone (n : ℕ) (hn : 1≤n) (p : ℝ) (hp : 0<p) : AntitoneOn (S.gapThreshold n p) S.gapDomain
theorem
BanditRLProof.CUCB.SourceModel.gapThreshold_nonneg
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_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem gapThreshold_nonneg (n : ℕ) (hn : 1≤n) (p : ℝ) (hp : 0<p) {d : ℝ} (hd : d∈S.gapDomain) : 0≤S.gapThreshold n p d
theorem
BanditRLProof.CUCB.SourceModel.gapThreshold_intervalIntegrable
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_intervalIntegrableReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem gapThreshold_intervalIntegrable (n : ℕ) (hn : 1≤n) (p : ℝ) (hp : 0<p) {a b : ℝ} (ha : a∈S.gapDomain) (hb : b∈S.gapDomain) : IntervalIntegrable (S.gapThreshold n p) volume a b