Lean module · Foundations
BanditRLProof.Algorithms.CUCBChargedConditional
Conditional trigger factor along the actual history-dependent charging recursion and actual randomized CUCB trajectory.
Module map
Imports
BanditRLProof.Algorithms.CUCBChargedMGF
Imported by
BanditRLProof, BanditRLProof.Algorithms.CUCBChargedConcentration
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.CUCB.ChargeData.prefixActions
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.ChargeData.prefixActionsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def prefixActions (n : ℕ) (h : (i : Finset.Iic n) → Round A m) : ℕ → A
def
BanditRLProof.CUCB.ChargeData.prefixCounters
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.ChargeData.prefixCountersReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def prefixCounters (n : ℕ) (h : (i : Finset.Iic n) → Round A m) : Fin m → ℕ
theorem
BanditRLProof.CUCB.ChargeData.prefixCounters_eq
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.ChargeData.prefixCounters_eqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem prefixCounters_eq (n : ℕ) (Y : ℕ → Round A m) : C.prefixCounters n (Preorder.frestrictLe n Y) = C.counters (fun t => (Y t).1) (n+1)
theorem
BanditRLProof.CUCB.ChargeData.measurable_prefixActions
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.ChargeData.measurable_prefixActionsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_prefixActions (n : ℕ) : Measurable (prefixActions (A:=A) (m:=m) n)
theorem
BanditRLProof.CUCB.ChargeData.measurable_prefixCounters
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.ChargeData.measurable_prefixCountersReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_prefixCounters (n : ℕ) : Measurable (C.prefixCounters n)
theorem
BanditRLProof.CUCB.ChargeData.cucb_condExp_chargedTriggerFactor
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.ChargeData.cucb_condExp_chargedTriggerFactorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem cucb_condExp_chargedTriggerFactor (n : ℕ) (tilt : ℝ) (htilt : 0≤tilt) : (cucbTrajectory oracle environment)[fun Y => C.chargedTriggerFactor i tilt (C.counters (fun t => (Y t).1) (n+1)) (Y (n+1)) | MeasurableSpace.comap (Preorder.frestrictLe n) inferInstance] ≤ᵐ[cucbTrajectory oracle environment] fun _ => 1
theorem
BanditRLProof.CUCB.ChargeData.cucb_initial_chargedTriggerFactor
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.ChargeData.cucb_initial_chargedTriggerFactorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem cucb_initial_chargedTriggerFactor (tilt : ℝ) (htilt : 0≤tilt) : (∫Y, C.chargedTriggerFactor i tilt (C.counters (fun t => (Y t).1) 0) (Y 0) ∂cucbTrajectory oracle environment)≤1