LocalizedInteriorEnergy #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Localized split-skew energy for bounded interior solutions #
The localization is supported inside the domain, so the solution may have nonzero trace. Both split-skew constants are read on an active set containing the topological support of the localization.
theorem
DivergenceFormProcess.Decay.weightedEnergy_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 zeta : HCPolySupport.Vec d → ℝ}
{L : Set (HCPolySupport.Vec d)}
{nu LamS Ks M : ℝ}
(hnu : 0 < nu)
(hKs : 0 ≤ Ks)
(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)
(hzeta : ContDiff ℝ (↑⊤) zeta)
(hzetaCompact : HasCompactSupport zeta)
(hzetaOm : tsupport zeta ⊆ Om)
(hzetaL : tsupport zeta ⊆ L)
(hksSize :
∀ y ∈ L,
∀ (v : HCPolySupport.Vec d),
HCPolySupport.vecNormSq (HCPolySupport.matVecMul (ks y) v) ≤ Ks ^ 2 * HCPolySupport.vecNormSq v)
:
((nu / 2 * ∫ (y : HCPolySupport.Vec d) in Om, zeta y ^ 2 * HCPolySupport.vecNormSq (u.grad y)) + 1 / 2 * ∫ (y : HCPolySupport.Vec d) in Om, u.toFun y ^ 2 * HCPolySupport.vecDot (skewFieldDiv kl y) fun (i : Fin d) =>
(fderiv ℝ (fun (z : HCPolySupport.Vec d) => zeta z ^ 2) y) (HCPolySupport.basisVec i)) ≤ (∫ (y : HCPolySupport.Vec d) in Om, g y * (zeta y ^ 2 * u.toFun y)) + 2 * (nu + Ks) ^ 2 / nu * ∫ (y : HCPolySupport.Vec d) in Om, u.toFun y ^ 2 * HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ zeta y) (HCPolySupport.basisVec i)
The split-skew weighted energy inequality for a bounded H¹ solution.
The smooth skew term is transferred using the compact support of the weight,
not a zero-trace property of the solution.