Lean module · Foundations
BanditRLProof.Algorithms.CUCBChargedMGF
The actual oracle mixture preserves the trigger bound for the normalized charge, which is chosen before the environment draws the current feedback.
Module map
Imports
BanditRLProof.Algorithms.CUCBCharge, BanditRLProof.Algorithms.CUCBTriggerMGF
Imported by
BanditRLProof, BanditRLProof.Algorithms.CUCBChargedConditional
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.CUCB.ChargeData.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.chargedTriggerFactorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def chargedTriggerFactor (i : Fin m) (tilt : ℝ) (N : Fin m → ℕ) (z : Round A m) : ℝ
theorem
BanditRLProof.CUCB.ChargeData.chargedTriggerFactor_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.ChargeData.chargedTriggerFactor_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem chargedTriggerFactor_nonneg (i : Fin m) (tilt : ℝ) (N : Fin m → ℕ) (z : Round A m) : 0≤C.chargedTriggerFactor i tilt N z
theorem
BanditRLProof.CUCB.ChargeData.chargedTriggerFactor_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.ChargeData.chargedTriggerFactor_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem chargedTriggerFactor_le (i : Fin m) (tilt : ℝ) (N : Fin m → ℕ) (z : Round A m) : C.chargedTriggerFactor i tilt N z ≤ Real.exp (|tilt|+|(1-Real.exp (-tilt))*C.triggerLower i|)
theorem
BanditRLProof.CUCB.ChargeData.measurable_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.measurable_chargedTriggerFactorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_chargedTriggerFactor (i : Fin m) (tilt : ℝ) : Measurable (fun p : (Fin m → ℕ) × Round A m => C.chargedTriggerFactor i tilt p.1 p.2)
theorem
BanditRLProof.CUCB.ChargeData.integrable_chargedTriggerFactor_comp
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.integrable_chargedTriggerFactor_compReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrable_chargedTriggerFactor_comp {Ω : Type*} [MeasurableSpace Ω] (ν : Measure Ω) [IsProbabilityMeasure ν] (i : Fin m) (tilt : ℝ) (g : Ω → (Fin m → ℕ) × Round A m) (hg : Measurable g) : Integrable (fun ω => C.chargedTriggerFactor i tilt (g ω).1 (g ω).2) ν
theorem
BanditRLProof.CUCB.ChargeData.roundKernel_chargedTriggerFactor_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.ChargeData.roundKernel_chargedTriggerFactor_le_oneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem roundKernel_chargedTriggerFactor_le_one (oracle : Kernel (Input m) A) (environment : Kernel A (Feedback m)) [IsMarkovKernel oracle] [IsMarkovKernel environment] (i : Fin m) (htrigger : ∀a, i∈C.triggers a → C.triggerLower i≤(environment a (observedSet i)).toReal) (v : Input m) (N : Fin m → ℕ) (tilt : ℝ) (htilt : 0≤tilt) : (∫z, C.chargedTriggerFactor i tilt N z ∂roundKernel oracle environment v)≤1