Conditioning trace-exp provider wrapper

This module proves a thin wrapper from strengthened sigma-independence and an explicit frozen trace bound to the existing conditional trace-exponential hardbone statement.

It keeps the weak hardbone statement unchanged. The pair-law trace-exp integrability premise is left explicit on purpose rather than deriving it from the ambient hardbone hTraceInt; that derivation remains a separate proof-engineering task.

theorem HighDimProb.condExp_traceExp_history_add_independent_step_of_indep_sigma {Omega : Type u_1} [mOmega : MeasurableSpace Omega] [Nonempty Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure P] {n : ℕ} [StandardBorelSpace (Matrix (Fin n) (Fin n) ℝ)] (mHist : MeasurableSpace Omega) (H Z : RandomMatrix Omega n n) (K : Matrix (Fin n) (Fin n) ℝ) (hHistStepIndep : ProbabilityTheory.Indep mHist (MeasurableSpace.comap Z inferInstance) P) (hPairInt : MeasureTheory.Integrable (fun (p : Matrix (Fin n) (Fin n) ℝ × Matrix (Fin n) (Fin n) ℝ) => traceMatrixExp (p.1 + p.2)) (MeasureTheory.Measure.map (fun (omega : Omega) => (H omega, Z omega)) P)) (hFrozenBound : ∀ (A : Matrix (Fin n) (Fin n) ℝ), ∫ (B : Matrix (Fin n) (Fin n) ℝ), traceMatrixExp (A + B) ∂MeasureTheory.Measure.map Z P ≤ traceMatrixExp (A + K)) : condExp_traceExp_history_add_independent_step_statement mHist H Z K

Strengthened sigma-independence wrapper for the conditional trace-exp hardbone step.

This theorem discharges the existing weak statement condExp_traceExp_history_add_independent_step_statement from a stronger history/current-step sigma-independence premise together with an explicit pair-law integrability witness and a frozen-history trace bound.