MixedAllocation

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

Deterministic mixed two-lane Orlicz allocation

ABK26 uses, in the proof of Proposition p.homogenization.step, a random variable carrying a two-term weak-Orlicz bound at the pair of exponents (1, 1/4) as if it were a pair of single-lane variables, one for each exponent, so that the finite-range concentration corollary of Proposition p.concentration may be applied lane by lane. Neither obvious splitting survives that step: the witnesses of the two-term relation are arbitrary random variables, in no way functions of the original one, so nothing makes them measurable for the local σ-field of the cube that carries it, and they only dominate it rather than sum to it; while a deterministic truncation at a fixed threshold is local but pays the truncation level, not the linear amplitude, in its Γ_1 lane.

This module supplies the deterministic allocation that does survive. For positive amplitudes a and b the profile

mixedProfile a b t = a * t + b * t ^ 4

is the exact composite threshold appearing in the two-term tail: a times the inverse of Γ_1 at level e^{-t} plus b times the inverse of Γ_{1/4} at the same level. It is a strictly increasing bijection of [0, ∞) onto itself, so a real number x has a unique allocation time mixedTime a b |x|, and the two summands of the profile at that time, resigned to the sign of x, are two lanes

linearLane a b x + quarticLane a b x = x

that are fixed Borel functions of x alone. Composing them with a random variable therefore preserves every σ-field the variable is measurable for; this is measurable_linearLane_comp and measurable_quarticLane_comp, and it is what transfers locality, and with it independence, to the lanes.

The tail transfer is isBigO_gammaSigma_one_linearLane_comp and isBigO_gammaSigma_quarter_quarticLane_comp: a mixed tail P[|X| > mixedProfile a b t] ≤ C e^{-t} gives a genuine one-lane O_{Γ_1}(c a) bound for the linear lane and a genuine one-lane O_{Γ_{1/4}}(c' b) bound for the quartic lane, where the tail constant C is absorbed into the amplitudes by the single logarithmic shift laneAbsorb C.

Allocation destroys exact centering. Both variants are supplied: the raw lanes with explicit mean bounds (abs_integral_linearLane_comp_le and its quartic twin), and the centered lanes centeredLinearLane and centeredQuarticLane, whose sum reproduces X exactly when X is centered, and whose amplitudes pay the constant factor laneCenterConst.

References

• ABK26, Appendix (the two-term weak-Orlicz notation and e.Gamma.sigma).
• ABK26, Proposition p.homogenization.step.

The two-channel profile and its inverse

def Algsuperdiff.Section3.Provider.Orlicz.mixedProfile (a b t : ℝ) : ℝ

The composite threshold of a two-term (Γ_1, Γ_{1/4}) tail at level e^{-t}: the linear amplitude times t plus the quartic amplitude times t ^ 4.

Equations

• Algsuperdiff.Section3.Provider.Orlicz.mixedProfile a b t = a * t + b * t ^ 4

theorem Algsuperdiff.Section3.Provider.Orlicz.continuous_mixedProfile (a b : ℝ) : Continuous (mixedProfile a b)

@[simp]

theorem Algsuperdiff.Section3.Provider.Orlicz.mixedProfile_zero (a b : ℝ) : mixedProfile a b 0 = 0

theorem Algsuperdiff.Section3.Provider.Orlicz.strictMonoOn_mixedProfile {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : StrictMonoOn (mixedProfile a b) (Set.Ici 0)

theorem Algsuperdiff.Section3.Provider.Orlicz.exists_mixedProfile_eq {a b y : ℝ} (ha : 0 < a) (hb : 0 < b) (hy : 0 ≤ y) : ∃ t ∈ Set.Ici 0, mixedProfile a b t = y

The profile is onto [0, ∞): every nonnegative level is attained at a nonnegative time. This is the intermediate value theorem on [0, y / a].

noncomputable def Algsuperdiff.Section3.Provider.Orlicz.mixedTime (a b y : ℝ) : ℝ

The allocation time: the nonnegative inverse of mixedProfile. The unused negative branch makes it a total real function.

Equations

• Algsuperdiff.Section3.Provider.Orlicz.mixedTime a b y = if 0 ≤ y then Function.invFunOn (Algsuperdiff.Section3.Provider.Orlicz.mixedProfile a b) (Set.Ici 0) y else 0

theorem Algsuperdiff.Section3.Provider.Orlicz.mixedProfile_mixedTime {a b y : ℝ} (ha : 0 < a) (hb : 0 < b) (hy : 0 ≤ y) : mixedProfile a b (mixedTime a b y) = y

theorem Algsuperdiff.Section3.Provider.Orlicz.mixedTime_nonneg {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (y : ℝ) : 0 ≤ mixedTime a b y

theorem Algsuperdiff.Section3.Provider.Orlicz.monotone_mixedTime {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : Monotone (mixedTime a b)

theorem Algsuperdiff.Section3.Provider.Orlicz.measurable_mixedTime {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : Measurable (mixedTime a b)

The two lanes

noncomputable def Algsuperdiff.Section3.Provider.Orlicz.linearLane (a b x : ℝ) : ℝ

The Γ_1 lane of the allocation: the linear part of the profile at the allocation time of |x|, carrying the sign of x.

Equations

• Algsuperdiff.Section3.Provider.Orlicz.linearLane a b x = x / |x| * (a * Algsuperdiff.Section3.Provider.Orlicz.mixedTime a b |x|)

noncomputable def Algsuperdiff.Section3.Provider.Orlicz.quarticLane (a b x : ℝ) : ℝ

The Γ_{1/4} lane of the allocation: the quartic part of the profile at the allocation time of |x|, carrying the sign of x.

Equations

• Algsuperdiff.Section3.Provider.Orlicz.quarticLane a b x = x / |x| * (b * Algsuperdiff.Section3.Provider.Orlicz.mixedTime a b |x| ^ 4)

theorem Algsuperdiff.Section3.Provider.Orlicz.abs_div_abs_self_le_one (x : ℝ) : |x / |x|| ≤ 1

theorem Algsuperdiff.Section3.Provider.Orlicz.linearLane_add_quarticLane {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (x : ℝ) : linearLane a b x + quarticLane a b x = x

The allocation is a pointwise splitting. The two lanes are exact summands of the identity.

theorem Algsuperdiff.Section3.Provider.Orlicz.measurable_linearLane {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : Measurable (linearLane a b)

theorem Algsuperdiff.Section3.Provider.Orlicz.measurable_quarticLane {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : Measurable (quarticLane a b)

theorem Algsuperdiff.Section3.Provider.Orlicz.measurable_linearLane_comp {Ω : Type u_1} {m : MeasurableSpace Ω} {a b : ℝ} (ha : 0 < a) (hb : 0 < b) {X : Ω → ℝ} (hX : Measurable X) : Measurable fun (ω : Ω) => linearLane a b (X ω)

Locality transfer for the linear lane. The lane is a fixed Borel function of the value alone, so composing it with a random variable preserves every σ-field that variable is measurable for.

theorem Algsuperdiff.Section3.Provider.Orlicz.measurable_quarticLane_comp {Ω : Type u_1} {m : MeasurableSpace Ω} {a b : ℝ} (ha : 0 < a) (hb : 0 < b) {X : Ω → ℝ} (hX : Measurable X) : Measurable fun (ω : Ω) => quarticLane a b (X ω)

Locality transfer for the quartic lane.

theorem Algsuperdiff.Section3.Provider.Orlicz.abs_linearLane_le {a b x s : ℝ} (ha : 0 < a) (hb : 0 < b) (hs : mixedTime a b |x| ≤ s) : |linearLane a b x| ≤ a * s

theorem Algsuperdiff.Section3.Provider.Orlicz.abs_quarticLane_le {a b x s : ℝ} (ha : 0 < a) (hb : 0 < b) (hs : mixedTime a b |x| ≤ s) : |quarticLane a b x| ≤ b * s ^ 4

theorem Algsuperdiff.Section3.Provider.Orlicz.absTailEvent_linearLane_comp_subset {Ω : Type u_1} (X : Ω → ℝ) {a b s : ℝ} (ha : 0 < a) (hb : 0 < b) (hs : 0 ≤ s) : HCPolySupport.IndependentSums.absTailEvent (fun (ω : Ω) => linearLane a b (X ω)) (a * s) ⊆ HCPolySupport.IndependentSums.absTailEvent X (mixedProfile a b s)

Above the linear share of the profile, the linear lane can only be large where the original value already exceeds the whole profile.

theorem Algsuperdiff.Section3.Provider.Orlicz.absTailEvent_quarticLane_comp_subset {Ω : Type u_1} (X : Ω → ℝ) {a b s : ℝ} (ha : 0 < a) (hb : 0 < b) (hs : 0 ≤ s) : HCPolySupport.IndependentSums.absTailEvent (fun (ω : Ω) => quarticLane a b (X ω)) (b * s ^ 4) ⊆ HCPolySupport.IndependentSums.absTailEvent X (mixedProfile a b s)

Above the quartic share of the profile, the quartic lane can only be large where the original value already exceeds the whole profile.

The mixed tail datum

def Algsuperdiff.Section3.Provider.Orlicz.HasMixedGammaTailWith {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (X : Ω → ℝ) (C a b : ℝ) : Prop

The two-term tail at the composite profile: for every level t ≥ 1 the variable exceeds mixedProfile a b t with probability at most C e^{-t}. This is the shape produced by a two-term (Γ_1, Γ_{1/4}) weak-Orlicz bound at amplitudes a and b; see hasMixedGammaTailWith_two_of_isTwoTermBigOWith_abs.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Orlicz.rpow_quarter_pow_four {u : ℝ} (hu : 0 ≤ u) : (u ^ (1 / 4)) ^ 4 = u

(u ^ (1/4)) ^ 4 = u on the nonnegative reals; the only place where a real power of the level appears.

theorem Algsuperdiff.Section3.Provider.Orlicz.pow_four_rpow_quarter {t : ℝ} (ht : 0 ≤ t) : (t ^ 4) ^ (1 / 4) = t

(t ^ 4) ^ (1/4) = t on the nonnegative reals: the quartic level of the two-term tail returns the linear level.

theorem Algsuperdiff.Section3.Provider.Orlicz.hasMixedGammaTailWith_two_of_isTwoTermBigOWith_abs {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {A₁ A₄ : ℝ} (hX : Probability.IsTwoTermBigOWith μ (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma (1 / 4)) (fun (ω : Ω) => |X ω|) A₁ A₄) : HasMixedGammaTailWith μ X 2 A₁ A₄

The bridge from the proved two-term vocabulary. A two-term one-sided weak-Orlicz bound for |X| at the exponents 1 and 1/4 gives the mixed tail at the same two amplitudes, with tail constant 2: the two witness tails are evaluated at the levels t and t ^ 4, both of which return e^{-t}.

Absorbing the tail constant into the amplitude

noncomputable def Algsuperdiff.Section3.Provider.Orlicz.laneAbsorb (C : ℝ) : ℝ

The logarithmic amplitude shift that turns a tail bound C e^{-t} into a genuine e^{-t} bound at the enlarged amplitude.

Equations

• Algsuperdiff.Section3.Provider.Orlicz.laneAbsorb C = 1 + Real.log (max 1 C)

theorem Algsuperdiff.Section3.Provider.Orlicz.one_le_laneAbsorb (C : ℝ) : 1 ≤ laneAbsorb C

theorem Algsuperdiff.Section3.Provider.Orlicz.laneAbsorb_pos (C : ℝ) : 0 < laneAbsorb C

theorem Algsuperdiff.Section3.Provider.Orlicz.mul_exp_neg_laneAbsorb_mul_le (C : ℝ) {w : ℝ} (hw : 1 ≤ w) : C * Real.exp (-(laneAbsorb C * w)) ≤ Real.exp (-w)

The defining property of the shift: at every level w ≥ 1 the constant C is paid for by the extra decay e^{-(laneAbsorb C - 1) w}.

The one-lane tails of the allocation

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigO_gammaSigma_one_linearLane_comp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {C a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hX : HasMixedGammaTailWith μ X C a b) : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma 1) (fun (ω : Ω) => linearLane a b (X ω)) (laneAbsorb C * a)

The linear lane is a genuine Γ_1 variable. A mixed tail with constant C at amplitudes (a, b) gives linearLane a b ∘ X = O_{Γ_1}(λ_C a), with λ_C = laneAbsorb C.

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigO_gammaSigma_quarter_quarticLane_comp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {C a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hX : HasMixedGammaTailWith μ X C a b) : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma (1 / 4)) (fun (ω : Ω) => quarticLane a b (X ω)) (laneAbsorb C ^ 4 * b)

The quartic lane is a genuine Γ_{1/4} variable. A mixed tail with constant C at amplitudes (a, b) gives quarticLane a b ∘ X = O_{Γ_{1/4}}(λ_C ^ 4 b).

Centering a stretched-exponential variable at its own mean

noncomputable def Algsuperdiff.Section3.Provider.Orlicz.laneCenterConst (σ : ℝ) : ℝ

The cost of centering a Γ_σ variable at its own mean: the two-term triangle constant times one plus the first-moment constant.

Equations

• Algsuperdiff.Section3.Provider.Orlicz.laneCenterConst σ = HCPolySupport.IndependentSums.gammaTriangleConst σ * (1 + HCPolySupport.IndependentSums.gammaMomentConst σ)

theorem Algsuperdiff.Section3.Provider.Orlicz.laneCenterConst_pos {σ : ℝ} (hσ : 0 < σ) : 0 < laneCenterConst σ

theorem Algsuperdiff.Section3.Provider.Orlicz.integrable_of_isBigO_gammaSigma {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σ K : ℝ} (hσ : 0 < σ) (hK : 0 < K) (hXm : AEMeasurable X μ) (hX : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma σ) X K) : MeasureTheory.Integrable X μ

theorem Algsuperdiff.Section3.Provider.Orlicz.abs_integral_le_of_isBigO_gammaSigma {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σ K : ℝ} (hσ : 0 < σ) (hK : 0 < K) (hXm : AEMeasurable X μ) (hX : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma σ) X K) : |∫ (ω : Ω), X ω ∂μ| ≤ HCPolySupport.IndependentSums.gammaMomentConst σ * K

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigO_gammaSigma_sub_integral {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {σ K : ℝ} (hσ : 0 < σ) (hK : 0 < K) (hXm : AEMeasurable X μ) (hX : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma σ) X K) : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma σ) (fun (ω : Ω) => X ω - ∫ (ω' : Ω), X ω' ∂μ) (laneCenterConst σ * K)

Centering costs a constant factor. A Γ_σ variable stays Γ_σ after subtracting its own mean, at the amplitude laneCenterConst σ times the original one.

theorem Algsuperdiff.Section3.Provider.Orlicz.integral_sub_integral_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hX : MeasureTheory.Integrable X μ) : ∫ (ω : Ω), X ω - ∫ (ω' : Ω), X ω' ∂μ ∂μ = 0

The centered lanes

noncomputable def Algsuperdiff.Section3.Provider.Orlicz.centeredLinearLane {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (a b : ℝ) (X : Ω → ℝ) : Ω → ℝ

The Γ_1 lane of the allocation, recentred at its own mean.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Orlicz.centeredQuarticLane {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (a b : ℝ) (X : Ω → ℝ) : Ω → ℝ

The Γ_{1/4} lane of the allocation, recentred at its own mean.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Orlicz.mixedLinearConst (C : ℝ) : ℝ

The Γ_1 amplitude constant of the centered allocation.

Equations

• Algsuperdiff.Section3.Provider.Orlicz.mixedLinearConst C = Algsuperdiff.Section3.Provider.Orlicz.laneCenterConst 1 * Algsuperdiff.Section3.Provider.Orlicz.laneAbsorb C

noncomputable def Algsuperdiff.Section3.Provider.Orlicz.mixedQuarticConst (C : ℝ) : ℝ

The Γ_{1/4} amplitude constant of the centered allocation.

Equations

• Algsuperdiff.Section3.Provider.Orlicz.mixedQuarticConst C = Algsuperdiff.Section3.Provider.Orlicz.laneCenterConst (1 / 4) * Algsuperdiff.Section3.Provider.Orlicz.laneAbsorb C ^ 4

theorem Algsuperdiff.Section3.Provider.Orlicz.mixedLinearConst_pos (C : ℝ) : 0 < mixedLinearConst C

theorem Algsuperdiff.Section3.Provider.Orlicz.mixedQuarticConst_pos (C : ℝ) : 0 < mixedQuarticConst C

theorem Algsuperdiff.Section3.Provider.Orlicz.integrable_linearLane_comp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {C a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hXm : Measurable X) (hX : HasMixedGammaTailWith μ X C a b) : MeasureTheory.Integrable (fun (ω : Ω) => linearLane a b (X ω)) μ

theorem Algsuperdiff.Section3.Provider.Orlicz.integrable_quarticLane_comp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {C a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hXm : Measurable X) (hX : HasMixedGammaTailWith μ X C a b) : MeasureTheory.Integrable (fun (ω : Ω) => quarticLane a b (X ω)) μ

theorem Algsuperdiff.Section3.Provider.Orlicz.measurable_centeredLinearLane {Ω : Type u_1} {m : MeasurableSpace Ω} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hX : Measurable X) : Measurable (centeredLinearLane μ a b X)

theorem Algsuperdiff.Section3.Provider.Orlicz.measurable_centeredQuarticLane {Ω : Type u_1} {m : MeasurableSpace Ω} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hX : Measurable X) : Measurable (centeredQuarticLane μ a b X)

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigO_gammaSigma_one_centeredLinearLane {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {C a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hXm : Measurable X) (hX : HasMixedGammaTailWith μ X C a b) : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma 1) (centeredLinearLane μ a b X) (mixedLinearConst C * a)

The centered linear lane retains the Γ_1 tail.

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigO_gammaSigma_quarter_centeredQuarticLane {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {C a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hXm : Measurable X) (hX : HasMixedGammaTailWith μ X C a b) : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma (1 / 4)) (centeredQuarticLane μ a b X) (mixedQuarticConst C * b)

The centered quartic lane retains the Γ_{1/4} tail.

theorem Algsuperdiff.Section3.Provider.Orlicz.integral_centeredLinearLane_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {C a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hXm : Measurable X) (hX : HasMixedGammaTailWith μ X C a b) : ∫ (ω : Ω), centeredLinearLane μ a b X ω ∂μ = 0

theorem Algsuperdiff.Section3.Provider.Orlicz.integral_centeredQuarticLane_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {C a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hXm : Measurable X) (hX : HasMixedGammaTailWith μ X C a b) : ∫ (ω : Ω), centeredQuarticLane μ a b X ω ∂μ = 0

theorem Algsuperdiff.Section3.Provider.Orlicz.centeredLinearLane_add_centeredQuarticLane {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {C a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hXm : Measurable X) (hX : HasMixedGammaTailWith μ X C a b) (hXmean : ∫ (ω : Ω), X ω ∂μ = 0) (ω : Ω) : X ω = centeredLinearLane μ a b X ω + centeredQuarticLane μ a b X ω

The centered lanes still split a centered variable exactly. The two mean shifts cancel because the raw lanes sum to X, whose mean is zero.

The packaged two-lane split

theorem Algsuperdiff.Section3.Provider.Orlicz.exists_centeredTwoLaneSplit {Ω : Type u_1} {m : MeasurableSpace Ω} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {C a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hXloc : Measurable X) (hXmeas : Measurable X) (hXtail : HasMixedGammaTailWith μ X C a b) (hXmean : ∫ (ω : Ω), X ω ∂μ = 0) : ∃ (Y : Ω → ℝ) (Z : Ω → ℝ), (∀ (ω : Ω), X ω = Y ω + Z ω) ∧ Measurable Y ∧ Measurable Z ∧ Measurable Y ∧ Measurable Z ∧ HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma 1) Y (mixedLinearConst C * a) ∧ HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma (1 / 4)) Z (mixedQuarticConst C * b) ∧ ∫ (ω : Ω), Y ω ∂μ = 0 ∧ ∫ (ω : Ω), Z ω ∂μ = 0

The deterministic mixed two-lane Orlicz allocation.

A centered variable with a two-term (Γ_1, Γ_{1/4}) tail at amplitudes (a, b) and tail constant C splits into two centered summands, each a fixed Borel function of the variable minus a constant, hence measurable for every σ-field the variable is measurable for, and each carrying a single-lane weak-Orlicz bound at its own exponent and its own amplitude. This is exactly the input format consumed by the two-lane grid concentration display: the two lanes may be fed independently to the one-exponent concentration inequality, and the pointwise identity recombines them.

The witnesses are the explicit centeredLinearLane and centeredQuarticLane; the uncentered core, its explicit mean shifts, and the per-lane statements are available separately in this module.

theorem Algsuperdiff.Section3.Provider.Orlicz.exists_centeredTwoLaneSplit_of_isTwoTermBigOWith_abs {Ω : Type u_1} {m : MeasurableSpace Ω} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {A₁ A₄ : ℝ} (hA₁ : 0 < A₁) (hA₄ : 0 < A₄) (hXloc : Measurable X) (hXmeas : Measurable X) (hXtail : Probability.IsTwoTermBigOWith μ (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma (1 / 4)) (fun (ω : Ω) => |X ω|) A₁ A₄) (hXmean : ∫ (ω : Ω), X ω ∂μ = 0) : ∃ (Y : Ω → ℝ) (Z : Ω → ℝ), (∀ (ω : Ω), X ω = Y ω + Z ω) ∧ Measurable Y ∧ Measurable Z ∧ Measurable Y ∧ Measurable Z ∧ HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma 1) Y (mixedLinearConst 2 * A₁) ∧ HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma (1 / 4)) Z (mixedQuarticConst 2 * A₄) ∧ ∫ (ω : Ω), Y ω ∂μ = 0 ∧ ∫ (ω : Ω), Z ω ∂μ = 0

The same split, fed by the proved two-term weak-Orlicz vocabulary: a two-term one-sided bound for |X| at exponents 1 and 1/4 and amplitudes (A₁, A₄) is enough, the tail constant then being 2.