CommonEventAggregation

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Countable aggregation of weak-Orlicz bounds onto one common event

That is the content of Algsuperdiff.Section3.Probability.IsCommonEventTwoTermBigOWith, and this module is the first A on that carrier:

• amplitude monotonicity, at fixed envelopes and fixed common event;
• absorption of a nonnegative deterministic shift into the first amplitude, with no side condition;
• transfer along an almost-sure pointwise domination by members of an already bounded family, the step by which an arbitrary --- possibly uncountable --- index type inherits a bound obtained for a countable one, the index quantifier staying inside the event;
• the countable aggregation itself, at the amplitudes C_triangle(sigma) * sum a.

The two Orlicz terms stay separate and one-sided throughout: the two lanes are never merged. Positivity of the individual amplitudes is never a hypothesis; it is carried by each two-term datum. The passage from the one-sided IsBigOWith of the weak-Orlicz notation to the two-sided IsBigO required by the envelope engine is done by replacing each lane by its positive part, and its one-sided half is consumed, not re-derived: it is the public isBigOWith_max_zero of Provider/Tail/TailSqrt.lean.

Nothing in this module refers to Section 3.5. Typing data: the abstract carriers Omega, mu, Psi1, Psi2, the index types, the families and the amplitudes.

theorem Algsuperdiff.Section3.Provider.Homogenization.isBigO_posPart_of_isBigOWith {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {Psi : ℝ → ℝ} {Y : Omega → ℝ} {A : ℝ} (hA : 0 < A) (hY : HCPolySupport.IndependentSums.IsBigOWith mu Psi Y A) : HCPolySupport.IndependentSums.IsBigO mu Psi (fun (omega : Omega) => max (Y omega) 0) A

The one-sided weak-Orlicz relation transfers to the positive part as a two-sided relation, at the same amplitude.

The weak-Orlicz notation of the ABK26 Appendix controls only the upper tail, while a countable envelope has to be built from absolute values. Replacing a lane by its positive part costs nothing: the two upper-tail events agree above every positive threshold, and the positive part still dominates the lane.

theorem Algsuperdiff.Section3.Provider.Homogenization.isCommonEventTwoTermBigOWith_mono_scale {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {I : Type u_2} [MeasureTheory.IsFiniteMeasure mu] {Psi1 Psi2 : ℝ → ℝ} {X : I → Omega → ℝ} {A1 A2 B1 B2 : ℝ} (hX : Probability.IsCommonEventTwoTermBigOWith mu Psi1 Psi2 X A1 A2) (h1 : A1 ≤ B1) (h2 : A2 ≤ B2) : Probability.IsCommonEventTwoTermBigOWith mu Psi1 Psi2 X B1 B2

Amplitude monotonicity for the common-event two-term relation. The two envelopes and the common event are unchanged; only the two scales grow.

theorem Algsuperdiff.Section3.Provider.Homogenization.isCommonEventTwoTermBigOWith_add_const {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {I : Type u_2} [MeasureTheory.IsFiniteMeasure mu] {Psi1 Psi2 : ℝ → ℝ} {X : I → Omega → ℝ} {A1 A2 c : ℝ} (hX : Probability.IsCommonEventTwoTermBigOWith mu Psi1 Psi2 X A1 A2) (hc : 0 ≤ c) : Probability.IsCommonEventTwoTermBigOWith mu Psi1 Psi2 (fun (i : I) (omega : Omega) => X i omega + c) (A1 + c) A2

A nonnegative deterministic shift is absorbed by the first lane at the cost of the same shift in its amplitude.

This is the absorption performed at ABK26, where the deterministic mean bound (1/2) epsilon E^2 gamma produced by the iteration is added to the fluctuation estimate and the sum is rewritten as a single Gamma_1 term.

theorem Algsuperdiff.Section3.Provider.Homogenization.isCommonEventTwoTermBigOWith_of_ae_forall_exists_le {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {I : Type u_2} {J : Type u_3} {Psi1 Psi2 : ℝ → ℝ} {W : J → Omega → ℝ} {X : I → Omega → ℝ} {A1 A2 : ℝ} (hW : Probability.IsCommonEventTwoTermBigOWith mu Psi1 Psi2 W A1 A2) (hXm : ∀ (i : I), Measurable (X i)) (hle : ∀ᵐ (omega : Omega) ∂mu, ∀ (i : I), ∃ (j : J), X i omega ≤ W j omega) : Probability.IsCommonEventTwoTermBigOWith mu Psi1 Psi2 X A1 A2

Transfer of a common-event two-term bound along an almost-sure pointwise domination by members of the bounded family.

The new family may be indexed by an arbitrary type: the domination is one almost-sure statement whose index quantifier sits inside the event, so no intersection over the new index is taken. This is the step that lets an uncountable index inherit the bound obtained for a countable one.

theorem Algsuperdiff.Section3.Provider.Homogenization.isCommonEventTwoTermBigOWith_of_summable_isTwoTermBigOWith {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {sigmaOne sigmaTwo : ℝ} (hsigmaOne : 0 < sigmaOne) (hsigmaTwo : 0 < sigmaTwo) {aOne aTwo : ℕ → ℝ} (haOne : Summable aOne) (haTwo : Summable aTwo) {W : ℕ → Omega → ℝ} (hW : ∀ (j : ℕ), Probability.IsTwoTermBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigmaOne) (HCPolySupport.IndependentSums.gammaSigma sigmaTwo) (W j) (aOne j) (aTwo j)) : Probability.IsCommonEventTwoTermBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigmaOne) (HCPolySupport.IndependentSums.gammaSigma sigmaTwo) W (HCPolySupport.IndependentSums.gammaTriangleConst sigmaOne * ∑' (j : ℕ), aOne j) (HCPolySupport.IndependentSums.gammaTriangleConst sigmaTwo * ∑' (j : ℕ), aTwo j)

The countable aggregation. A sequence of one-sided two-term weak-Orlicz bounds with summable amplitudes admits one pair of measurable envelopes dominating every member on a single event of probability one, at the two amplitudes C_triangle(sigma) * sum a.

Positivity of the individual amplitudes is not a hypothesis: it is carried by each two-term datum. No independence between the members is used.