LocalizedInteriorMass

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

Localized Agmon mass estimate for bounded H¹ solutions

The compactly supported multiplier lies strictly inside the domain. Thus the weighted argument applies to an arbitrary H1Function; no trace condition on the solution is used. The rough size and smooth divergence are read only on the topological support of the localization.

theorem DivergenceFormProcess.Decay.agmonMass_split_interior_le {d : ℕ} {Om : Set (HCPolySupport.Vec d)} (hOm : HCPolySupport.IsOpenBoundedConvexDomain Om) {a : HCPolySupport.CoeffField d} {ks kl : HCPolySupport.Vec d → HCPolySupport.Mat d} {u : HCPolySupport.H1Function Om} {g eta psi : HCPolySupport.Vec d → ℝ} {L : Set (HCPolySupport.Vec d)} {nu LamS Ks Kl mass kappa M : ℝ} (hnu : 0 < nu) (hKs : 0 ≤ Ks) (hmass : 0 < mass) (hM : 0 ≤ M) (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 g 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) (hpsi : ContDiff ℝ (↑⊤) psi) (hpsiGrad : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn Om, (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ psi y) (HCPolySupport.basisVec i)) ≤ 1) (hg : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn Om, eta y ≠ 0 → g y * u.toFun y ≤ -(mass * u.toFun y ^ 2)) (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) (hadmiss : (4 * (nu + Ks) ^ 2 / nu + 4 * Kl ^ 2 / mass) * kappa ^ 2 ≤ 3 * mass / 8) : mass / 2 * ∫ (y : HCPolySupport.Vec d) in Om, u.toFun y ^ 2 * (eta y ^ 2 * Real.exp (kappa * psi y) ^ 2) ≤ (4 * (nu + Ks) ^ 2 / nu + 4 * Kl ^ 2 / mass) * ∫ (y : HCPolySupport.Vec d) in Om, u.toFun y ^ 2 * (Real.exp (kappa * psi y) ^ 2 * HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ eta y) (HCPolySupport.basisVec i))

The split-skew Agmon mass estimate for an H¹ solution, using an interior compactly supported multiplier.

theorem DivergenceFormProcess.Decay.agmonMass_localizedSplit_interior_le {d : ℕ} {Om : Set (HCPolySupport.Vec d)} (hOm : HCPolySupport.IsOpenBoundedConvexDomain Om) {a : HCPolySupport.CoeffField d} {ks kl : HCPolySupport.Vec d → HCPolySupport.Mat d} {u : HCPolySupport.H1Function Om} {g eta psi : HCPolySupport.Vec d → ℝ} {L : Set (HCPolySupport.Vec d)} {nu LamS Ks Kl mass kappa M : ℝ} (hnu : 0 < nu) (hKs : 0 ≤ Ks) (hKl : 0 ≤ Kl) (hmass : 0 < mass) (hM : 0 ≤ M) (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 g 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) (hpsi : ContDiff ℝ (↑⊤) psi) (hpsiGrad : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn Om, (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ psi y) (HCPolySupport.basisVec i)) ≤ 1) (hg : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn Om, eta y ≠ 0 → g y * u.toFun y ≤ -(mass * u.toFun y ^ 2)) (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) (hkappa : 8 * localizedAgmonUpper nu mass Ks Kl ^ 2 * kappa ^ 2 ≤ nu * mass) : mass / 2 * ∫ (y : HCPolySupport.Vec d) in Om, u.toFun y ^ 2 * (eta y ^ 2 * Real.exp (kappa * psi y) ^ 2) ≤ 4 * localizedAgmonUpper nu mass Ks Kl ^ 2 / nu * ∫ (y : HCPolySupport.Vec d) in Om, u.toFun y ^ 2 * (Real.exp (kappa * psi y) ^ 2 * HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ eta y) (HCPolySupport.basisVec i))

The H¹ interior mass estimate at the effective localized upper constant.

The sharp zero-divergence branch

noncomputable def DivergenceFormProcess.Decay.localizedInteriorUpper (nu mass Ks Kl : ℝ) : ℝ

Effective upper constant for the interior estimate. When the smooth part has zero divergence bound, its transferred contribution vanishes and the sharp rough-only constant nu + Ks is retained.

Equations

• DivergenceFormProcess.Decay.localizedInteriorUpper nu mass Ks Kl = if Kl = 0 then nu + Ks else DivergenceFormProcess.Decay.localizedAgmonUpper nu mass Ks Kl

theorem DivergenceFormProcess.Decay.localizedInteriorUpper_pos {nu mass Ks Kl : ℝ} (hnu : 0 < nu) (hKs : 0 ≤ Ks) (hKl : 0 ≤ Kl) : 0 < localizedInteriorUpper nu mass Ks Kl

theorem DivergenceFormProcess.Decay.agmonMass_localizedInterior_le {d : ℕ} {Om : Set (HCPolySupport.Vec d)} (hOm : HCPolySupport.IsOpenBoundedConvexDomain Om) {a : HCPolySupport.CoeffField d} {ks kl : HCPolySupport.Vec d → HCPolySupport.Mat d} {u : HCPolySupport.H1Function Om} {g eta psi : HCPolySupport.Vec d → ℝ} {L : Set (HCPolySupport.Vec d)} {nu LamS Ks Kl mass kappa M : ℝ} (hnu : 0 < nu) (hKs : 0 ≤ Ks) (hKl : 0 ≤ Kl) (hmass : 0 < mass) (hM : 0 ≤ M) (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 g 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) (hpsi : ContDiff ℝ (↑⊤) psi) (hpsiGrad : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn Om, (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ psi y) (HCPolySupport.basisVec i)) ≤ 1) (hg : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn Om, eta y ≠ 0 → g y * u.toFun y ≤ -(mass * u.toFun y ^ 2)) (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) (hkappa : 8 * localizedInteriorUpper nu mass Ks Kl ^ 2 * kappa ^ 2 ≤ nu * mass) : mass / 2 * ∫ (y : HCPolySupport.Vec d) in Om, u.toFun y ^ 2 * (eta y ^ 2 * Real.exp (kappa * psi y) ^ 2) ≤ 4 * localizedInteriorUpper nu mass Ks Kl ^ 2 / nu * ∫ (y : HCPolySupport.Vec d) in Om, u.toFun y ^ 2 * (Real.exp (kappa * psi y) ^ 2 * HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ eta y) (HCPolySupport.basisVec i))

The interior mass estimate at the sharp branched upper constant.