BanditRLProof.OFULSelfNormalizedConfidence

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

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

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

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