Lean module · Foundations
BanditRLProof.Algorithms.CUCBRegretDecomposition
Actual charged-gap decomposition preserving the signed oracle-failure credit.
Module map
Imports
BanditRLProof.Algorithms.CUCBActualReward, BanditRLProof.Algorithms.CUCBSufficientSampling
Imported by
BanditRLProof, BanditRLProof.Algorithms.CUCBRegretTail, BanditRLProof.Algorithms.CUCBUnderCount
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.CUCB.SourceModel.underSampledGap
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.underSampledGapReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def underSampledGap (H : ℕ) (N : Fin m → ℕ) (a : A) : ℝ
def
BanditRLProof.CUCB.SourceModel.sufficientIndicator
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.sufficientIndicatorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def sufficientIndicator (H n : ℕ) (Y : ℕ → Round A m) : ℝ
theorem
BanditRLProof.CUCB.SourceModel.maxPositiveGap_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.SourceModel.maxPositiveGap_nonnegReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem maxPositiveGap_nonneg : 0≤maxPositiveGap S.score M.trueInput S.alpha
theorem
BanditRLProof.CUCB.SourceModel.underSampledGap_mem
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.underSampledGap_memReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem underSampledGap_mem (H : ℕ) (N : Fin m → ℕ) (a : A) : S.underSampledGap H N a∈Set.Icc 0 (maxPositiveGap S.score M.trueInput S.alpha)
theorem
BanditRLProof.CUCB.SourceModel.sufficientIndicator_mem
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.sufficientIndicator_memReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem sufficientIndicator_mem (H n : ℕ) (Y : ℕ → Round A m) : S.sufficientIndicator H n Y∈Set.Icc (0:ℝ) 1
theorem
BanditRLProof.CUCB.SourceModel.gap_decomposition
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.gap_decompositionReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem gap_decomposition (H n : ℕ) (Y : ℕ → Round A m) : S.gap (Y n).1≤S.underSampledGap H (S.chargeData.counters (fun t => (Y t).1) n) (Y n).1 + maxPositiveGap S.score M.trueInput S.alpha*S.sufficientIndicator H n Y + S.alpha*scoreOptimum S.score M.trueInput* (1-S.successIndicator (oracleInput (fun t => (Y t).2) n) (Y n))
theorem
BanditRLProof.CUCB.SourceModel.measurable_actual_underSampledGap
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.measurable_actual_underSampledGapReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_actual_underSampledGap (H n : ℕ) : Measurable (fun Y : ℕ → Round A m => S.underSampledGap H (S.chargeData.counters (fun t => (Y t).1) n) (Y n).1)
theorem
BanditRLProof.CUCB.SourceModel.measurableSet_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.measurableSet_sufficientSuccessfulChargeReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurableSet_sufficientSuccessfulCharge (H n : ℕ) : MeasurableSet (S.SufficientSuccessfulCharge H n)
theorem
BanditRLProof.CUCB.SourceModel.integrable_actual_underSampledGap
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.integrable_actual_underSampledGapReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrable_actual_underSampledGap (H n : ℕ) : Integrable (fun Y : ℕ → Round A m => S.underSampledGap H (S.chargeData.counters (fun t => (Y t).1) n) (Y n).1) (cucbTrajectory S.oracle M.environment)
theorem
BanditRLProof.CUCB.SourceModel.integrable_sufficientIndicator
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.integrable_sufficientIndicatorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrable_sufficientIndicator (H n : ℕ) : Integrable (S.sufficientIndicator H n) (cucbTrajectory S.oracle M.environment)
theorem
BanditRLProof.CUCB.SourceModel.expected_gap_decomposition
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.expected_gap_decompositionReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem expected_gap_decomposition (H n : ℕ) : (∫Y : ℕ → Round A m, S.gap (Y n).1 ∂cucbTrajectory S.oracle M.environment) ≤ (∫Y : ℕ → Round A m, S.underSampledGap H (S.chargeData.counters (fun t => (Y t).1) n) (Y n).1 ∂cucbTrajectory S.oracle M.environment) + maxPositiveGap S.score M.trueInput S.alpha* (∫Y, S.sufficientIndicator H n Y ∂cucbTrajectory S.oracle M.environment) + S.alpha*scoreOptimum S.score M.trueInput*(1-S.beta)
theorem
BanditRLProof.CUCB.SourceModel.approximationRegret_le_underSampled_add_sufficient
Compiled
Exact cancellation against the negative credit in the original signed approximation regret. The under-count term is still the actual random weight.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.SourceModel.approximationRegret_le_underSampled_add_sufficientReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem approximationRegret_le_underSampled_add_sufficient (H : ℕ) : S.approximationRegret H ≤ (∑n∈Finset.range H, ∫Y : ℕ → Round A m, S.underSampledGap H (S.chargeData.counters (fun t => (Y t).1) n) (Y n).1 ∂cucbTrajectory S.oracle M.environment) + maxPositiveGap S.score M.trueInput S.alpha* ∑n∈Finset.range H, ∫Y, S.sufficientIndicator H n Y ∂cucbTrajectory S.oracle M.environment