ConstantWeakening

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

Constant weakening for the coarse-ellipticity tail carriers

Proposition p.cg.ellipticity.bounds (ABK26) is stated as ∃ C(d) < ∞ such that two weak-Orlicz displays hold. Its frozen Lean surface Algsuperdiff.Frozen.Section3.coarse_ellipticity_bounds therefore only records 0 < Ccg, while several consumers need a normalized constant (concretely 1 ≤ Ccg; see Provider/BadEvents/BadEventLemmaCases.lean, whose hCcg binder is exactly that gate). Nothing but monotonicity is needed: the source statement is weaker for a larger constant, in every one of its slots.

This module supplies the three monotonicity facts that make that precise, all of them model-free.

• isLowerIntegerFamilyOrlicz_mono --- the lower-family carrier Probability.IsLowerIntegerFamilyOrlicz is monotone in the deterministic shift b and in the tail scale A. The witness is unchanged; the domination X L ω ≤ b + Y ω only weakens, and the tail weakens by CoarseGraining's IsBigOWith.mono_scale.
• isDeterministicShiftTwoTermOneSidedOrlicz_mono --- the two-term carrier Probability.IsDeterministicShiftTwoTermOneSidedOrlicz is monotone in the deterministic shift b and in both tail scales A₁, A₂, by the same two ingredients.
• lowerEllipticityProfile_mono_const --- the source-corrected deterministic lower profile of Section3/Exponent.lean is monotone in its constant, in all three branches of CoarseEllipticityExponent (finite q < 2 at pole order 2 / q, finite q ≥ 2 at pole order one, and the infinity endpoint). Its two hypotheses 0 ≤ s and 0 ≤ 2 * s - gamma are consequences of the source window s ∈ [gamma/2 + exp(...), 1], not extra premises.

References

• ABK26, p.cg.ellipticity.bounds.
• ABK26, Appendix, (the weak-Orlicz notation).

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isLowerIntegerFamilyOrlicz_mono {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Ψ : ℝ → ℝ} {X : ℤ → Ω → ℝ} {L0 : ℤ} {b b' A A' : ℝ} (hX : Probability.IsLowerIntegerFamilyOrlicz μ Ψ X L0 b A) (hb : b ≤ b') (hA : A ≤ A') : Probability.IsLowerIntegerFamilyOrlicz μ Ψ X L0 b' A'

The lower-indexed source supremum bound weakens when the deterministic shift and the tail scale both increase. The common measurable witness is unchanged.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isDeterministicShiftTwoTermOneSidedOrlicz_mono {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Ψ₁ Ψ₂ : ℝ → ℝ} {X : Ω → ℝ} {b b' A₁ A₁' A₂ A₂' : ℝ} (hX : Probability.IsDeterministicShiftTwoTermOneSidedOrlicz μ Ψ₁ Ψ₂ X b A₁ A₂) (hb : b ≤ b') (hA₁ : A₁ ≤ A₁') (hA₂ : A₂ ≤ A₂') : Probability.IsDeterministicShiftTwoTermOneSidedOrlicz μ Ψ₁ Ψ₂ X b' A₁' A₂'

The one-sided two-term weak-Orlicz relation with a deterministic shift weakens when the shift and both tail scales increase. Both witnesses are unchanged.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.lowerEllipticityProfile_mono_const {C C' gamma s : ℝ} (hs : 0 ≤ s) (hgap : 0 ≤ 2 * s - gamma) (hC : C ≤ C') (q : CoarseEllipticityExponent) : lowerEllipticityProfile C gamma s q ≤ lowerEllipticityProfile C' gamma s q

The source-corrected deterministic lower-ellipticity profile is monotone in its constant, on the whole admissible exponent carrier.

The two hypotheses are exactly what the source window s ∈ [gamma/2 + exp(-C⁻¹E⁻²gamma⁻¹), 1] supplies; they are needed only so that the finite q < 2 branch's real power has a nonnegative base.