BanditRLProof.OFULSelfNormalizedMarkov

The common conditional sub-Gaussian variance proxy `R²`.

def constantSquaredVarianceProxy (R : Real) : Nat -> NNReal

The unweighted finite-horizon feature Gram `sum_{i<n} x_i x_i^T`.

noncomputable def finiteHorizonFeatureGram (feature : Nat -> Omega -> Feature -> Real) (n : Nat) (omega : Omega) : Matrix Feature Feature Real

At common proxy `R²`, the variance Gram is `R²` times the unweighted feature Gram.

theorem finiteHorizonVarianceGram_constantSquared_eq_smul_featureGram [Fintype Feature] (R : Real) (hR : 0 < R) (feature : Nat -> Omega -> Feature -> Real) (n : Nat) (omega : Omega) : finiteHorizonVarianceGram feature (constantSquaredVarianceProxy R) n omega = R ^ 2 • finiteHorizonFeatureGram feature n omega

The unweighted finite-horizon feature Gram is positive semidefinite.

theorem finiteHorizonFeatureGram_posSemidef [Fintype Feature] (feature : Nat -> Omega -> Feature -> Real) (n : Nat) (omega : Omega) : (finiteHorizonFeatureGram feature n omega).PosSemidef

Positive scalar-square rescaling preserves positive definiteness.

theorem sq_smul_posDef [Fintype Feature] [DecidableEq Feature] (R : Real) (hR : 0 < R) (V0 : Matrix Feature Feature Real) (hV0 : V0.PosDef) : (R ^ 2 • V0).PosDef

A common nonzero scalar factor cancels from a determinant ratio.

theorem det_sq_smul_div_det_sq_smul [Fintype Feature] [DecidableEq Feature] (R : Real) (hR : 0 < R) (A B : Matrix Feature Feature Real) : Matrix.det (R ^ 2 • A) / Matrix.det (R ^ 2 • B) = Matrix.det A / Matrix.det B

The inverse quadratic form of a matrix scaled by `R²` is the original quadratic form divided by `R²`.

theorem dotProduct_sq_smul_inv_mulVec [Fintype Feature] [DecidableEq Feature] (R : Real) (hR : 0 < R) (A : Matrix Feature Feature Real) (hA : A.PosDef) (score : EuclideanSpace Real Feature) : score ⬝ᵥ (R ^ 2 • A)⁻¹.mulVec score = (score ⬝ᵥ A⁻¹.mulVec score) / R ^ 2

Markov's inequality for the evaluated finite-horizon Gaussian-mixture surface, with an arbitrary nonzero finite `ENNReal` confidence level.

theorem measure_inv_le_finiteHorizonDetRatioInvGramExponential_le [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (mu : Measure Omega) [IsProbabilityMeasure mu] (V0 : Matrix Feature Feature Real) (hV0 : V0.PosDef) (F : Filtration Nat mOmega) (feature : Nat -> Omega -> Feature -> Real) (noise : Nat -> Omega -> Real) (varianceProxy : Nat -> NNReal) (projectionBound : EuclideanSpace Real Feature -> Nat -> Real) (hfeature : forall i j, StronglyMeasurable[F i] (fun omega => feature i omega j)) (hnoise : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => noise i omega)) (hprojectionBound_nonneg : forall theta i, 0 <= projectionBound theta i) (hprojectionBound : forall theta i omega, |dotProduct (WithLp.ofLp theta) (feature i omega)| <= projectionBound theta i) (n : Nat) (hsubGaussian : forall i, i < n -> HasCondSubgaussianMGF (F i) (F.le i) (noise i) (varianceProxy i) mu) (delta : ENNReal) (hdelta_zero : delta ≠ 0) (hdelta_top : delta ≠ ∞) : mu {omega | delta⁻¹ <= finiteHorizonDetRatioInvGramExponential V0 feature noise varianceProxy n omega} <= delta

Real-confidence specialization of the evaluated-mixture Markov bound.

theorem measure_invOfReal_le_finiteHorizonDetRatioInvGramExponential_le [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (mu : Measure Omega) [IsProbabilityMeasure mu] (V0 : Matrix Feature Feature Real) (hV0 : V0.PosDef) (F : Filtration Nat mOmega) (feature : Nat -> Omega -> Feature -> Real) (noise : Nat -> Omega -> Real) (varianceProxy : Nat -> NNReal) (projectionBound : EuclideanSpace Real Feature -> Nat -> Real) (hfeature : forall i j, StronglyMeasurable[F i] (fun omega => feature i omega j)) (hnoise : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => noise i omega)) (hprojectionBound_nonneg : forall theta i, 0 <= projectionBound theta i) (hprojectionBound : forall theta i omega, |dotProduct (WithLp.ofLp theta) (feature i omega)| <= projectionBound theta i) (n : Nat) (hsubGaussian : forall i, i < n -> HasCondSubgaussianMGF (F i) (F.le i) (noise i) (varianceProxy i) mu) (delta : Real) (hdelta : 0 < delta) : mu {omega | (ENNReal.ofReal delta)⁻¹ <= finiteHorizonDetRatioInvGramExponential V0 feature noise varianceProxy n omega} <= ENNReal.ofReal delta

The inverse-Gram/log-determinant bad-event inequality implies the evaluated Gaussian-mixture Markov threshold, pointwise.

theorem invOfReal_le_gaussianDetRatioExponential_of_invGramQuadratic_gt [Fintype Feature] [DecidableEq Feature] (V0 G : Matrix Feature Feature Real) (hV0 : V0.PosDef) (hG : G.PosSemidef) (score : EuclideanSpace Real Feature) (delta : Real) (hdelta : 0 < delta) (hbad : score ⬝ᵥ (V0 + G)⁻¹.mulVec score > 2 * Real.log (Real.sqrt (Matrix.det (V0 + G) / Matrix.det V0) / delta)) : (ENNReal.ofReal delta)⁻¹ <= ENNReal.ofReal (Real.sqrt (Matrix.det V0 / Matrix.det (V0 + G)) * Real.exp (score ⬝ᵥ (V0 + G)⁻¹.mulVec score / 2))

Finite-horizon inverse-Gram/log-determinant bad-event probability bound for the variance-weighted Gram produced by the conditional-MGF route.

theorem measure_finiteHorizon_invGramQuadratic_gt_two_log_detRatio_div_le [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (mu : Measure Omega) [IsProbabilityMeasure mu] (V0 : Matrix Feature Feature Real) (hV0 : V0.PosDef) (F : Filtration Nat mOmega) (feature : Nat -> Omega -> Feature -> Real) (noise : Nat -> Omega -> Real) (varianceProxy : Nat -> NNReal) (projectionBound : EuclideanSpace Real Feature -> Nat -> Real) (hfeature : forall i j, StronglyMeasurable[F i] (fun omega => feature i omega j)) (hnoise : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => noise i omega)) (hprojectionBound_nonneg : forall theta i, 0 <= projectionBound theta i) (hprojectionBound : forall theta i omega, |dotProduct (WithLp.ofLp theta) (feature i omega)| <= projectionBound theta i) (n : Nat) (hsubGaussian : forall i, i < n -> HasCondSubgaussianMGF (F i) (F.le i) (noise i) (varianceProxy i) mu) (delta : Real) (hdelta : 0 < delta) : mu {omega | (finiteHorizonNoiseScore feature noise n omega) ⬝ᵥ (V0 + finiteHorizonVarianceGram feature varianceProxy n omega)⁻¹.mulVec (finiteHorizonNoiseScore feature noise n omega) > 2 * Real.log (Real.sqrt (Matrix.det (V0 + finiteHorizonVarianceGram feature varianceProxy n omega) / Matrix.det V0) / delta)} <= ENNReal.ofReal delta

Finite-horizon self-normalized tail bound with the conventional common conditional sub-Gaussian scale `R`. The matrix in the reported norm is the unweighted feature Gram, while the confidence radius carries the factor `R²`.

theorem measure_finiteHorizon_selfNormalizedQuadratic_gt_two_mul_sq_mul_log_detRatio_div_le [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] [Fintype Feature] [DecidableEq Feature] [Nonempty Feature] (mu : Measure Omega) [IsProbabilityMeasure mu] (V0 : Matrix Feature Feature Real) (hV0 : V0.PosDef) (F : Filtration Nat mOmega) (feature : Nat -> Omega -> Feature -> Real) (noise : Nat -> Omega -> Real) (R : Real) (hR : 0 < R) (projectionBound : EuclideanSpace Real Feature -> Nat -> Real) (hfeature : forall i j, StronglyMeasurable[F i] (fun omega => feature i omega j)) (hnoise : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => noise i omega)) (hprojectionBound_nonneg : forall theta i, 0 <= projectionBound theta i) (hprojectionBound : forall theta i omega, |dotProduct (WithLp.ofLp theta) (feature i omega)| <= projectionBound theta i) (n : Nat) (hsubGaussian : forall i, i < n -> HasCondSubgaussianMGF (F i) (F.le i) (noise i) (constantSquaredVarianceProxy R i) mu) (delta : Real) (hdelta : 0 < delta) : mu {omega | (finiteHorizonNoiseScore feature noise n omega) ⬝ᵥ (V0 + finiteHorizonFeatureGram feature n omega)⁻¹.mulVec (finiteHorizonNoiseScore feature noise n omega) > 2 * R ^ 2 * Real.log (Real.sqrt (Matrix.det (V0 + finiteHorizonFeatureGram feature n omega) / Matrix.det V0) / delta)} <= ENNReal.ofReal delta