Lean module · Foundations
BanditRLProof.Algorithms.CUCBDeterministicTrigger
Deterministic triggering on the actual CUCB law, including all horizons. No claim is made about feedback records in null sets.
Module map
Imports
BanditRLProof.Algorithms.CUCBChargedConcentration
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.cucbTrajectory_ae_round_property
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.cucbTrajectory_ae_round_propertyReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem cucbTrajectory_ae_round_property (oracle : Kernel (Input m) A) (environment : Kernel A (Feedback m)) [IsMarkovKernel oracle] [IsMarkovKernel environment] (s : Set (Round A m)) (hs : MeasurableSet s) (hround : ∀v, ∀ᵐ z ∂roundKernel oracle environment v, z∈s) : ∀ᵐ Y ∂cucbTrajectory oracle environment, ∀n, Y n∈s
def
BanditRLProof.CUCB.ChargeData.triggerSupport
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.triggerSupportReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def triggerSupport (i : Fin m) : Set (Round A m)
theorem
BanditRLProof.CUCB.ChargeData.measurableSet_triggerSupport
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.measurableSet_triggerSupportReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurableSet_triggerSupport (i : Fin m) : MeasurableSet (C.triggerSupport i)
theorem
BanditRLProof.CUCB.ChargeData.environment_ae_observed_of_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.environment_ae_observed_of_oneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem environment_ae_observed_of_one (environment : Kernel A (Feedback m)) [IsMarkovKernel environment] (i : Fin m) (htrigger : ∀a, i∈C.triggers a → C.triggerLower i≤(environment a (observedSet i)).toReal) (hp : C.triggerLower i=1) (a : A) (ha : i∈C.triggers a) : ∀ᵐ z ∂environment a, z.1 i=true
theorem
BanditRLProof.CUCB.ChargeData.roundKernel_ae_triggerSupport_of_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_ae_triggerSupport_of_oneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem roundKernel_ae_triggerSupport_of_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) (hp : C.triggerLower i=1) (v : Input m) : ∀ᵐ z ∂roundKernel oracle environment v, z∈C.triggerSupport i
theorem
BanditRLProof.CUCB.ChargeData.counters_le_observations_ae_of_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.counters_le_observations_ae_of_oneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem counters_le_observations_ae_of_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) (hp : C.triggerLower i=1) : ∀ᵐ Y ∂cucbTrajectory oracle environment, ∀n, C.counters (fun t => (Y t).1) n i≤observationCount (fun t => (Y t).2) n i