GaugeAntitone

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

Antitonicity of the gauge λ_{s,q}^{-1} in the exponent s

ABK26, e.ellipticities.monotone.ordered, read in the inverted direction.

Why this file exists

The event side of that trade is free, and this file is the reason: a larger gauge exponent puts less weight on the deep scales, so

λ_{s,q}^{-1}(Q; a) ≤ λ_{γ,q}^{-1}(Q; a)      whenever  0 < γ ≤ s .

Hence every γ-gauge upper bound the good event supplies is automatically an s-gauge upper bound, at constant 1.

References

• ABK26, e.ellipticities.monotone.ordered.

theorem Algsuperdiff.Section4.Provider.Localize.inv_lambdaSq_antitone_gauge {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {t s : ℝ} {q : HCPolySupport.Book.Ch02.MultiscaleExponent} (ht : 0 < t) (hts : t ≤ s) (hq : q.IsAdmissible) : (HCPolySupport.Book.Ch02.lambdaSq Q s q a)⁻¹ ≤ (HCPolySupport.Book.Ch02.lambdaSq Q t q a)⁻¹

Gauge antitonicity of λ^{-1} (the inverted first inequality of e.ellipticities.monotone.ordered). For 0 < t ≤ s and admissible q,

λ_{s,q}^{-1}(Q; a) ≤ λ_{t,q}^{-1}(Q; a) .

A larger gauge exponent discounts the deep scales more heavily, and the per-depth maxima are nondecreasing in the depth, so raising the exponent can only decrease the gauge's inverse. Constant 1; no cube, field or dimension enters.

theorem Algsuperdiff.Section4.Provider.Localize.inv_lambdaSq_two_antitone_gauge {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {t s : ℝ} (ht : 0 < t) (hts : t ≤ s) : (HCPolySupport.Book.Ch02.lambdaSq Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ ≤ (HCPolySupport.Book.Ch02.lambdaSq Q t (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹

The finite-q instance at q = 2, the only exponent §4.1 uses.