Lean module · Foundations
BanditRLProof.Algorithms.CUCBTriggerMGF
Primitive Bernoulli exponential bound for actual triggered observations. No stopping-time or adaptive-count tail is assumed here.
Module map
Imports
BanditRLProof.Algorithms.CUCBObservationMGF
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.CUCB.triggerFactor
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.triggerFactorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def triggerFactor {m : ℕ} (i : Fin m) (p tilt : ℝ) (z : Feedback m) : ℝ
theorem
BanditRLProof.CUCB.measurable_triggerFactor
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.measurable_triggerFactorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_triggerFactor {m : ℕ} (i : Fin m) (p tilt : ℝ) : Measurable (triggerFactor i p tilt)
theorem
BanditRLProof.CUCB.triggerFactor_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.triggerFactor_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem triggerFactor_nonneg {m : ℕ} (i : Fin m) (p tilt : ℝ) (z : Feedback m) : 0≤triggerFactor i p tilt z
theorem
BanditRLProof.CUCB.triggerFactor_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.CUCB.triggerFactor_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem triggerFactor_le {m : ℕ} (i : Fin m) (p tilt : ℝ) (z : Feedback m) : triggerFactor i p tilt z≤Real.exp (|tilt|+|(1-Real.exp (-tilt))*p|)
theorem
BanditRLProof.CUCB.triggerFactor_piecewise
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.triggerFactor_piecewiseReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem triggerFactor_piecewise {m : ℕ} (i : Fin m) (p tilt : ℝ) [DecidablePred (· ∈ observedSet i)] : triggerFactor i p tilt = (observedSet i).piecewise (fun _ => Real.exp (-tilt+(1-Real.exp (-tilt))*p)) (fun _ => Real.exp ((1-Real.exp (-tilt))*p))
theorem
BanditRLProof.CUCB.integrable_triggerFactor
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.integrable_triggerFactorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrable_triggerFactor {m : ℕ} (ν : Measure (Feedback m)) [IsProbabilityMeasure ν] (i : Fin m) (p tilt : ℝ) : Integrable (triggerFactor i p tilt) ν
theorem
BanditRLProof.CUCB.integral_triggerFactor
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.integral_triggerFactorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_triggerFactor {m : ℕ} (ν : Measure (Feedback m)) [IsProbabilityMeasure ν] (i : Fin m) (p tilt : ℝ) : (∫z, triggerFactor i p tilt z ∂ν) = (1-(ν (observedSet i)).toReal*(1-Real.exp (-tilt)))* Real.exp ((1-Real.exp (-tilt))*p)
theorem
BanditRLProof.CUCB.integral_triggerFactor_le_one
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.integral_triggerFactor_le_oneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_triggerFactor_le_one {m : ℕ} (ν : Measure (Feedback m)) [IsProbabilityMeasure ν] (i : Fin m) (p tilt : ℝ) (hp : p≤(ν (observedSet i)).toReal) (htilt : 0≤tilt) : (∫z, triggerFactor i p tilt z ∂ν)≤1