Lean module · Foundations
BanditRLProof.Algorithms.CUCBOracleSuccess
Per-input approximate oracle success lifted to the actual initial and conditional successor laws, with the actual history-dependent oracle input.
Module map
Imports
BanditRLProof.Algorithms.CUCBOracleMeasurable
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.CUCB.SourceModel.successIndicator
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.successIndicatorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def successIndicator (v : Input m) (z : Round A m) : ℝ
theorem
BanditRLProof.CUCB.SourceModel.measurable_successIndicator
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_successIndicatorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_successIndicator : Measurable (fun p : Input m × Round A m => S.successIndicator p.1 p.2)
theorem
BanditRLProof.CUCB.SourceModel.successIndicator_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.successIndicator_memReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem successIndicator_mem (v : Input m) (z : Round A m) : S.successIndicator v z∈Set.Icc (0:ℝ) 1
theorem
BanditRLProof.CUCB.SourceModel.integrable_successIndicator_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.SourceModel.integrable_successIndicator_compReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrable_successIndicator_comp {Ω : Type*} [MeasurableSpace Ω] (ν : Measure Ω) [IsProbabilityMeasure ν] (g : Ω → Input m × Round A m) (hg : Measurable g) : Integrable (fun ω => S.successIndicator (g ω).1 (g ω).2) ν
theorem
BanditRLProof.CUCB.SourceModel.roundKernel_success_lower
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.roundKernel_success_lowerReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem roundKernel_success_lower (v : Input m) : S.beta≤∫z, S.successIndicator v z ∂roundKernel S.oracle M.environment v
theorem
BanditRLProof.CUCB.SourceModel.condExp_oracle_success
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.condExp_oracle_successReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem condExp_oracle_success (n : ℕ) : (fun _ => S.beta) ≤ᵐ[cucbTrajectory S.oracle M.environment] (cucbTrajectory S.oracle M.environment)[fun Y => S.successIndicator (oracleInput (fun t => (Y t).2) (n+1)) (Y (n+1)) | MeasurableSpace.comap (Preorder.frestrictLe n) inferInstance]
theorem
BanditRLProof.CUCB.SourceModel.initial_oracle_success
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.initial_oracle_successReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem initial_oracle_success : S.beta≤∫Y, S.successIndicator (oracleInput (fun t => (Y t).2) 0) (Y 0) ∂cucbTrajectory S.oracle M.environment
theorem
BanditRLProof.CUCB.SourceModel.expected_oracle_success
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_oracle_successReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem expected_oracle_success (n : ℕ) : S.beta≤∫Y, S.successIndicator (oracleInput (fun t => (Y t).2) n) (Y n) ∂cucbTrajectory S.oracle M.environment
theorem
BanditRLProof.CUCB.SourceModel.oracle_failure_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.oracle_failure_probabilityReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem oracle_failure_probability (n : ℕ) : (cucbTrajectory S.oracle M.environment) {Y | (oracleInput (fun t => (Y t).2) n,(Y n).1)∈S.oracleSuccess}ᶜ ≤ ENNReal.ofReal (1-S.beta)