FreezingRadius

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

A polynomial quantitative freezing radius for the stream coefficient

The subcritical Hölder modulus gives an explicit point-dependent ball on which subtracting the skew value at the centre and normalizing by nu produces a coefficient within delta of the identity. The radius is exactly a positive sample-dependent constant times (1 + |x|) ^ (-2 / gamma).

noncomputable def Algsuperdiff.Section5.Field.streamCoefficient {d : ℕ} {gamma : ℝ} (nu : ℝ) (omega : FullSample d gamma) : HCPolySupport.CoeffField d

The scalar-plus-stream coefficient.

Equations

• Algsuperdiff.Section5.Field.streamCoefficient nu omega x = nu • 1 + Algsuperdiff.Section5.Field.streamField omega x

theorem Algsuperdiff.Section5.Field.continuous_streamCoefficient {d : ℕ} {gamma : ℝ} (nu : ℝ) (omega : FullSample d gamma) : Continuous (streamCoefficient nu omega)

The scalar-plus-stream coefficient is continuous.

theorem Algsuperdiff.Section5.Field.symmPart_streamCoefficient {d : ℕ} {gamma : ℝ} (nu : ℝ) (omega : FullSample d gamma) (x : HCPolySupport.Vec d) : HCPolySupport.symmPart (streamCoefficient nu omega x) = nu • 1

The symmetric part of the scalar-plus-stream coefficient is nu I.

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

The reciprocal Hölder exponent governing the freezing radius.

Equations

• Algsuperdiff.Section5.Field.streamFreezingExponent M = (Algsuperdiff.Section5.Field.streamHolderExponent M)⁻¹

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

The dimensionless amplitude in the explicit freezing radius.

Equations

• Algsuperdiff.Section5.Field.streamFreezingAmplitude M omega nu delta = min 1 (delta * nu / (1 + 3 * Algsuperdiff.Section5.Field.streamFieldHolderConst M omega))

noncomputable def Algsuperdiff.Section5.Field.streamFreezingRadius {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (nu delta : ℝ) (x : HCPolySupport.Vec d) : ℝ

An explicit radius on which the coefficient frozen at x has contrast at most delta.

Equations

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

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

theorem Algsuperdiff.Section5.Field.streamFreezingAmplitude_pos {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {nu delta : ℝ} (hnu : 0 < nu) (hdelta : 0 < delta) : 0 < streamFreezingAmplitude M omega nu delta

theorem Algsuperdiff.Section5.Field.streamFreezingAmplitude_le_one {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (nu delta : ℝ) : streamFreezingAmplitude M omega nu delta ≤ 1

theorem Algsuperdiff.Section5.Field.streamFreezingRadius_pos {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {nu delta : ℝ} (hnu : 0 < nu) (hdelta : 0 < delta) (x : HCPolySupport.Vec d) : 0 < streamFreezingRadius M omega nu delta x

theorem Algsuperdiff.Section5.Field.streamFreezingRadius_le_one {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {nu delta : ℝ} (hnu : 0 < nu) (hdelta : 0 < delta) (x : HCPolySupport.Vec d) : streamFreezingRadius M omega nu delta x ≤ 1

theorem Algsuperdiff.Section5.Field.streamFreezingRadius_eq_polynomial {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {nu delta : ℝ} (hnu : 0 < nu) (hdelta : 0 < delta) (x : HCPolySupport.Vec d) : streamFreezingRadius M omega nu delta x = (streamFreezingAmplitude M omega nu delta).rpow (streamFreezingExponent M) * (1 + HCPolySupport.euclideanNorm x).rpow (-streamFreezingExponent M)

theorem Algsuperdiff.Section5.Field.coefficientIdentityDistanceLE_streamCoefficient {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {nu delta : ℝ} (hnu : 0 < nu) (hdelta : 0 < delta) (x : HCPolySupport.Vec d) : StochasticProcess.Common.Regularity.Ported.CoefficientIdentityDistanceLE (HCPolySupport.euclideanBall x (streamFreezingRadius M omega nu delta x)) (StochasticProcess.Common.Regularity.Freezing.normalizedFrozenCoeff nu (streamCoefficient nu omega) x) delta

The explicit radius gives the small normalized coefficient contrast needed by the freezing argument.