LocalizedTailEnvelope

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

Spatial envelopes for the localized stream-field tail constants

The local field bounds are logarithmic in the Euclidean observation radius. This file converts them to the ambient Vec d norm and combines them with the polynomial freezing radius. The resulting amplitude has polynomial growth, while the decay rate loses one logarithmic weight.

def Algsuperdiff.Section5.Field.streamTailDimensionFactor (d : ℕ) : ℝ

A dimension factor comparing the Euclidean and ambient norms.

Equations

• Algsuperdiff.Section5.Field.streamTailDimensionFactor d = 1 + ↑d

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

The effective upper constant before the spatial logarithmic weight.

Equations

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

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

The effective upper constant enlarged by the norm-comparison logarithm.

Equations

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

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

The spatially uniform part of the polynomial freezing-radius lower bound.

Equations

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

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

The coefficient multiplying the effective upper constant in the two non-forcing terms of the tail amplitude.

Equations

• Algsuperdiff.Section5.Field.streamTailLinearConst M = DivergenceFormProcess.Decay.agmonTailL2Coefficient d M.nu 1 + DivergenceFormProcess.Decay.agmonTailGradientCoefficient d M.nu 1 (1 / 2)

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

The polynomial exponent contributed by one logarithmic field factor and the d-dimensional inverse freezing volume.

Equations

• Algsuperdiff.Section5.Field.streamTailAmplitudeExponent M = 1 + ↑d * Algsuperdiff.Section5.Field.streamFreezingExponent M

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

A point-independent polynomial envelope constant for the tail amplitude.

Equations

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

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

A point-independent numerator for the logarithmic lower envelope on the decay rate.

Equations

• Algsuperdiff.Section5.Field.streamTailDecayConst M omega = DivergenceFormProcess.Decay.agmonTailRate d M.nu (Algsuperdiff.Section5.Field.streamTailUpperConst M omega) (1 / 2)

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

The polynomial envelope amplitude is nonnegative.

theorem Algsuperdiff.Section5.Field.streamTailDecayConst_pos {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : 0 < streamTailDecayConst M omega

The logarithmic envelope decay numerator is strictly positive.

theorem Algsuperdiff.Section5.Field.streamTailAlgebraicAmplitude_le {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (x : HCPolySupport.Vec d) : streamTailAlgebraicAmplitude M omega x ≤ streamTailAmplitudeConst M omega * (1 + ‖x‖) ^ streamTailAmplitudeExponent M

A polynomial envelope for the per-point algebraic amplitude.

theorem Algsuperdiff.Section5.Field.streamTailDecayRate_ge {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (x : HCPolySupport.Vec d) : streamTailDecayConst M omega / (1 + Real.log (1 + ‖x‖)) ≤ streamTailDecayRate M omega x

A logarithmic envelope for the per-point decay rate.