LocalizedInteriorPointwise

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

Frozen pointwise decay for bounded interior solutions

The weighted half reads the skew constants only on tsupport eta. The pointwise half freezes the coefficient on a separate small ball about the evaluation point.

noncomputable def DivergenceFormProcess.Decay.localizedInteriorDecayConstant (d : ℕ) (nu mass Ks Kl M Ceta volLayer alpha E r₀ : ℝ) : ℝ

Explicit constant in the localized interior pointwise estimate.

Equations

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

theorem DivergenceFormProcess.Decay.interior_abs_center_le_exp_localized {d : ℕ} [NeZero d] {a : HCPolySupport.CoeffField d} {ks kl : HCPolySupport.Vec d → HCPolySupport.Mat d} {Om : Set (HCPolySupport.Vec d)} (hOm : HCPolySupport.IsOpenBoundedConvexDomain Om) {u : HCPolySupport.H1Function Om} {eta psi : HCPolySupport.Vec d → ℝ} {L : Set (HCPolySupport.Vec d)} {nu LamS Ks Kl mass M Ceta volLayer delta alpha tA tx E : ℝ} (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) (hmass : 0 < mass) (hM : 0 ≤ M) (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) => -(mass * u.toFun y)) u) (hMbound : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn Om, |u.toFun y| ≤ M) (heta : ContDiff ℝ (↑⊤) eta) (hetaCompact : HasCompactSupport eta) (hetaOm : tsupport eta ⊆ Om) (hetaL : tsupport eta ⊆ L) (hCeta : 0 ≤ Ceta) (hetaGrad : ∀ y ∈ Om, (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ eta y) (HCPolySupport.basisVec i)) ≤ Ceta) (hlayer : ∀ y ∈ Om, fderiv ℝ eta y ≠ 0 → psi y ≤ tA) (hvolLayer : (MeasureTheory.volume {y : HCPolySupport.Vec d | y ∈ Om ∧ fderiv ℝ eta y ≠ 0}).toReal ≤ volLayer) (hpsi : ContDiff ℝ (↑⊤) psi) (hpsiGrad : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn Om, (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ psi y) (HCPolySupport.basisVec i)) ≤ 1) (hksSize : ∀ y ∈ L, ∀ (v : HCPolySupport.Vec d), HCPolySupport.vecNormSq (HCPolySupport.matVecMul (ks y) v) ≤ Ks ^ 2 * HCPolySupport.vecNormSq v) (hklDiv : ∀ y ∈ L, HCPolySupport.vecNormSq (skewFieldDiv kl y) ≤ Kl ^ 2) {x : HCPolySupport.Vec d} {r₀ : ℝ} (hr₀ : 0 < r₀) (hball : HCPolySupport.euclideanBall x r₀ ⊆ Om) (hsmall : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.CoefficientIdentityDistanceLE (HCPolySupport.euclideanBall x r₀) (Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.normalizedFrozenCoeff nu a x) delta) (hE : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorLpSizeOn (HCPolySupport.euclideanBall x r₀) 2 u.grad ≤ E) (hinner : ∀ y ∈ HCPolySupport.euclideanBall x (r₀ / 2), eta y = 1) (hphase : ∀ y ∈ HCPolySupport.euclideanBall x (r₀ / 2), tx ≤ psi y) (hlayerLe : tA ≤ tx) : ∃ (v : HCPolySupport.Vec d → ℝ), ContinuousOn v (HCPolySupport.euclideanBall x (r₀ / 2)) ∧ v =ᵐ[MeasureTheory.volume.restrict (HCPolySupport.euclideanBall x r₀)] u.toFun ∧ |v x| ≤ localizedInteriorDecayConstant d nu mass Ks Kl M Ceta volLayer alpha E r₀ * Real.exp (-(agmonRate nu (localizedInteriorUpper nu mass Ks Kl) mass * alpha / (alpha + ↑d / 2) * (tx - tA)))

Frozen pointwise decay of a bounded homogeneous H¹ solution. The rough size and smooth divergence are required only on an active set containing the topological support of the localization.