LocalizedTailData

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

Localized split-skew data for the whole-space exhaustion

This module records the structural inputs used by the localized Agmon tail. The coefficient is split as a = nu I + ks + kl: the rough skew part is bounded only on the ball about the evaluation point, while only the local divergence of the continuously differentiable skew part is bounded. The ambient upper ellipticity constant may depend on the exhaustion cube.

For the stream coefficient, the intended fields are supplied by Section5.Field.ScaleDecomposition, Section5.Field.LocalSplitBounds, and Section5.Field.FreezingRadius. No global small-contrast condition is part of this datum.

structure DivergenceFormProcess.Form.WholeSpaceLocalizedSplitData {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) : Type

Structural and quantitative local data for the arbitrary-size split-skew tail estimate. The local constants may grow with the centre and radius; the localized family theorem is uniform in the exhaustion index because these constants do not depend on that index.

• ks : HCPolySupport.CoeffField d

  The rough skew component of the whole-space coefficient split.

• kl : HCPolySupport.CoeffField d

  The differentiable skew component of the whole-space coefficient split.

• split (y : HCPolySupport.Vec d) : A.a y = A.nu • 1 + self.ks y + self.kl y
• ksSkew (y : HCPolySupport.Vec d) : HCPolySupport.matTranspose (self.ks y) = -self.ks y
• klSkew (y : HCPolySupport.Vec d) : HCPolySupport.matTranspose (self.kl y) = -self.kl y
• klContDiff (p q : Fin d) : ContDiff ℝ 1 fun (y : HCPolySupport.Vec d) => self.kl y p q
• roughEllipticityUpper : ℕ → ℝ

  The upper ellipticity bound for the rough component on each exhaustion cube.

• roughEllipticity (m : ℕ) : HCPolySupport.IsEllipticFieldOn A.nu (self.roughEllipticityUpper m) (wholeSpaceCube d m) fun (y : HCPolySupport.Vec d) => A.nu • 1 + self.ks y
• holderExponent : ℝ

  The Hölder exponent used in the local small-contrast estimate.

• holderExponent_mem : self.holderExponent ∈ Set.Ico (1 / 2) 1
• delta : ℝ

  The allowed deviation from the frozen identity coefficient.

• delta_nonneg : 0 ≤ self.delta
• delta_le : self.delta ≤ Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastThreshold d self.holderExponent
• freezingRadius : HCPolySupport.Vec d → ℝ

  The positive radius on which the normalized coefficient has small contrast.

• freezingRadius_pos (x : HCPolySupport.Vec d) : 0 < self.freezingRadius x
• smallContrast (x : HCPolySupport.Vec d) : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.CoefficientIdentityDistanceLE (HCPolySupport.euclideanBall x (self.freezingRadius x)) (Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.normalizedFrozenCoeff A.nu A.a x) self.delta
• roughBound : HCPolySupport.Vec d → ℝ → ℝ

  The local operator-norm bound for the rough skew component.

• smoothDivBound : HCPolySupport.Vec d → ℝ → ℝ

  The local divergence bound for the differentiable skew component.

• roughBound_nonneg (x : HCPolySupport.Vec d) (r : ℝ) : 0 ≤ r → 0 ≤ self.roughBound x r
• smoothDivBound_nonneg (x : HCPolySupport.Vec d) (r : ℝ) : 0 ≤ r → 0 ≤ self.smoothDivBound x r
• roughBound_spec (x : HCPolySupport.Vec d) (r : ℝ) : 0 ≤ r → ∀ y ∈ HCPolySupport.euclideanBall x r, ∀ (v : HCPolySupport.Vec d), HCPolySupport.vecNormSq (HCPolySupport.matVecMul (self.ks y) v) ≤ self.roughBound x r ^ 2 * HCPolySupport.vecNormSq v
• smoothDivBound_spec (x : HCPolySupport.Vec d) (r : ℝ) : 0 ≤ r → ∀ y ∈ HCPolySupport.euclideanBall x r, HCPolySupport.vecNormSq (Decay.skewFieldDiv self.kl y) ≤ self.smoothDivBound x r ^ 2

noncomputable def DivergenceFormProcess.Form.WholeSpaceLocalizedSplitData.clippedFreezingRadius {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (L : WholeSpaceLocalizedSplitData A) (x : HCPolySupport.Vec d) (r : ℝ) : ℝ

The freezing radius clipped to half the source-free radius.

Equations

• L.clippedFreezingRadius x r = min (L.freezingRadius x) (r / 2)

theorem DivergenceFormProcess.Form.WholeSpaceLocalizedSplitData.clippedFreezingRadius_pos {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (L : WholeSpaceLocalizedSplitData A) (x : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : 0 < L.clippedFreezingRadius x r

The clipped freezing radius is positive whenever the outer radius is.

theorem DivergenceFormProcess.Form.WholeSpaceLocalizedSplitData.clippedFreezingRadius_le_half {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (L : WholeSpaceLocalizedSplitData A) (x : HCPolySupport.Vec d) (r : ℝ) : L.clippedFreezingRadius x r ≤ r / 2

The clipped radius is admissible for the localized tail estimate.

theorem DivergenceFormProcess.Form.WholeSpaceLocalizedSplitData.smallContrast_clipped {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (L : WholeSpaceLocalizedSplitData A) (x : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.CoefficientIdentityDistanceLE (HCPolySupport.euclideanBall x (L.clippedFreezingRadius x r)) (Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.normalizedFrozenCoeff A.nu A.a x) L.delta

Small contrast persists after clipping the freezing ball.

noncomputable def DivergenceFormProcess.Form.WholeSpaceLocalizedSplitData.tail {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (L : WholeSpaceLocalizedSplitData A) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (x : HCPolySupport.Vec d) (r : ℝ) : ℝ

The explicit local two-scale tail for a centre and source-free radius.

Equations

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