LocalizedTailFreezing

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

The resolvent tail with layer constants

The tail estimate is re-run with the coefficient split as a = nu • I + ks + kl, with ks merely bounded and kl continuously differentiable and antisymmetric. Every constant of the conclusion is read off the ball euclideanBall x r about the evaluation point: the size of ks and the size of the divergence of kl there. Uniform ellipticity on the whole domain enters only qualitatively, through the square integrability of the flux, and its upper constant never appears in the conclusion.

The two halves of the chain are the localized ones: the exponentially weighted mass estimate and the Caccioppoli gradient bound, both at the effective upper constant localizedAgmonUpper nu mu Ks Kl. The pointwise half is unchanged: it is applied to the normalized coefficient frozen at x on the ball of radius r₀, on which small contrast is assumed.

Main results

• DivergenceFormProcess.Decay.vectorLpSizeOn_grad_le_agmonTailGradientSize_localized
• DivergenceFormProcess.Decay.resolventTail_localized
• DivergenceFormProcess.Decay.resolventTail_localized_representative

Elementary restatements

theorem DivergenceFormProcess.Decay.symmPart_eq_of_splitSkew {d : ℕ} {nu : ℝ} {A K1 K2 : HCPolySupport.Mat d} (hA : A = nu • 1 + K1 + K2) (hK1 : HCPolySupport.matTranspose K1 = -K1) (hK2 : HCPolySupport.matTranspose K2 = -K2) : HCPolySupport.symmPart A = nu • 1

The symmetric part of a coefficient split as a scalar plus two antisymmetric parts.

The localized gradient size

theorem DivergenceFormProcess.Decay.vectorLpSizeOn_grad_le_agmonTailGradientSize_localized {d : ℕ} [NeZero d] {a : HCPolySupport.CoeffField d} {ks kl : HCPolySupport.Vec d → HCPolySupport.Mat d} {Om : Set (HCPolySupport.Vec d)} (hOmOpen : IsOpen Om) (hOmBdd : HCPolySupport.IsBoundedDomain Om) {z : HCPolySupport.H10Function Om} {g : HCPolySupport.Vec d → ℝ} {nu LamS Ks Kl mu : ℝ} (hnu : 0 < nu) (hKs : 0 ≤ Ks) (hKl : 0 ≤ Kl) (hmu : 0 < mu) (hEllS : HCPolySupport.IsEllipticFieldOn nu LamS Om fun (y : HCPolySupport.Vec d) => nu • 1 + ks y) (hsplit : ∀ (y : HCPolySupport.Vec d), a y = nu • 1 + ks y + kl y) (hksSkew : ∀ (y : HCPolySupport.Vec d), HCPolySupport.matTranspose (ks y) = -ks y) (hklSkew : ∀ (y : HCPolySupport.Vec d), HCPolySupport.matTranspose (kl y) = -kl y) (hklC1 : ∀ (p q : Fin d), ContDiff ℝ 1 fun (y : HCPolySupport.Vec d) => kl y p q) (hsol : Form.IsScalarForcedWeakSolution a Om (fun (y : HCPolySupport.Vec d) => g y - mu * z.toFun y) z.toH1Function) (hMbound : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn Om, |z.toFun y| ≤ 1 / mu) {x : HCPolySupport.Vec d} {r : ℝ} (hr : 0 < r) (hball : HCPolySupport.euclideanBall x r ⊆ Om) (hksSize : ∀ y ∈ HCPolySupport.euclideanBall x r, ∀ (v : HCPolySupport.Vec d), HCPolySupport.vecNormSq (HCPolySupport.matVecMul (ks y) v) ≤ Ks ^ 2 * HCPolySupport.vecNormSq v) (hklDiv : ∀ y ∈ HCPolySupport.euclideanBall x r, HCPolySupport.vecNormSq (skewFieldDiv kl y) ≤ Kl ^ 2) (hg : ∀ᵐ (y : HCPolySupport.Vec d), y ∈ HCPolySupport.euclideanBall x r → g y = 0) : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorLpSizeOn (HCPolySupport.euclideanBall x (r / 2)) 2 z.grad ≤ agmonTailGradientSize d nu (localizedAgmonUpper nu mu Ks Kl) mu r

The Caccioppoli gradient size with layer constants. The gradient size consumed by the interior estimate is the one of the uniformly elliptic chain, with lower constant nu and upper constant the effective one read off the ball about the evaluation point.

The localized tail estimate

theorem DivergenceFormProcess.Decay.resolventTail_localized {d : ℕ} [NeZero d] {a : HCPolySupport.CoeffField d} {ks kl : HCPolySupport.Vec d → HCPolySupport.Mat d} {Om : Set (HCPolySupport.Vec d)} (hOmOpen : IsOpen Om) (hOmBdd : HCPolySupport.IsBoundedDomain Om) {z : HCPolySupport.H10Function Om} {g : HCPolySupport.Vec d → ℝ} {nu LamS Ks Kl mu delta alpha : ℝ} (hd : 2 ≤ d) (halpha : alpha ∈ Set.Ico (1 / 2) 1) (hdelta0 : 0 ≤ delta) (hdelta : delta ≤ Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastThreshold d alpha) (hnu : 0 < nu) (hKs : 0 ≤ Ks) (hKl : 0 ≤ Kl) (hmu : 0 < mu) (hameas : Measurable a) (hEllS : HCPolySupport.IsEllipticFieldOn nu LamS Om fun (y : HCPolySupport.Vec d) => nu • 1 + ks y) (hsplit : ∀ (y : HCPolySupport.Vec d), a y = nu • 1 + ks y + kl y) (hksSkew : ∀ (y : HCPolySupport.Vec d), HCPolySupport.matTranspose (ks y) = -ks y) (hklSkew : ∀ (y : HCPolySupport.Vec d), HCPolySupport.matTranspose (kl y) = -kl y) (hklC1 : ∀ (p q : Fin d), ContDiff ℝ 1 fun (y : HCPolySupport.Vec d) => kl y p q) (hsol : Form.IsScalarForcedWeakSolution a Om (fun (y : HCPolySupport.Vec d) => g y - mu * z.toFun y) z.toH1Function) (hMbound : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn Om, |z.toFun y| ≤ 1 / mu) {x : HCPolySupport.Vec d} {r r₀ : ℝ} (hr : 0 < r) (hr₀ : 0 < r₀) (hr₀r : r₀ ≤ r / 2) (hball : HCPolySupport.euclideanBall x r ⊆ Om) (hksSize : ∀ y ∈ HCPolySupport.euclideanBall x r, ∀ (v : HCPolySupport.Vec d), HCPolySupport.vecNormSq (HCPolySupport.matVecMul (ks y) v) ≤ Ks ^ 2 * HCPolySupport.vecNormSq v) (hklDiv : ∀ y ∈ HCPolySupport.euclideanBall x r, HCPolySupport.vecNormSq (skewFieldDiv kl y) ≤ Kl ^ 2) (hsmall : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.CoefficientIdentityDistanceLE (HCPolySupport.euclideanBall x r₀) (Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.normalizedFrozenCoeff nu a x) delta) (hg : ∀ᵐ (y : HCPolySupport.Vec d), y ∈ HCPolySupport.euclideanBall x r → g y = 0) : ∃ (v : HCPolySupport.Vec d → ℝ), ContinuousOn v (HCPolySupport.euclideanBall x (r₀ / 2)) ∧ v =ᵐ[MeasureTheory.volume.restrict (HCPolySupport.euclideanBall x r₀)] z.toFun ∧ mu * |v x| ≤ agmonTailFunctionFrozen d nu (localizedAgmonUpper nu mu Ks Kl) nu alpha (√mu * r) (√mu * r₀)

The resolvent tail with layer constants. For a coefficient split as nu • I + ks + kl with both parts antisymmetric and kl continuously differentiable, the tail of the resolvent at x is bounded by the two-scale tail function at lower constant nu and upper constant localizedAgmonUpper nu mu Ks Kl, whose ingredients are the size of ks and the size of the divergence of kl on the ball euclideanBall x r alone. The ambient ellipticity constant LamS does not appear in the conclusion.

Representatives and families

theorem DivergenceFormProcess.Decay.resolventTail_localized_representative {d : ℕ} [NeZero d] {a : HCPolySupport.CoeffField d} {ks kl : HCPolySupport.Vec d → HCPolySupport.Mat d} {Om : Set (HCPolySupport.Vec d)} (hOmOpen : IsOpen Om) (hOmBdd : HCPolySupport.IsBoundedDomain Om) {z : HCPolySupport.H10Function Om} {g zRep : HCPolySupport.Vec d → ℝ} {nu LamS Ks Kl mu delta alpha : ℝ} (hd : 2 ≤ d) (halpha : alpha ∈ Set.Ico (1 / 2) 1) (hdelta0 : 0 ≤ delta) (hdelta : delta ≤ Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastThreshold d alpha) (hnu : 0 < nu) (hKs : 0 ≤ Ks) (hKl : 0 ≤ Kl) (hmu : 0 < mu) (hameas : Measurable a) (hEllS : HCPolySupport.IsEllipticFieldOn nu LamS Om fun (y : HCPolySupport.Vec d) => nu • 1 + ks y) (hsplit : ∀ (y : HCPolySupport.Vec d), a y = nu • 1 + ks y + kl y) (hksSkew : ∀ (y : HCPolySupport.Vec d), HCPolySupport.matTranspose (ks y) = -ks y) (hklSkew : ∀ (y : HCPolySupport.Vec d), HCPolySupport.matTranspose (kl y) = -kl y) (hklC1 : ∀ (p q : Fin d), ContDiff ℝ 1 fun (y : HCPolySupport.Vec d) => kl y p q) (hsol : Form.IsScalarForcedWeakSolution a Om (fun (y : HCPolySupport.Vec d) => g y - mu * z.toFun y) z.toH1Function) (hMbound : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn Om, |z.toFun y| ≤ 1 / mu) {x : HCPolySupport.Vec d} {r r₀ : ℝ} (hr : 0 < r) (hr₀ : 0 < r₀) (hr₀r : r₀ ≤ r / 2) (hball : HCPolySupport.euclideanBall x r ⊆ Om) (hksSize : ∀ y ∈ HCPolySupport.euclideanBall x r, ∀ (v : HCPolySupport.Vec d), HCPolySupport.vecNormSq (HCPolySupport.matVecMul (ks y) v) ≤ Ks ^ 2 * HCPolySupport.vecNormSq v) (hklDiv : ∀ y ∈ HCPolySupport.euclideanBall x r, HCPolySupport.vecNormSq (skewFieldDiv kl y) ≤ Kl ^ 2) (hsmall : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.CoefficientIdentityDistanceLE (HCPolySupport.euclideanBall x r₀) (Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.normalizedFrozenCoeff nu a x) delta) (hg : ∀ᵐ (y : HCPolySupport.Vec d), y ∈ HCPolySupport.euclideanBall x r → g y = 0) (hRepCont : ContinuousOn zRep (HCPolySupport.euclideanBall x (r₀ / 2))) (hRepAe : zRep =ᵐ[MeasureTheory.volume.restrict (HCPolySupport.euclideanBall x (r₀ / 2))] z.toFun) : mu * |zRep x| ≤ agmonTailFunctionFrozen d nu (localizedAgmonUpper nu mu Ks Kl) nu alpha (√mu * r) (√mu * r₀)

The localized tail bound read on a fixed continuous representative near the evaluation point.

Exponential domination