Generated-history Bernstein trace-exp provider wrappers

This module upstreams the smallest stable generated-history Bernstein wrappers from the provider repository into HighDimProb.

It derives the finite-family Tropp trace-MGF wrapper and the downstream Bernstein trace-MGF and quadratic-form upper-tail contracts from the usual bounded centered self-adjoint Bernstein primitives along the generated natural history. Current-step exponential-mean self-adjointness is derived from the centered self-adjoint summand primitives, while strict positivity is derived from the self-adjoint current step and its matrix-exponential integrability. This module does not prove full Matrix Bernstein.

theorem HighDimProb.isSelfAdjointMatrix_matrixExpect_matrixExp_troppCurrentRandomStep_of_centeredSelfAdjoint {Omega : Type u_1} [mOmega : MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {m n : ℕ} (theta : ℝ) (X : Fin m → RandomMatrix Omega n n) (i : Fin m) (hCentered : CenteredSelfAdjointRandomMatrixFamily P X) : IsSelfAdjointMatrix (matrixExpect P fun (omega : Omega) => matrixExp (troppCurrentRandomStep theta X i omega))

The exponential mean of a Bernstein current step is self-adjoint under the usual centered self-adjoint summand primitives.

theorem HighDimProb.isStrictlyPositive_matrixExpect_matrixExp_troppCurrentRandomStep_of_centeredSelfAdjoint {Omega : Type u_1} [mOmega : MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {m n : ℕ} (theta R : ℝ) (X : Fin m → RandomMatrix Omega n n) (i : Fin m) (hCentered : CenteredSelfAdjointRandomMatrixFamily P X) (hBound : PointwiseOperatorNormBound X R) (hR : 0 ≤ R) : IsStrictlyPositive (matrixExpect P fun (omega : Omega) => matrixExp (troppCurrentRandomStep theta X i omega))

The exponential mean of a Bernstein current step is strictly positive under the usual bounded centered self-adjoint summand primitives.

structure HighDimProb.TraceExpTroppFrozenBoundInputs {Omega : Type u_1} [mOmega : MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {n : ℕ} (Z : RandomMatrix Omega n n) (K : Matrix (Fin n) (Fin n) ℝ) : Prop

Reusable finite-dimensional side-condition packet for the frozen-history Tropp trace-exp bound.

The packet contains no history-independence claim; consumers must supply either sigma-level independence or a justified history-sigma containment relation.

• stepAEMeasurable : AEMeasurable Z P
• frozenTraceIntegrable : HighDimProb.TraceExpFrozenTraceIntegrable✝ Z
• stepSelfAdjoint : RandomSelfAdjointMatrix P Z
• expIntegrable : IntegrableRandomMatrix P fun (omega : Omega) => matrixExp (Z omega)
• expMeanSelfAdjoint : IsSelfAdjointMatrix (matrixExpect P fun (omega : Omega) => matrixExp (Z omega))
• expMeanStrictlyPositive : IsStrictlyPositive (matrixExpect P fun (omega : Omega) => matrixExp (Z omega))
• comparisonSelfAdjoint : IsSelfAdjointMatrix K
• matrixMGFBound : MatrixLE (matrixExpect P fun (omega : Omega) => matrixExp (Z omega)) (matrixExp K)

theorem HighDimProb.TraceExpConditioning.troppStep_of_history_le {Omega : Type u_1} [mOmega : MeasurableSpace Omega] [Nonempty Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {n : ℕ} [StandardBorelSpace (Matrix (Fin n) (Fin n) ℝ)] {mHist : MeasurableSpace Omega} {H Z : RandomMatrix Omega n n} {K : Matrix (Fin n) (Fin n) ℝ} (hHistoryLe : mHist ≤ MeasurableSpace.comap H inferInstance) (hTropp : TraceExpTroppFrozenBoundInputs Z K) : troppMasterTraceMGFConditionalStep_statement mHist H Z K

Close the exact conditional-step contract when the chosen history sigma-algebra is contained in the sigma-algebra generated by the history matrix.

The contract's own IndepFun H Z P premise then supplies the sigma-level independence required by the frozen-bound conditioning proof. This theorem does not cover an arbitrary larger history sigma-algebra.

theorem HighDimProb.TraceExpConditioning.condExpStep_of_history_le {Omega : Type u_1} [mOmega : MeasurableSpace Omega] [Nonempty Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {n : ℕ} [StandardBorelSpace (Matrix (Fin n) (Fin n) ℝ)] {mHist : MeasurableSpace Omega} {H Z : RandomMatrix Omega n n} {K : Matrix (Fin n) (Fin n) ℝ} (hHistoryLe : mHist ≤ MeasurableSpace.comap H inferInstance) (hTropp : TraceExpTroppFrozenBoundInputs Z K) : condExp_traceExp_history_add_independent_step_statement mHist H Z K

Hardbone-name facade for troppStep_of_history_le.

@[reducible, inline]

abbrev HighDimProb.TraceExpConditioning.bernsteinInputs_of_primitives {Omega : Type u_1} [mOmega : MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {m n : ℕ} (theta R : ℝ) (X : Fin m → RandomMatrix Omega n n) (i : Fin m) (hCentered : CenteredSelfAdjointRandomMatrixFamily P X) (hIntX : ∀ (j : Fin m), IntegrableRandomMatrix P (X j)) (hIntSq : ∀ (j : Fin m), IntegrableRandomMatrix P (randomMatrixSquare (X j))) (hBound : PointwiseOperatorNormBound X R) (hR : 0 ≤ R) (hRange : |theta| * R < 3) : TraceExpTroppFrozenBoundInputs (troppCurrentRandomStep theta X i) (bernsteinSecondMomentComparisonFamily P X theta R i)

Build the frozen-bound current-step packet from the standard Bernstein single-summand primitives.

theorem HighDimProb.TraceExpConditioning.bernsteinStep_of_history_le {Omega : Type u_1} [mOmega : MeasurableSpace Omega] [Nonempty Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {m n : ℕ} [StandardBorelSpace (Matrix (Fin n) (Fin n) ℝ)] (theta R : ℝ) (X : Fin m → RandomMatrix Omega n n) (i : Fin m) (hCentered : CenteredSelfAdjointRandomMatrixFamily P X) (hIntX : ∀ (j : Fin m), IntegrableRandomMatrix P (X j)) (hIntSq : ∀ (j : Fin m), IntegrableRandomMatrix P (randomMatrixSquare (X j))) (hBound : PointwiseOperatorNormBound X R) (hR : 0 ≤ R) (hRange : |theta| * R < 3) {mHist : MeasurableSpace Omega} {H : RandomMatrix Omega n n} (hHistoryLe : mHist ≤ MeasurableSpace.comap H inferInstance) : troppMasterTraceMGFConditionalStep_statement mHist H (troppCurrentRandomStep theta X i) (bernsteinSecondMomentComparisonFamily P X theta R i)

Close a restricted-history conditional step directly from the standard Bernstein single-summand primitives.

The exact conditional-step statement still supplies its own history/current-step IndepFun premise. This theorem removes only the separate frozen-bound packet construction; it does not control an arbitrary larger history sigma-algebra.

theorem HighDimProb.troppMasterTraceMGFFiniteFamily_generatedHistory_of_bernsteinPrimitives {Omega : Type u_1} [mOmega : MeasurableSpace Omega] [Nonempty Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {m n : ℕ} [StandardBorelSpace (Matrix (Fin n) (Fin n) ℝ)] (theta R : ℝ) (X : Fin m → RandomMatrix Omega n n) (V : Matrix (Fin n) (Fin n) ℝ) (hCentered : CenteredSelfAdjointRandomMatrixFamily P X) (hIntX : ∀ (j : Fin m), IntegrableRandomMatrix P (X j)) (hIntSq : ∀ (j : Fin m), IntegrableRandomMatrix P (randomMatrixSquare (X j))) (hBound : PointwiseOperatorNormBound X R) (hR : 0 ≤ R) (hRange : |theta| * R < 3) (hIndep : ProbabilityTheory.iIndepFun X P) : troppMasterTraceMGFFiniteFamily_statement X (bernsteinSecondMomentComparisonFamily P X theta R) V theta R

Finite-family Tropp wrapper for Bernstein primitives along the generated natural history.

This derives the generated-history measurability, self-adjointness, sigma-finiteness, and bounded trace-exp integrability side conditions from the Bernstein primitive bundle itself. Current-step exponential-mean self-adjointness is derived from the centered self-adjoint summand primitives; strict positivity is derived from bounded self-adjoint current steps.

theorem HighDimProb.traceExpIntegrable_randomMatrixSum_of_operatorNormBounds_finiteMeasure {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure P] {m n : ℕ} (theta RX : ℝ) (X : Fin m → RandomMatrix Omega n n) (hX : ∀ (i : Fin m), IsRandomMatrix P (X i)) (hRX : 0 ≤ RX) (hXBound : ∀ (i : Fin m) (omega : Omega), operatorNorm (X i) omega ≤ RX) : IntegrableRealRandomVariable P (traceExpIntegrand (randomMatrixSum X) theta)

Finite-measure full-sum trace-exp integrability from uniform summand bounds.

This is the bounded finite-family bridge for the exact hTraceIntegrable-shaped consumer conclusion used downstream by the Tropp / Matrix Bernstein route.

theorem HighDimProb.matrixBernsteinTraceMGFWithBernsteinCoeff_generatedHistory_of_bernsteinPrimitives {Omega : Type u_1} [mOmega : MeasurableSpace Omega] [Nonempty Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {m n : ℕ} [StandardBorelSpace (Matrix (Fin n) (Fin n) ℝ)] (theta R : ℝ) (X : Fin m → RandomMatrix Omega n n) (hCentered : CenteredSelfAdjointRandomMatrixFamily P X) (hIndepSA : IndependentSelfAdjointRandomMatrices P X) (hIntX : ∀ (j : Fin m), IntegrableRandomMatrix P (X j)) (hIntSq : ∀ (j : Fin m), IntegrableRandomMatrix P (randomMatrixSquare (X j))) (hBound : PointwiseOperatorNormBound X R) (hR : 0 ≤ R) (hRange : |theta| * R < 3) : matrixBernsteinTraceMGFWithBernsteinCoeff_statement P X theta R

Matrix Bernstein trace-MGF wrapper from Bernstein primitives and the generated-history Tropp chain.

This consumes the generated-history finite-family wrapper above and the main HighDimProb Bernstein trace-MGF wrapper. The bounded finite-measure integrability side conditions for the per-summand matrix exponential and the full trace-exponential sum are derived from the pointwise operator-norm bound. Current-step exponential-mean self-adjointness is derived from the centered self-adjoint summand primitives, and strict positivity is derived internally.

theorem HighDimProb.matrixBernsteinQuadraticFormUpperTail_generatedHistory_of_bernsteinPrimitives {Omega : Type u_1} [mOmega : MeasurableSpace Omega] [Nonempty Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {m n : ℕ} [StandardBorelSpace (Matrix (Fin n) (Fin n) ℝ)] (theta t R : ℝ) (X : Fin m → RandomMatrix Omega n n) (hCentered : CenteredSelfAdjointRandomMatrixFamily P X) (hIndepSA : IndependentSelfAdjointRandomMatrices P X) (hIntX : ∀ (j : Fin m), IntegrableRandomMatrix P (X j)) (hIntSq : ∀ (j : Fin m), IntegrableRandomMatrix P (randomMatrixSquare (X j))) (hBound : PointwiseOperatorNormBound X R) (hR : 0 ≤ R) (hRange : |theta| * R < 3) (hTailMeas : AEMeasurable (fun (omega : Omega) => ENNReal.ofReal (traceExpIntegrand (randomMatrixSum X) theta omega)) P) (hTailSubset : quadraticFormUpperTailEvent (randomMatrixSum X) t ⊆ traceExpThresholdEvent (randomMatrixSum X) theta t) : P (quadraticFormUpperTailEvent (randomMatrixSum X) t) ≤ ENNReal.ofReal (Real.exp (-(theta * t))) * ENNReal.ofReal (traceMatrixExp (SMul.smul (bernsteinMGFCoeff theta R) (matrixVarianceProxy P X)))

Quadratic-form upper-tail Laplace bound from Bernstein primitives and the generated-history Tropp chain.

This composes the generated-history Bernstein trace-MGF wrapper with the Laplace contract. The tail-side measurability and event-subset bridge remain explicit, and current-step exponential-mean self-adjointness is derived from the centered self-adjoint summand primitives, with strict positivity derived internally.