CommonEnvelope

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

Common envelopes for two countable Orlicz channels

The Section 3.5 cutoff union is countable, but its conclusion requires one pair of measurable witnesses chosen before every cutoff index. This module performs exactly that quantifier exchange for two summable families of weak-Orlicz scales. It does not use independence or identify any source-facing node.

The proof takes the sum of measurable absolute-value representatives in each channel. Summability almost everywhere follows from the channel tails, and the countable Gamma_sigma triangle inequality controls the resulting common envelopes.

References

• ABK26, Appendix.
• ABK26, Proposition p.homogenization.step.

theorem Algsuperdiff.Section3.Provider.Orlicz.exists_twoChannel_commonEnvelope_of_summable {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {sigmaOne sigmaTwo : ℝ} (hsigmaOne : 0 < sigmaOne) (hsigmaTwo : 0 < sigmaTwo) {aOne aTwo : ℕ → ℝ} (haOne : ∀ (j : ℕ), 0 < aOne j) (haTwo : ∀ (j : ℕ), 0 < aTwo j) (haOneSummable : Summable aOne) (haTwoSummable : Summable aTwo) {FOne FTwo : ℕ → Omega → ℝ} (hFOneMeas : ∀ (j : ℕ), AEMeasurable (FOne j) mu) (hFTwoMeas : ∀ (j : ℕ), AEMeasurable (FTwo j) mu) (hFOne : ∀ (j : ℕ), HCPolySupport.IndependentSums.IsBigO mu (HCPolySupport.IndependentSums.gammaSigma sigmaOne) (FOne j) (aOne j)) (hFTwo : ∀ (j : ℕ), HCPolySupport.IndependentSums.IsBigO mu (HCPolySupport.IndependentSums.gammaSigma sigmaTwo) (FTwo j) (aTwo j)) : ∃ (SOne : Omega → ℝ) (STwo : Omega → ℝ), Measurable SOne ∧ Measurable STwo ∧ (∀ (j : ℕ), (fun (omega : Omega) => |FOne j omega|) ≤ᵐ[mu] SOne) ∧ (∀ (j : ℕ), (fun (omega : Omega) => |FTwo j omega|) ≤ᵐ[mu] STwo) ∧ HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigmaOne) SOne (HCPolySupport.IndependentSums.gammaTriangleConst sigmaOne * ∑' (j : ℕ), aOne j) ∧ HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma sigmaTwo) STwo (HCPolySupport.IndependentSums.gammaTriangleConst sigmaTwo * ∑' (j : ℕ), aTwo j)

Two countable families with summable positive Gamma_sigma scales admit one measurable envelope in each channel. The witnesses are selected before the family index, and each domination statement holds on a conull event.

This is a candidate countable-envelope mechanism for the Section 3.5 cutoff union. It deliberately keeps the two tail exponents and their scales separate.