LocalizedWeightedEnergy

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

The weighted energy inequality with layer constants

The weighted energy estimate is restated so that the size of the coefficient enters only on the transition layer of the weight. Two structural facts make this possible.

• The symmetric part of the coefficient is the fixed scalar nu • I, so the elliptic energy is exactly nu times the squared gradient at every point of the domain. No upper size constant is used there.
• The coefficient enters everywhere else only through the flux cross term ⟨a grad u, grad zeta⟩, whose second factor is supported on the layer {grad zeta ≠ 0}. The Young inequality is therefore applied with a size constant that the caller supplies on that layer alone.

The resulting statements take exactly the form of the uniformly elliptic ones with lower constant nu and with the upper constant replaced by the layer size C; the ellipticity hypothesis on the whole domain survives only qualitatively, to know that the flux is square integrable, and its upper constant never enters a conclusion.

Main results

• DivergenceFormProcess.Decay.weightedEnergy_localized_le
• DivergenceFormProcess.Decay.weightedMass_le_of_energy
• DivergenceFormProcess.Decay.integral_sq_mul_gradSq_product_le
• DivergenceFormProcess.Decay.localizedMass_absorb

The layer form of the weighted energy inequality

theorem DivergenceFormProcess.Decay.weightedEnergy_localized_le {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {g zeta : HCPolySupport.Vec d → ℝ} {u : HCPolySupport.H1Function U} {kk : HCPolySupport.Vec d → HCPolySupport.Mat d} {nu Lam C : ℝ} (hnu : 0 < nu) (hC : 0 < C) (hEll : HCPolySupport.IsEllipticFieldOn nu Lam U a) (hsplit : ∀ (y : HCPolySupport.Vec d), a y = nu • 1 + kk y) (hskew : ∀ (y : HCPolySupport.Vec d), HCPolySupport.matTranspose (kk y) = -kk y) (hsol : Form.IsScalarForcedWeakSolution a U g u) (hzeta : ContDiff ℝ (↑⊤) zeta) (hzetaCompact : HasCompactSupport zeta) (hadm : IsAdmissibleMultiplier U u fun (x : HCPolySupport.Vec d) => zeta x ^ 2) (hlayer : ∀ y ∈ U, fderiv ℝ zeta y ≠ 0 → ∀ (v : HCPolySupport.Vec d), HCPolySupport.vecNormSq (HCPolySupport.matVecMul (a y) v) ≤ C ^ 2 * HCPolySupport.vecNormSq v) : nu / 2 * ∫ (x : HCPolySupport.Vec d) in U, zeta x ^ 2 * HCPolySupport.vecNormSq (u.grad x) ≤ (∫ (x : HCPolySupport.Vec d) in U, g x * (zeta x ^ 2 * u.toFun x)) + 2 * C ^ 2 / nu * ∫ (x : HCPolySupport.Vec d) in U, u.toFun x ^ 2 * HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ zeta x) (HCPolySupport.basisVec i)

The weighted energy inequality with a layer size constant. The coefficient has scalar symmetric part nu • I, so the elliptic energy is exactly nu times the squared gradient; the size constant C is required only where the weight gradient does not vanish.

The mass form

theorem DivergenceFormProcess.Decay.weightedMass_le_of_energy {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {g zeta : HCPolySupport.Vec d → ℝ} {u : HCPolySupport.H1Function U} {lam mass T : ℝ} (hlam : 0 < lam) (hsol : Form.IsScalarForcedWeakSolution a U g u) (hadm : IsAdmissibleMultiplier U u fun (x : HCPolySupport.Vec d) => zeta x ^ 2) (hg : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, zeta x ≠ 0 → g x * u.toFun x ≤ -(mass * u.toFun x ^ 2)) (henergy : lam / 2 * ∫ (x : HCPolySupport.Vec d) in U, zeta x ^ 2 * HCPolySupport.vecNormSq (u.grad x) ≤ (∫ (x : HCPolySupport.Vec d) in U, g x * (zeta x ^ 2 * u.toFun x)) + T) : mass * ∫ (x : HCPolySupport.Vec d) in U, zeta x ^ 2 * u.toFun x ^ 2 ≤ T

The mass form of an energy inequality. When the forcing has the dissipative sign, the localized mass is bounded by whatever bounds the layer term of the energy inequality. The coefficient enters only through that inequality.

Absorbing the exponential factor

theorem DivergenceFormProcess.Decay.integral_sq_mul_gradSq_product_le {d : ℕ} {U : Set (HCPolySupport.Vec d)} {u : HCPolySupport.H1Function U} {eta chi : HCPolySupport.Vec d → ℝ} {kappa : ℝ} (heta : ContDiff ℝ (↑⊤) eta) (hetaCompact : HasCompactSupport eta) (hchi : ContDiff ℝ (↑⊤) chi) (hchiGrad : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ chi x) (HCPolySupport.basisVec i)) ≤ kappa ^ 2 * chi x ^ 2) : (∫ (x : HCPolySupport.Vec d) in U, u.toFun x ^ 2 * HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ (fun (y : HCPolySupport.Vec d) => eta y * chi y) x) (HCPolySupport.basisVec i)) ≤ (2 * ∫ (x : HCPolySupport.Vec d) in U, u.toFun x ^ 2 * (chi x ^ 2 * HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ eta x) (HCPolySupport.basisVec i))) + 2 * kappa ^ 2 * ∫ (x : HCPolySupport.Vec d) in U, u.toFun x ^ 2 * (eta x ^ 2 * chi x ^ 2)

The squared gradient of a product weight is controlled by the squared gradient of the localization and the logarithmic rate of the second factor.

theorem DivergenceFormProcess.Decay.localizedMass_absorb_remainder {d : ℕ} {U : Set (HCPolySupport.Vec d)} {u : HCPolySupport.H1Function U} {eta chi : HCPolySupport.Vec d → ℝ} {mass kappa Cbase remainder : ℝ} (heta : ContDiff ℝ (↑⊤) eta) (hetaCompact : HasCompactSupport eta) (hchi : ContDiff ℝ (↑⊤) chi) (hCbase : 0 ≤ Cbase) (hchiGrad : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ chi x) (HCPolySupport.basisVec i)) ≤ kappa ^ 2 * chi x ^ 2) (habs : remainder + 2 * Cbase * kappa ^ 2 ≤ mass / 2) (hbase : mass * ∫ (x : HCPolySupport.Vec d) in U, (eta x * chi x) ^ 2 * u.toFun x ^ 2 ≤ (Cbase * ∫ (x : HCPolySupport.Vec d) in U, u.toFun x ^ 2 * HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ (fun (y : HCPolySupport.Vec d) => eta y * chi y) x) (HCPolySupport.basisVec i)) + remainder * ∫ (x : HCPolySupport.Vec d) in U, u.toFun x ^ 2 * (eta x ^ 2 * chi x ^ 2)) : mass / 2 * ∫ (x : HCPolySupport.Vec d) in U, u.toFun x ^ 2 * (eta x ^ 2 * chi x ^ 2) ≤ 2 * Cbase * ∫ (x : HCPolySupport.Vec d) in U, u.toFun x ^ 2 * (chi x ^ 2 * HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ eta x) (HCPolySupport.basisVec i))

Absorb a logarithmic weight while paying an explicit remainder from the mass budget.

theorem DivergenceFormProcess.Decay.localizedMass_absorb {d : ℕ} {U : Set (HCPolySupport.Vec d)} {u : HCPolySupport.H1Function U} {eta chi : HCPolySupport.Vec d → ℝ} {mass kappa Cbase : ℝ} (heta : ContDiff ℝ (↑⊤) eta) (hetaCompact : HasCompactSupport eta) (hchi : ContDiff ℝ (↑⊤) chi) (hCbase : 0 ≤ Cbase) (hchiGrad : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ chi x) (HCPolySupport.basisVec i)) ≤ kappa ^ 2 * chi x ^ 2) (habs : 2 * Cbase * kappa ^ 2 ≤ mass / 2) (hbase : mass * ∫ (x : HCPolySupport.Vec d) in U, (eta x * chi x) ^ 2 * u.toFun x ^ 2 ≤ Cbase * ∫ (x : HCPolySupport.Vec d) in U, u.toFun x ^ 2 * HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ (fun (y : HCPolySupport.Vec d) => eta y * chi y) x) (HCPolySupport.basisVec i)) : mass / 2 * ∫ (x : HCPolySupport.Vec d) in U, u.toFun x ^ 2 * (eta x ^ 2 * chi x ^ 2) ≤ 2 * Cbase * ∫ (x : HCPolySupport.Vec d) in U, u.toFun x ^ 2 * (chi x ^ 2 * HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ eta x) (HCPolySupport.basisVec i))

Absorption of a logarithmic weight. Given a mass bound whose layer term is the squared gradient of the product weight, and a factor obeying the logarithmic gradient bound at rate kappa, half of the mass is absorbed and only the gradient of the localization survives.

The localized Agmon mass estimate