Lean module · OFUL
BanditRLProof.OFULSelfNormalizedConfidence
# OFUL self-normalized confidence route This module starts the probabilistic OFUL route after the deterministic elliptical-potential theorem. It first formalizes the predictable-projection conditional exponential inequality used by the method of mixtures. The multivariate Gaussian mixture identity and final self-normalized event bound remain separate until they are compiled locally.
Module map
Imports
BanditRLProof.ConditionalExpectationReward, BanditRLProof.ConcentrationSubGaussian, BanditRLProof.OFULEllipticalPotentialFoundation
Imported by
BanditRLProof, BanditRLProof.OFULFiniteHorizonScoreGram, BanditRLProof.OFULGaussianMixture
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
ProbabilityTheory.HasCondSubgaussianMGF.predictable_mul_compensated_hasCondMGFUpperBoundAt
Compiled
Freeze a conditioning-measurable multiplier inside the conditional law and compensate its conditionally sub-Gaussian MGF. The explicit exponential-integrability premise is the regularity required by the local fixed-tilt composition API. A bounded-predictable-multiplier wrapper will discharge it for the OFUL feature process.
theorem HasCondSubgaussianMGF.predictable_mul_compensated_hasCondMGFUpperBoundAt {Omega : Type u} {m mOmega : MeasurableSpace Omega} [StandardBorelSpace Omega] {mu : Measure Omega} [IsProbabilityMeasure mu] {X A : Omega -> Real} {c : NNReal} (hm : m <= mOmega) (hX : HasCondSubgaussianMGF m hm X c mu) (hA : @Measurable Omega Real m inferInstance A) (hintegrable : forall s : Real, Integrable (fun omega => Real.exp (s * (A omega * X omega - (((c : NNReal) : Real) * A omega ^ 2 / 2)))) mu) : BanditRLProof.Concentration.HasCondMGFUpperBoundAt m hm (fun omega => A omega * X omega - (((c : NNReal) : Real) * A omega ^ 2 / 2)) 1 0 mu
theorem
ProbabilityTheory.HasCondSubgaussianMGF.integrable_exp_mul_predictable_mul_compensated_of_abs_le
Compiled
Uniform boundedness of a predictable multiplier discharges the exponential integrability contract of the compensated increment.
theorem HasCondSubgaussianMGF.integrable_exp_mul_predictable_mul_compensated_of_abs_le {Omega : Type u} {m mOmega : MeasurableSpace Omega} [StandardBorelSpace Omega] {mu : Measure Omega} [IsProbabilityMeasure mu] {X A : Omega -> Real} {c : NNReal} (hm : m <= mOmega) (hX : HasCondSubgaussianMGF m hm X c mu) (hA : @Measurable Omega Real m inferInstance A) (B : Real) (hB : 0 <= B) (hAbound : forall omega, |A omega| <= B) : forall s : Real, Integrable (fun omega => Real.exp (s * (A omega * X omega - (((c : NNReal) : Real) * A omega ^ 2 / 2)))) mu
theorem
ProbabilityTheory.HasCondSubgaussianMGF.predictable_mul_compensated_hasCondMGFUpperBoundAt_of_abs_le
Compiled
Bounded predictable multipliers satisfy the compensated conditional MGF contract without a caller-supplied exponential-integrability proof.
theorem HasCondSubgaussianMGF.predictable_mul_compensated_hasCondMGFUpperBoundAt_of_abs_le {Omega : Type u} {m mOmega : MeasurableSpace Omega} [StandardBorelSpace Omega] {mu : Measure Omega} [IsProbabilityMeasure mu] {X A : Omega -> Real} {c : NNReal} (hm : m <= mOmega) (hX : HasCondSubgaussianMGF m hm X c mu) (hA : @Measurable Omega Real m inferInstance A) (B : Real) (hB : 0 <= B) (hAbound : forall omega, |A omega| <= B) : BanditRLProof.Concentration.HasCondMGFUpperBoundAt m hm (fun omega => A omega * X omega - (((c : NNReal) : Real) * A omega ^ 2 / 2)) 1 0 mu
theorem
BanditRLProof.OFUL.fixedDirectionCompensatedScore_hasMGFUpperBoundAt
Compiled
Finite-horizon fixed-direction exponential-supermartingale endpoint for predictable vector features and conditionally sub-Gaussian scalar noise. This is the deterministic-horizon local form of Lemma 1 in Abbasi-Yadkori, Pal, and Szepesvari (2011). It is the input to the Gaussian mixture step, not yet the vector self-normalized determinant-ratio theorem.
theorem fixedDirectionCompensatedScore_hasMGFUpperBoundAt {Omega : Type v} {Feature : Type w} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (mu : Measure Omega) [IsProbabilityMeasure mu] (F : Filtration Nat mOmega) (feature : Nat -> Omega -> Feature -> Real) (noise : Nat -> Omega -> Real) (varianceProxy : Nat -> NNReal) (theta : Feature -> Real) (projectionBound : Nat -> Real) (hprojection : forall i, StronglyMeasurable[F i] (fun omega => dotProduct theta (feature i omega))) (hnoise : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => noise i omega)) (hprojectionBound_nonneg : forall i, 0 <= projectionBound i) (hprojectionBound : forall i omega, |dotProduct theta (feature i omega)| <= projectionBound i) (n : Nat) (hsubGaussian : forall i, i < n -> HasCondSubgaussianMGF (F i) (F.le i) (noise i) (varianceProxy i) mu) : Concentration.HasMGFUpperBoundAt (fun omega => (Finset.range (n + 1)).sum (fun t => match t with | 0 => 0 | i + 1 => dotProduct theta (feature i omega) * noise i omega - (((varianceProxy i : NNReal) : Real) * (dotProduct theta (feature i omega)) ^ 2 / 2))) 1 0 mu