Lean module · Foundations
BanditRLProof.Algorithms.CUCBSufficientSampling
The actual successful-oracle bad-action event after the normalized charged counter crosses its source threshold. The nice-event and trigger-tail constants are retained, including the probability-one observation branch.
Module map
Imports
BanditRLProof.Algorithms.CUCBThresholdTail, BanditRLProof.Algorithms.CUCBImpossibleCase
Imported by
BanditRLProof, BanditRLProof.Algorithms.CUCBRegretDecomposition
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.CUCB.SourceModel.SufficientSuccessfulCharge
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.SufficientSuccessfulChargeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def SufficientSuccessfulCharge (H n : ℕ) : Set (ℕ → Round A m)
theorem
BanditRLProof.CUCB.SourceModel.sufficient_successful_charge_subset
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.sufficient_successful_charge_subsetReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sufficient_successful_charge_subset (H n : ℕ) : S.SufficientSuccessfulCharge H n ⊆ (NiceEvent (fun i => (M.trueInput i:ℝ)) n)ᶜ ∪ ⋃i, S.TriggerShortfall H n i
theorem
BanditRLProof.CUCB.SourceModel.sufficient_successful_charge_probability
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.sufficient_successful_charge_probabilityReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sufficient_successful_charge_probability (H n : ℕ) (hH : n+1≤H) : (cucbTrajectory S.oracle M.environment) (S.SufficientSuccessfulCharge H n) ≤ ENNReal.ofReal (3*(m:ℝ)/((n:ℝ)+1)^2)
theorem
BanditRLProof.CUCB.SourceModel.sufficient_successful_charge_probability_of_all_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.SourceModel.sufficient_successful_charge_probability_of_all_oneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sufficient_successful_charge_probability_of_all_one (H n : ℕ) (hH : n+1≤H) (hp : ∀i, M.minTrigger i=1) : (cucbTrajectory S.oracle M.environment) (S.SufficientSuccessfulCharge H n) ≤ ENNReal.ofReal (2*(m:ℝ)/((n:ℝ)+1)^2)
theorem
BanditRLProof.CUCB.SourceModel.sufficient_successful_charge_probability_source
Compiled
The source indicator uses the minimum of actual trigger probabilities, not an independent parameter. Nonempty base arms follow from the feasible family.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.SourceModel.sufficient_successful_charge_probability_sourceReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sufficient_successful_charge_probability_source (H n : ℕ) (hH : n+1≤H) : (cucbTrajectory S.oracle M.environment) (S.SufficientSuccessfulCharge H n) ≤ ENNReal.ofReal ((2+(if M.globalMinTrigger<1 then 1 else 0))*(m:ℝ)/((n:ℝ)+1)^2)