TwoTermCalculus

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

Two-term weak-Orlicz calculus

Generic, unconditional A for the Section 3 two-term one-sided weak-Orlicz relations Algsuperdiff.Section3.Probability.IsTwoTermBigOWith and Algsuperdiff.Section3.Probability.IsTwoTermBigOWithWitnesses, together with the Γ_σ scale calculus the Section 3.6 assembly consumes.

Every declaration here is a proved local helper of the Provider layer.

Main results

• isBigOWith_of_forall_add_pos: a one-sided weak-Orlicz bound at scale A follows from the same bound at every strictly larger scale.
• isTwoTermBigOWithWitnesses_mono_scales, isTwoTermBigOWith_mono_scales: amplitude monotonicity, with and without the named witness pair.
• isBigOWith_gammaSigma_tsum_of_nonneg_amplitude and its majorant form isBigOWith_gammaSigma_tsum_of_nonneg_amplitude_of_tsum_le: the countable Γ_σ triangle inequality with nonnegative rather than positive amplitudes.
• isBigOWith_gammaSigma_add: the two-summand form of the same estimate.
• isTwoTermBigOWithWitnesses_sqrt_of_sq: the square-root buckle F² ≤ O_{Γ_{σ₁}}(A) + O_{Γ_{σ₂}}(B) ⟹ F ≤ O_{Γ_{2σ₁}}(√A) + O_{Γ_{2σ₂}}(√B), with the named output witnesses √(Y ∨ 0), √(Z ∨ 0). Its call-site variants isTwoTermBigOWithWitnesses_sqrt_of_sq_of_eq and isTwoTermBigOWithWitnesses_sqrt_of_sq_one_quarter take the output exponents as equations τᵢ = 2 σᵢ rather than as literal products.
• isBigOWith_gammaSigma_mono_exponent: downgrading the stretched-exponential index of a one-sided display.
• isTwoTermBigOWithWitnesses_mono_exponent, isTwoTermBigOWith_mono_exponent: lane-wise exponent downgrade of a two-term display, witnesses and amplitudes preserved, no constant paid.
• cstar_pos, sigmaBar_pos, neZero_of_model, dim_pos_of_model: the named positivity facts of the standing model.

References

• ABK26, Appendix (the two-term notation).
• ABK26, Lemma l.Gamma.sigma.triangle.

1. Scale limits

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_of_forall_add_pos {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Ψ : ℝ → ℝ} {X : Ω → ℝ} {A : ℝ} (h : ∀ (ε : ℝ), 0 < ε → HCPolySupport.IndependentSums.IsBigOWith μ Ψ X (A + ε)) : HCPolySupport.IndependentSums.IsBigOWith μ Ψ X A

A one-sided weak-Orlicz upper-tail bound at scale A follows from the same bound at every strictly larger scale.

The upper-tail events at the scales A + 1/(n+1) increase to the upper-tail event at A, so continuity of the measure from below transfers the common bound. This is the device that removes strict positivity from amplitudes.

2. Nonnegative normalization of a witness (consumed, not re-derived)

This section declares nothing. The two scalar/tail facts the two-term displays below need at this place are proved elsewhere and are consumed:

• the positive-part clamp of a one-sided tail at a strictly positive scale is Algsuperdiff.Section3.Provider.Tail.isBigOWith_max_zero (Algsuperdiff/Section3/Provider/Tail/TailSqrt.lean). It is stated with the argument order max 0 (Y ω); the displays below normalize witnesses as max (Y ω) 0, and the two are exchanged by max_comm at the point of use.
• subadditivity of √ on the nonnegative reals is CoarseGraining's Homogenization.sqrt_add_le_add_sqrt_of_nonneg (Homogenization/Deterministic/WeakNormInterfaces/Definitions.lean), already in this file's import closure.

Both were previously re-derived here as private theorems; those private re-derivations are deleted.

4. Amplitude monotonicity

theorem Algsuperdiff.Section3.Provider.Orlicz.isTwoTermBigOWithWitnesses_mono_scales {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Ψ₁ Ψ₂ : ℝ → ℝ} {X Y Z : Ω → ℝ} {A₁ A₂ B₁ B₂ : ℝ} (h : Probability.IsTwoTermBigOWithWitnesses μ Ψ₁ Ψ₂ X Y Z A₁ A₂) (h₁ : A₁ ≤ B₁) (h₂ : A₂ ≤ B₂) : Probability.IsTwoTermBigOWithWitnesses μ Ψ₁ Ψ₂ X Y Z B₁ B₂

Amplitude monotonicity preserving the witnesses. The two witnesses Y and Z are untouched, so any side clause naming them -- for instance the s ≤ Cms * ε refinement of the frozen multiscale conclusion -- survives the enlargement verbatim.

Only A₁ ≤ B₁ and A₂ ≤ B₂ are needed: strict positivity of B₁ and B₂ comes from the strict positivity of A₁ and A₂ already bundled in the hypothesis.

theorem Algsuperdiff.Section3.Provider.Orlicz.isTwoTermBigOWith_mono_scales {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Ψ₁ Ψ₂ : ℝ → ℝ} {X : Ω → ℝ} {A₁ A₂ B₁ B₂ : ℝ} (h : Probability.IsTwoTermBigOWith μ Ψ₁ Ψ₂ X A₁ A₂) (h₁ : A₁ ≤ B₁) (h₂ : A₂ ≤ B₂) : Probability.IsTwoTermBigOWith μ Ψ₁ Ψ₂ X B₁ B₂

Amplitude monotonicity for the existential two-term relation.

6. The Γ_σ triangle inequality at nonnegative amplitudes

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_gammaSigma_tsum_of_nonneg_amplitude {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → ℝ} {a : ℕ → ℝ} {σ : ℝ} (hσ : 0 < σ) (hX_nonneg : ∀ (k : ℕ) (ω : Ω), 0 ≤ X k ω) (hX_meas : ∀ (k : ℕ), Measurable (X k)) (ha : ∀ (k : ℕ), 0 ≤ a k) (ha_summable : Summable a) (hX : ∀ (k : ℕ), HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (X k) (a k)) : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (fun (ω : Ω) => ∑' (k : ℕ), X k ω) (HCPolySupport.IndependentSums.gammaTriangleConst σ * ∑' (k : ℕ), a k)

Countable Γ_σ triangle inequality for nonnegative summands at nonnegative amplitudes.

This is the proved positive-amplitude statement isBigOWith_gammaSigma_tsum with ∀ k, 0 < a k weakened to ∀ k, 0 ≤ a k. The positive statement is consumed, never re-proved: the amplitudes are perturbed to a k + δ 2^{-k}, which shifts the conclusion by 2 δ gammaTriangleConst σ, and isBigOWith_of_forall_add_pos removes the perturbation in the limit δ ↓ 0.

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_gammaSigma_tsum_of_nonneg_amplitude_of_tsum_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → ℝ} {a : ℕ → ℝ} {σ B : ℝ} (hσ : 0 < σ) (hX_nonneg : ∀ (k : ℕ) (ω : Ω), 0 ≤ X k ω) (hX_meas : ∀ (k : ℕ), Measurable (X k)) (ha : ∀ (k : ℕ), 0 ≤ a k) (ha_summable : Summable a) (hX : ∀ (k : ℕ), HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (X k) (a k)) (hB : ∑' (k : ℕ), a k ≤ B) : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (fun (ω : Ω) => ∑' (k : ℕ), X k ω) (HCPolySupport.IndependentSums.gammaTriangleConst σ * B)

The nonnegative-amplitude countable triangle inequality stated against an arbitrary majorant B of the amplitude series, which is the form used at the ABK26 call sites. This is the nonnegative-amplitude twin of the proved isBigOWith_gammaSigma_tsum_of_tsum_le (Algsuperdiff/Section3/Provider/Orlicz/TsumTriangle.lean).

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_gammaSigma_add {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f g : Ω → ℝ} {a b σ : ℝ} (hσ : 0 < σ) (hf_nonneg : ∀ (ω : Ω), 0 ≤ f ω) (hg_nonneg : ∀ (ω : Ω), 0 ≤ g ω) (hf_meas : Measurable f) (hg_meas : Measurable g) (ha : 0 ≤ a) (hb : 0 ≤ b) (hf : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) f a) (hg : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) g b) : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (fun (ω : Ω) => f ω + g ω) (HCPolySupport.IndependentSums.gammaTriangleConst σ * (a + b))

Two-summand Γ_σ triangle inequality for nonnegative observables at nonnegative amplitudes.

The constant gammaTriangleConst σ is the cost of the countable engine this statement is specialized from, and is carried here by choice, so that the binary and the countable statement run on one engine. It is not the only possible constant, and the earlier claim in this docstring that it "cannot be removed" was false and is withdrawn: cheaper proved binary publics are named in the module header's constant-bookkeeping block (ConclusionSeam3Closure.lean at (1 + Real.log 2) ^ σ⁻¹ * (a + b) with neither nonnegativity nor measurability, TailSqrt.lean, and BlockPayload.lean), and ABK26's l.Gamma.sigma.triangle prints factor 1 for σ ≥ 1.

8. The square-root buckle

theorem Algsuperdiff.Section3.Provider.Orlicz.isTwoTermBigOWithWitnesses_sqrt_of_sq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {σ₁ σ₂ : ℝ} (hσ₁ : 0 < σ₁) (hσ₂ : 0 < σ₂) {F Y Z : Ω → ℝ} {A B : ℝ} (hF_nonneg : ∀ (ω : Ω), 0 ≤ F ω) (h : Probability.IsTwoTermBigOWithWitnesses μ (HCPolySupport.IndependentSums.gammaSigma σ₁) (HCPolySupport.IndependentSums.gammaSigma σ₂) (fun (ω : Ω) => F ω ^ 2) Y Z A B) : Probability.IsTwoTermBigOWithWitnesses μ (HCPolySupport.IndependentSums.gammaSigma (2 * σ₁)) (HCPolySupport.IndependentSums.gammaSigma (2 * σ₂)) F (fun (ω : Ω) => √(max (Y ω) 0)) (fun (ω : Ω) => √(max (Z ω) 0)) √A √B

The square-root transfer, with named output witnesses.

If a nonnegative observable F has F² dominated by the named witness pair Y, Z at the exponents σ₁, σ₂ and amplitudes A, B, then F itself is dominated by the named pair √(Y ∨ 0), √(Z ∨ 0) at the exponents 2σ₁, 2σ₂ and amplitudes √A, √B. Naming the output witnesses is what lets a caller keep a side clause about them across the buckle.

No constant is lost. The pointwise step is F = √(F²) ≤ √(Y ∨ 0 + Z ∨ 0) ≤ √(Y ∨ 0) + √(Z ∨ 0), whose last inequality is CoarseGraining's Homogenization.sqrt_add_le_add_sqrt_of_nonneg. Each lane's tail step is the proved Provider.Tail.isBigOWith_gammaSigma_sqrt (Algsuperdiff/Section3/Provider/Tail/TailSqrt.lean, the p = 1/2 power rule), applied to the clamped witness produced by Provider.Tail.isBigOWith_max_zero (ibid.:163).

Measurability of F is not a premise: it follows from measurability of F², which the hypothesis carries, together with F = √(F²).

theorem Algsuperdiff.Section3.Provider.Orlicz.isTwoTermBigOWithWitnesses_sqrt_of_sq_of_eq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {σ₁ σ₂ τ₁ τ₂ : ℝ} (hσ₁ : 0 < σ₁) (hσ₂ : 0 < σ₂) (hτ₁ : τ₁ = 2 * σ₁) (hτ₂ : τ₂ = 2 * σ₂) {F Y Z : Ω → ℝ} {A B : ℝ} (hF_nonneg : ∀ (ω : Ω), 0 ≤ F ω) (h : Probability.IsTwoTermBigOWithWitnesses μ (HCPolySupport.IndependentSums.gammaSigma σ₁) (HCPolySupport.IndependentSums.gammaSigma σ₂) (fun (ω : Ω) => F ω ^ 2) Y Z A B) : Probability.IsTwoTermBigOWithWitnesses μ (HCPolySupport.IndependentSums.gammaSigma τ₁) (HCPolySupport.IndependentSums.gammaSigma τ₂) F (fun (ω : Ω) => √(max (Y ω) 0)) (fun (ω : Ω) => √(max (Z ω) 0)) √A √B

The witness-level buckle with the output exponents supplied as equations τᵢ = 2 σᵢ rather than as the literal terms 2 * σᵢ.

This is pure call-site ergonomics: a consumer whose target display is stated at, say, gammaSigma (1/2) does not have to rewrite gammaSigma (2 * (1/4)) into it, but discharges (1/2 : ℝ) = 2 * (1/4) by norm_num.

theorem Algsuperdiff.Section3.Provider.Orlicz.isTwoTermBigOWithWitnesses_sqrt_of_sq_one_quarter {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {F Y Z : Ω → ℝ} {A B : ℝ} (hF_nonneg : ∀ (ω : Ω), 0 ≤ F ω) (h : Probability.IsTwoTermBigOWithWitnesses μ (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma (1 / 4)) (fun (ω : Ω) => F ω ^ 2) Y Z A B) : Probability.IsTwoTermBigOWithWitnesses μ (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) F (fun (ω : Ω) => √(max (Y ω) 0)) (fun (ω : Ω) => √(max (Z ω) 0)) √A √B

9. Downgrading the stretched-exponential index

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_gammaSigma_mono_exponent {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {A σ σ' : ℝ} (hσσ' : σ' ≤ σ) (h : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) X A) : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ') X A

A Γ_σ upper tail at scale A is in particular a Γ_{σ'} upper tail at the same scale whenever σ' ≤ σ. No constant is paid. The engine is CoarseGraining's Homogenization.Book.Ch04.IsBigOWith.gammaSigma_mono_exponent, which is consumed, not re-proved.

theorem Algsuperdiff.Section3.Provider.Orlicz.isTwoTermBigOWithWitnesses_mono_exponent {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {σ₁ σ₂ σ₁' σ₂' : ℝ} (hσ₁' : 0 < σ₁') (hσ₂' : 0 < σ₂') (h₁ : σ₁' ≤ σ₁) (h₂ : σ₂' ≤ σ₂) {X Y Z : Ω → ℝ} {A₁ A₂ : ℝ} (h : Probability.IsTwoTermBigOWithWitnesses μ (HCPolySupport.IndependentSums.gammaSigma σ₁) (HCPolySupport.IndependentSums.gammaSigma σ₂) X Y Z A₁ A₂) : Probability.IsTwoTermBigOWithWitnesses μ (HCPolySupport.IndependentSums.gammaSigma σ₁') (HCPolySupport.IndependentSums.gammaSigma σ₂') X Y Z A₁ A₂

Lane-wise exponent downgrade of a two-term display, preserving the witnesses. Both exponents may be lowered independently; the observable, the two witnesses and the two amplitudes are untouched, and no constant is paid.

The engine is isBigOWith_gammaSigma_mono_exponent above, applied once per lane. The only positivity required is 0 < σ₁' and 0 < σ₂', and only because the carrier IsTwoTermBigOWithWitnesses bundles IsAdmissibleTail (gammaSigma σᵢ'), which Probability.isAdmissibleTail_gammaSigma supplies exactly from strict positivity of the target exponent. Positivity of σ₁ and σ₂ is not a premise: it follows from 0 < σᵢ' ≤ σᵢ.

theorem Algsuperdiff.Section3.Provider.Orlicz.isTwoTermBigOWith_mono_exponent {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {σ₁ σ₂ σ₁' σ₂' : ℝ} (hσ₁' : 0 < σ₁') (hσ₂' : 0 < σ₂') (h₁ : σ₁' ≤ σ₁) (h₂ : σ₂' ≤ σ₂) {X : Ω → ℝ} {A₁ A₂ : ℝ} (h : Probability.IsTwoTermBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ₁) (HCPolySupport.IndependentSums.gammaSigma σ₂) X A₁ A₂) : Probability.IsTwoTermBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ₁') (HCPolySupport.IndependentSums.gammaSigma σ₂') X A₁ A₂

Lane-wise exponent downgrade for the existential two-term relation.

10. Named positivity facts of the standing model

theorem Algsuperdiff.Section3.Provider.Orlicz.cstar_pos {d : ℕ} (M : ABKModel d) : 0 < Disorder.cstar M

The J4 non-degeneracy constant of the standing model is positive. This is the first conjunct of the proved unique-choice characterization.

theorem Algsuperdiff.Section3.Provider.Orlicz.sigmaBar_pos {d : ℕ} (M : ABKModel d) (m : ℤ) : 0 < ↑(Annealed.sigmaBar M m)

The running diffusivity of the standing model is positive at every scale. This is the first conjunct of the proved unique-choice characterization.

theorem Algsuperdiff.Section3.Provider.Orlicz.neZero_of_model {d : ℕ} (M : ABKModel d) : NeZero d

The paper-wide standing assumption 2 ≤ d, stored in the model, supplies the nonzero-dimension fact. This is a theorem and deliberately not an instance: registering it would leak a NeZero instance into unrelated typeclass searches.

theorem Algsuperdiff.Section3.Provider.Orlicz.dim_pos_of_model {d : ℕ} (M : ABKModel d) : 0 < d

The dimension of the standing model is positive.