LocalizedTailData

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

Localized whole-space tail data for the stream field

This module packages the sharp-carrier scale decomposition as the analytic split used by the localized Agmon estimate. The negative shells form the rough skew field and the nonnegative shells form the continuously differentiable skew field. Their quantitative hypotheses are the logarithmic ball bounds from LocalSplitBounds.

noncomputable def Algsuperdiff.Section5.Field.streamWholeSpaceAnalyticData {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : DivergenceFormProcess.Form.WholeSpaceAnalyticData d

The whole-space analytic coefficient furnished by one full stream-field sample.

Equations

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

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

The rough coefficient consisting of molecular diffusion and the negative shells.

Equations

• Algsuperdiff.Section5.Field.streamRoughCoefficient M omega x = M.nu • 1 + Algsuperdiff.Section5.Field.streamFieldSmall omega x

theorem Algsuperdiff.Section5.Field.symmPart_streamRoughCoefficient {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (x : HCPolySupport.Vec d) : HCPolySupport.symmPart (streamRoughCoefficient M omega x) = M.nu • 1

theorem Algsuperdiff.Section5.Field.continuous_streamRoughSkew {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : Continuous fun (x : HCPolySupport.Vec d) => streamRoughCoefficient M omega x - M.nu • 1

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

A compactness-supplied upper ellipticity constant for the rough coefficient on one exhaustion cube. It is qualitative only and does not enter the localized tail bound.

Equations

• Algsuperdiff.Section5.Field.streamRoughEllipticityUpper M omega m = Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.axisCubeEllipticUpper (fun (x : Fin d) => -3 ^ m) (2 * 3 ^ m) ⋯ ⋯ ⋯

theorem Algsuperdiff.Section5.Field.streamRoughEllipticity {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (m : ℕ) : HCPolySupport.IsEllipticFieldOn M.nu (streamRoughEllipticityUpper M omega m) (DivergenceFormProcess.Form.wholeSpaceCube d m) (streamRoughCoefficient M omega)

noncomputable def Algsuperdiff.Section5.Field.streamLocalizedTailDelta (d : ℕ) : ℝ

The fixed perturbative threshold used only after freezing.

Equations

• Algsuperdiff.Section5.Field.streamLocalizedTailDelta d = Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastThreshold d (1 / 2)

theorem Algsuperdiff.Section5.Field.streamLocalizedTailDelta_pos (d : ℕ) : 0 < streamLocalizedTailDelta d

noncomputable def Algsuperdiff.Section5.Field.streamLocalizedSplitData {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : DivergenceFormProcess.Form.WholeSpaceLocalizedSplitData (streamWholeSpaceAnalyticData M omega)

The stream field supplies every structural and local quantitative input of the split-skew tail estimate.

Equations

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