HolderEstimate

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

The stream-field Hölder estimate

This module joins the crossover estimate at distances below one to the linear growth estimate at larger distances. The resulting exponent is gamma / 2 and the radius-dependent modulus has polynomial growth of degree one.

theorem Algsuperdiff.Section5.Field.matrixOperatorNorm_streamField_sub_le {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {R : ℝ} (hR : 1 ≤ R) {x y : HCPolySupport.Vec d} (hx : √(HCPolySupport.vecNormSq x) ≤ R) (hy : √(HCPolySupport.vecNormSq y) ≤ R) : HCPolySupport.Book.Ch02.matrixOperatorNorm (streamField omega x - streamField omega y) ≤ streamFieldHolderModulus M omega R * ‖x - y‖.rpow (streamHolderExponent M)

The quantitative stream-field modulus. On the Euclidean ball of radius R ≥ 1, the field is Hölder continuous with exponent M.gamma / 2 and constant streamFieldHolderConst M omega * (1 + R).

theorem Algsuperdiff.Section5.Field.matrixOperatorNorm_streamField_sub_le_of_euclidean {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {R : ℝ} (hR : 1 ≤ R) {x y : HCPolySupport.Vec d} (hx : √(HCPolySupport.vecNormSq x) ≤ R) (hy : √(HCPolySupport.vecNormSq y) ≤ R) : HCPolySupport.Book.Ch02.matrixOperatorNorm (streamField omega x - streamField omega y) ≤ streamFieldHolderModulus M omega R * (√(HCPolySupport.vecNormSq (x - y))).rpow (streamHolderExponent M)

Euclidean-distance form of the quantitative modulus.