Holder

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

A quantitative subcritical Hölder modulus for the stream matrix

The sharp shell carrier has a linear weight at the shell/cube crossover. At the critical exponent this produces a logarithmic loss. Dropping from gamma to gamma / 2 leaves a geometric factor which absorbs that weight. This file performs that deterministic summation and records a modulus whose dependence on the observation radius is linear.

noncomputable def Algsuperdiff.Section5.Field.streamHolderExponent {d : ℕ} (M : Section3.ABKModel d) : ℝ

The subcritical Hölder exponent: half the shell exponent gamma.

Equations

• Algsuperdiff.Section5.Field.streamHolderExponent M = M.gamma / 2

theorem Algsuperdiff.Section5.Field.streamHolderExponent_pos {d : ℕ} (M : Section3.ABKModel d) : 0 < streamHolderExponent M

noncomputable def Algsuperdiff.Section5.Field.streamSharpConst {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : ℕ

A concrete sample constant for the sharp two-sided shell estimates.

Equations

• Algsuperdiff.Section5.Field.streamSharpConst M omega = Classical.choose ⋯

theorem Algsuperdiff.Section5.Field.streamSharpConst_spec {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : SharpTailBounded M.gamma (streamSharpConst M omega) ↑omega

noncomputable def Algsuperdiff.Section5.Field.holderLowerRatio {d : ℕ} (M : Section3.ABKModel d) : ℝ

The geometric ratio for the low-frequency part of the Hölder estimate.

Equations

• Algsuperdiff.Section5.Field.holderLowerRatio M = Real.rpow 3 (-M.gamma)

noncomputable def Algsuperdiff.Section5.Field.holderUpperRatio {d : ℕ} (M : Section3.ABKModel d) : ℝ

The geometric ratio for the high-frequency part of the Hölder estimate.

Equations

• Algsuperdiff.Section5.Field.holderUpperRatio M = Real.rpow 3 (M.gamma - 1)

noncomputable def Algsuperdiff.Section5.Field.holderGapRatio {d : ℕ} (M : Section3.ABKModel d) : ℝ

The geometric ratio determined by the stream Hölder exponent.

Equations

• Algsuperdiff.Section5.Field.holderGapRatio M = Real.rpow 3 (-Algsuperdiff.Section5.Field.streamHolderExponent M)

noncomputable def Algsuperdiff.Section5.Field.holderLowerSum {d : ℕ} (M : Section3.ABKModel d) : ℝ

The weighted geometric sum for the low-frequency Hölder bound.

Equations

• Algsuperdiff.Section5.Field.holderLowerSum M = ∑' (r : ℕ), (↑r + 1) * Algsuperdiff.Section5.Field.holderLowerRatio M ^ r

noncomputable def Algsuperdiff.Section5.Field.holderUpperSum {d : ℕ} (M : Section3.ABKModel d) : ℝ

The weighted geometric sum for the high-frequency Hölder bound.

Equations

• Algsuperdiff.Section5.Field.holderUpperSum M = ∑' (r : ℕ), (↑r + 1) * Algsuperdiff.Section5.Field.holderUpperRatio M ^ r

noncomputable def Algsuperdiff.Section5.Field.holderGapSum {d : ℕ} (M : Section3.ABKModel d) : ℝ

The weighted geometric sum for the Hölder-exponent gap bound.

Equations

• Algsuperdiff.Section5.Field.holderGapSum M = ∑' (r : ℕ), (↑r + 1) * Algsuperdiff.Section5.Field.holderGapRatio M ^ r

theorem Algsuperdiff.Section5.Field.norm_sub_le_of_mem_openOriginCube {d : ℕ} (ell : ℤ) (j : Frozen.Assumptions.ShellField d) {x y : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell)) (hy : y ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d ell)) : ‖(↑j).1 x - (↑j).1 y‖ ≤ ↑d * Section3.Provider.Stream.localCubeDerivNorm ell j * ‖x - y‖

The shell mean-value estimate between two points of the same origin cube.

noncomputable def Algsuperdiff.Section5.Field.streamFieldHolderConst {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : ℝ

An explicit radius-independent coefficient in the Hölder modulus.

Equations

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

noncomputable def Algsuperdiff.Section5.Field.streamFieldHolderModulus {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (R : ℝ) : ℝ

The radius-dependent modulus; its growth exponent is explicitly one.

Equations

• Algsuperdiff.Section5.Field.streamFieldHolderModulus M omega R = Algsuperdiff.Section5.Field.streamFieldHolderConst M omega * (1 + R)

theorem Algsuperdiff.Section5.Field.streamFieldHolderConst_nonneg {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : 0 ≤ streamFieldHolderConst M omega

theorem Algsuperdiff.Section5.Field.two_mul_dim_sq_mul_growthConst_le_holderConst {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : 2 * ↑d ^ 2 * streamFieldGrowthConst M omega ≤ streamFieldHolderConst M omega

theorem Algsuperdiff.Section5.Field.matrixOperatorNorm_streamField_sub_le_small {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) (hxy : x ≠ y) (hsmall : ‖x - y‖ < 1) : HCPolySupport.Book.Ch02.matrixOperatorNorm (streamField omega x - streamField omega y) ≤ streamFieldHolderModulus M omega R * ‖x - y‖.rpow (streamHolderExponent M)

The crossover estimate in the small-distance regime.