LocalizedConservativity

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

Localized split-skew decay of the whole-space boundary defect

The boundary defect on the mth exhaustion cube is a bounded homogeneous H¹ solution. The rough skew size and the smooth skew divergence are read on the full topological support of the cutoff. For the cubic cutoff that support lies in the origin-centred ball of radius 3^m.

This module carries the split datum explicitly. It assumes no global small-contrast or global upper-ellipticity bound.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_analyticCubeBoundaryRemainder_le_localized {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (L : WholeSpaceLocalizedSplitData A) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (m : ℕ) (x : HCPolySupport.Vec d) (hball : HCPolySupport.euclideanBall x (L.freezingRadius x) ⊆ wholeSpaceCube d m) (hinnerBall : HCPolySupport.euclideanBall x (L.freezingRadius x / 2) ⊆ HCPolySupport.euclideanBall 0 (cubeBoundaryCutoffInnerRadius m)) (hlayerLe : -cubeBoundaryCutoffInnerRadius m + 1 ≤ -(HCPolySupport.euclideanNorm (x - 0) + L.freezingRadius x / 2)) : |1 - ↑mu * A.analyticCubeResolvent mu (fun (x : HCPolySupport.Vec d) => 1) ⋯ ⋯ m x| ≤ Decay.localizedInteriorDecayConstant d A.nu (↑mu) (L.roughBound 0 (3 ^ m)) (L.smoothDivBound 0 (3 ^ m)) 1 cubeBoundaryCutoffUniformGradientBudget (MeasureTheory.volume (wholeSpaceCube d m)).toReal L.holderExponent (↑mu * (min (↑mu) A.nu)⁻¹ * (MeasureTheory.volume (wholeSpaceCube d m)).toReal) (L.freezingRadius x) * Real.exp (-(Decay.agmonRate A.nu (Decay.localizedInteriorUpper A.nu (↑mu) (L.roughBound 0 (3 ^ m)) (L.smoothDivBound 0 (3 ^ m))) ↑mu * L.holderExponent / (L.holderExponent + ↑d / 2) * (-(HCPolySupport.euclideanNorm (x - 0) + L.freezingRadius x / 2) - (-cubeBoundaryCutoffInnerRadius m + 1))))

The explicit localized split-skew upper bound for the boundary defect. All structural assumptions are carried by A and L; the three displayed geometric hypotheses merely place the fixed freezing ball inside the cube and separate it from the cutoff transition.