Lean module · Foundations
BanditRLProof.Algorithms.CUCBObservationMGF
Bounded-outcome MGF produced from the primitive uncensored marginal law. The current random observation mask remains inside the exponent.
Module map
Imports
BanditRLProof.Algorithms.CUCBTrajectory
Imported by
BanditRLProof, BanditRLProof.Algorithms.CUCBRoundMGF, BanditRLProof.Algorithms.CUCBTriggerMGF
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.CUCB.marginalMean
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.marginalMeanReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def marginalMean (D : Measure UnitOutcome) : ℝ
def
BanditRLProof.CUCB.centeredFactor
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.centeredFactorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def centeredFactor (D : Measure UnitOutcome) (tilt : ℝ) (x : UnitOutcome) : ℝ
theorem
BanditRLProof.CUCB.measurable_centeredFactor
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.measurable_centeredFactorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_centeredFactor (D : Measure UnitOutcome) (tilt : ℝ) : Measurable (centeredFactor D tilt)
theorem
BanditRLProof.CUCB.marginal_subgaussian
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.marginal_subgaussianReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem marginal_subgaussian (D : Measure UnitOutcome) [IsProbabilityMeasure D] : HasSubgaussianMGF (fun x : UnitOutcome => (x:ℝ)-marginalMean D) (1/4:ℝ≥0) D
theorem
BanditRLProof.CUCB.integrable_centeredFactor
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.integrable_centeredFactorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrable_centeredFactor (D : Measure UnitOutcome) [IsProbabilityMeasure D] (tilt : ℝ) : Integrable (centeredFactor D tilt) D
theorem
BanditRLProof.CUCB.integral_centeredFactor_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.integral_centeredFactor_le_oneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_centeredFactor_le_one (D : Measure UnitOutcome) [IsProbabilityMeasure D] (tilt : ℝ) : (∫ x, centeredFactor D tilt x ∂D)≤1
def
BanditRLProof.CUCB.observedSet
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.observedSetReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def observedSet {m : ℕ} (i : Fin m) : Set (Feedback m)
theorem
BanditRLProof.CUCB.measurableSet_observedSet
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.measurableSet_observedSetReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurableSet_observedSet {m : ℕ} (i : Fin m) : MeasurableSet (observedSet i)
def
BanditRLProof.CUCB.ObservationCompatible
Compiled
Primitive equality of measures, expressing the unchanged marginal law upon observation. It is not a concentration or MGF assumption.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.CUCB.ObservationCompatibleReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def ObservationCompatible {m : ℕ} (ν : Measure (Feedback m)) (D : Measure UnitOutcome) (i : Fin m) : Prop
theorem
BanditRLProof.CUCB.observed_centeredFactor_integrable
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.observed_centeredFactor_integrableReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem observed_centeredFactor_integrable {m : ℕ} (ν : Measure (Feedback m)) [IsProbabilityMeasure ν] (D : Measure UnitOutcome) [IsProbabilityMeasure D] (i : Fin m) (h : ObservationCompatible ν D i) (tilt : ℝ) : IntegrableOn (fun z => centeredFactor D tilt (z.2.1 i)) (observedSet i) ν
theorem
BanditRLProof.CUCB.observed_centeredFactor_integral
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.observed_centeredFactor_integralReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem observed_centeredFactor_integral {m : ℕ} (ν : Measure (Feedback m)) [IsProbabilityMeasure ν] (D : Measure UnitOutcome) [IsProbabilityMeasure D] (i : Fin m) (h : ObservationCompatible ν D i) (tilt : ℝ) : (∫ z in observedSet i, centeredFactor D tilt (z.2.1 i) ∂ν) = (ν (observedSet i)).toReal * ∫ x, centeredFactor D tilt x ∂D
def
BanditRLProof.CUCB.observedFactor
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.observedFactorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
noncomputable def observedFactor {m : ℕ} (D : Measure UnitOutcome) (i : Fin m) (tilt : ℝ) (z : Feedback m) : ℝ
theorem
BanditRLProof.CUCB.observedFactor_eq_piecewise
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.observedFactor_eq_piecewiseReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem observedFactor_eq_piecewise {m : ℕ} (D : Measure UnitOutcome) (i : Fin m) (tilt : ℝ) [DecidablePred (· ∈ observedSet i)] : observedFactor D i tilt = (observedSet i).piecewise (fun z => centeredFactor D tilt (z.2.1 i)) (fun _ => 1)
theorem
BanditRLProof.CUCB.observedFactor_eq_exp
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.observedFactor_eq_expReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem observedFactor_eq_exp {m : ℕ} (D : Measure UnitOutcome) (i : Fin m) (tilt : ℝ) (z : Feedback m) : observedFactor D i tilt z = Real.exp (tilt * (if z.1 i then (z.2.1 i:ℝ)-marginalMean D else 0) - tilt^2/8 * (if z.1 i then 1 else 0))
theorem
BanditRLProof.CUCB.integrable_observedFactor
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.integrable_observedFactorReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrable_observedFactor {m : ℕ} (ν : Measure (Feedback m)) [IsProbabilityMeasure ν] (D : Measure UnitOutcome) [IsProbabilityMeasure D] (i : Fin m) (h : ObservationCompatible ν D i) (tilt : ℝ) : Integrable (observedFactor D i tilt) ν
theorem
BanditRLProof.CUCB.integral_observedFactor_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.integral_observedFactor_le_oneReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_observedFactor_le_one {m : ℕ} (ν : Measure (Feedback m)) [IsProbabilityMeasure ν] (D : Measure UnitOutcome) [IsProbabilityMeasure D] (i : Fin m) (h : ObservationCompatible ν D i) (tilt : ℝ) : (∫ z, observedFactor D i tilt z ∂ν)≤1