Tail-event discharge for natural-state provider wrappers

This module proves a thin wrapper around the existing natural-state S16 consumer by discharging only the explicit tail-event subset premise through the already proved provider-assumption tail-subset-discharge wrapper.

It does not prove conditioning, trace-MGF bounds, variance-proxy normalization, theta optimization, or Matrix Bernstein.

theorem HighDimProb.matrixBernsteinQuadraticFormUpperTail_of_naturalStateProviderAssumptions_tailSubsetDischarged_of_randomSelfAdjoint {Omega : Type u_1} [mOmega : MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {m n : ℕ} (X : Fin m → RandomMatrix Omega n n) (K : Fin m → Matrix (Fin n) (Fin n) ℝ) (V : Matrix (Fin n) (Fin n) ℝ) (theta R t RH RZ RK RX : ℝ) (mHist : Fin m → MeasurableSpace Omega) (hChain : troppConditionalStep_of_iIndepFun_statement theta X K mHist) (hSuffix : ∀ (i j : Fin m), ↑i.succ ≤ ↑j → ∀ (r c : Fin n), Measurable fun (omega : Omega) => X j omega r c) (hConditionalExpectation : ∀ (i : Fin m), condExp_traceExp_history_add_independent_step_statement (mHist i) (troppStateHistory theta X K i) (troppCurrentRandomStep theta X i) (K i)) (hHistorySub : ∀ (i : Fin m), mHist i ≤ mOmega) (hHistoryRandom : ∀ (i : Fin m), IsRandomMatrix P (troppStateHistory theta X K i)) (hStepRandom : ∀ (i : Fin m), IsRandomMatrix P (troppCurrentRandomStep theta X i)) (hHistorySelfAdjoint : ∀ (i : Fin m) (omega : Omega), IsSelfAdjointMatrix (troppStateHistory theta X K i omega)) (hStepSelfAdjoint : ∀ (i : Fin m), RandomSelfAdjointMatrix P (troppCurrentRandomStep theta X i)) (hFiniteMeasure : MeasureTheory.IsFiniteMeasure P) (hHistoryOperatorNormBound : ∀ (i : Fin m) (omega : Omega), operatorNorm (troppStateHistory theta X K i) omega ≤ RH) (hStepOperatorNormBound : ∀ (i : Fin m) (omega : Omega), operatorNorm (troppCurrentRandomStep theta X i) omega ≤ RZ) (hKOperatorNormBound : ∀ (i : Fin m) (omega : Omega), operatorNorm (fun (x : Omega) => K i) omega ≤ RK) (hSummandOperatorNormBound : ∀ (i : Fin m) (omega : Omega), operatorNorm (X i) omega ≤ RX) (hSummandRadiusNonneg : 0 ≤ RX) (hExpMeanSelfAdjoint : ∀ (i : Fin m), IsSelfAdjointMatrix (matrixExpect P fun (omega : Omega) => matrixExp (troppCurrentRandomStep theta X i omega))) (hExpMeanStrictlyPositive : ∀ (i : Fin m), IsStrictlyPositive (matrixExpect P fun (omega : Omega) => matrixExp (troppCurrentRandomStep theta X i omega))) (hSigmaFiniteHistory : ∀ (i : Fin m), MeasureTheory.SigmaFinite (P.trim ⋯)) (hRandomMatrix : ∀ (i : Fin m), IsRandomMatrix P (X i)) (hSelfAdjoint : ∀ (i : Fin m), RandomSelfAdjointMatrix P (X i)) (hIndependent : ProbabilityTheory.iIndepFun X P) (hTraceIntegrable : IntegrableRealRandomVariable P (traceExpIntegrand (randomMatrixSum X) theta)) (hComparisonSelfAdjoint : ∀ (i : Fin m), IsSelfAdjointMatrix (K i)) (hVarianceProxySelfAdjoint : IsSelfAdjointMatrix V) (hRadiusNonneg : 0 ≤ R) (hThetaRange : |theta| * R < 3) (hMGFComparison : ∀ (i : Fin m), MatrixLE (matrixExpect P fun (omega : Omega) => matrixExp (SMul.smul theta (X i omega))) (matrixExp (K i))) (hVarianceProxyNormalization : ∑ i : Fin m, K i = SMul.smul (bernsteinMGFCoeff theta R) V) (hTailAEMeasurable : AEMeasurable (fun (omega : Omega) => ENNReal.ofReal (traceExpIntegrand (randomMatrixSum X) theta omega)) P) (hTheta : 0 ≤ theta) : P (quadraticFormUpperTailEvent (randomMatrixSum X) t) ≤ ENNReal.ofReal (Real.exp (-(theta * t))) * ENNReal.ofReal (traceMatrixExp (SMul.smul (bernsteinMGFCoeff theta R) V))

Tail-subset-discharge wrapper for the natural-state provider S16 route.

This keeps the conditioning, trace-MGF, integrability, comparison, and variance-proxy assumptions explicit. It removes only the final quadraticFormUpperTailEvent ⊆ traceExpThresholdEvent premise by forwarding to the existing provider-assumption tail-subset-discharge theorem.