LocalizedSplitMass

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

The Agmon mass estimate with a split antisymmetric part

The drift term produced by the smooth antisymmetric part carries the divergence of that part and the gradient of the exponential weight. Both contributions are paid for here: the part carried by the gradient of the localization is absorbed by half of the mass, and the part carried by the gradient of the phase is proportional to the rate, so it is absorbed by the same budget that fixes the rate.

Main results

• DivergenceFormProcess.Decay.integral_sq_mul_vecDot_skewFieldDiv_le
• DivergenceFormProcess.Decay.agmonMass_split_le
• DivergenceFormProcess.Decay.localizedAgmonUpper

The drift term

theorem DivergenceFormProcess.Decay.fderiv_sq_apply {d : ℕ} {zeta : HCPolySupport.Vec d → ℝ} (hzeta : ContDiff ℝ (↑⊤) zeta) (x : HCPolySupport.Vec d) (i : Fin d) : (fderiv ℝ (fun (y : HCPolySupport.Vec d) => zeta y ^ 2) x) (HCPolySupport.basisVec i) = 2 * zeta x * (fderiv ℝ zeta x) (HCPolySupport.basisVec i)

The coordinate gradient of a squared weight.

theorem DivergenceFormProcess.Decay.integral_sq_mul_vecDot_skewFieldDiv_le {d : ℕ} {Om : Set (HCPolySupport.Vec d)} {u : HCPolySupport.H1Function Om} {kl : HCPolySupport.Vec d → HCPolySupport.Mat d} {zeta : HCPolySupport.Vec d → ℝ} {L : Set (HCPolySupport.Vec d)} {Kl mass : ℝ} (hmass : 0 < mass) (hzeta : ContDiff ℝ (↑⊤) zeta) (hzetaCompact : HasCompactSupport zeta) (hzetaL : tsupport zeta ⊆ L) (hklC1 : ∀ (p q : Fin d), ContDiff ℝ 1 fun (y : HCPolySupport.Vec d) => kl y p q) (hklDiv : ∀ y ∈ L, HCPolySupport.vecNormSq (skewFieldDiv kl y) ≤ Kl ^ 2) : (-(1 / 2) * ∫ (y : HCPolySupport.Vec d) in Om, u.toFun y ^ 2 * HCPolySupport.vecDot (skewFieldDiv kl y) fun (i : Fin d) => (fderiv ℝ (fun (w : HCPolySupport.Vec d) => zeta w ^ 2) y) (HCPolySupport.basisVec i)) ≤ (mass / 8 * ∫ (y : HCPolySupport.Vec d) in Om, u.toFun y ^ 2 * zeta y ^ 2) + 2 * Kl ^ 2 / mass * ∫ (y : HCPolySupport.Vec d) in Om, u.toFun y ^ 2 * HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ zeta y) (HCPolySupport.basisVec i)

The drift term of the smooth antisymmetric part. The drift produced by integrating the smooth part by parts carries no gradient of the solution: it is split between a part absorbed by an eighth of the mass and a layer part proportional to the squared divergence bound and to the squared gradient of the weight. The size of the divergence is needed only on the layer that carries the weight.

theorem DivergenceFormProcess.Decay.agmonMass_split_of_energy_le {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {u : HCPolySupport.H1Function U} {g eta chi : HCPolySupport.Vec d → ℝ} {nu Ks Kl mass kappa D : ℝ} (hnu : 0 < nu) (hmass : 0 < mass) (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) (hsol : Form.IsScalarForcedWeakSolution a U g u) (hadm : IsAdmissibleMultiplier U u fun (x : HCPolySupport.Vec d) => (eta x * chi x) ^ 2) (hg : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, eta x * chi x ≠ 0 → g x * u.toFun x ≤ -(mass * u.toFun x ^ 2)) (henergy : (nu / 2 * ∫ (x : HCPolySupport.Vec d) in U, (eta x * chi x) ^ 2 * HCPolySupport.vecNormSq (u.grad x)) + 1 / 2 * D ≤ (∫ (x : HCPolySupport.Vec d) in U, g x * ((eta x * chi x) ^ 2 * u.toFun x)) + 2 * (nu + Ks) ^ 2 / nu * ∫ (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)) (hdrift : -(1 / 2) * D ≤ (mass / 8 * ∫ (x : HCPolySupport.Vec d) in U, u.toFun x ^ 2 * (eta x * chi x) ^ 2) + 2 * Kl ^ 2 / mass * ∫ (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)) (hadmiss : (4 * (nu + Ks) ^ 2 / nu + 4 * Kl ^ 2 / mass) * kappa ^ 2 ≤ 3 * mass / 8) : mass / 2 * ∫ (x : HCPolySupport.Vec d) in U, u.toFun x ^ 2 * (eta x ^ 2 * chi x ^ 2) ≤ (4 * (nu + Ks) ^ 2 / nu + 4 * Kl ^ 2 / mass) * ∫ (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))

The split-skew mass argument after admissibility, energy and drift witnesses are supplied. The logarithmic weight is arbitrary, and no trace or domain regularity is required here.

The Agmon mass estimate with a split antisymmetric part

theorem DivergenceFormProcess.Decay.agmonMass_split_le {d : ℕ} {Om : Set (HCPolySupport.Vec d)} (hOmOpen : IsOpen Om) (hOmBdd : HCPolySupport.IsBoundedDomain Om) {a : HCPolySupport.CoeffField d} {ks kl : HCPolySupport.Vec d → HCPolySupport.Mat d} {z : HCPolySupport.H10Function Om} {g eta psi : HCPolySupport.Vec d → ℝ} {L : Set (HCPolySupport.Vec d)} {nu LamS Ks Kl mass kappa : ℝ} (hnu : 0 < nu) (hKs : 0 ≤ Ks) (hmass : 0 < mass) (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 z.toH1Function) (heta : ContDiff ℝ (↑⊤) eta) (hetaCompact : HasCompactSupport eta) (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 * z.toFun y ≤ -(mass * z.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, z.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, z.toFun y ^ 2 * (Real.exp (kappa * psi y) ^ 2 * HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ eta y) (HCPolySupport.basisVec i))

The Agmon weighted mass estimate with a split antisymmetric part. The rough part contributes its size on the layer and the smooth part its divergence on the layer; the admissibility of the rate is the single budget inequality hadmiss.

The effective upper constant

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

The effective upper ellipticity constant of the localized estimate: the size of the rough part on the layer, together with the divergence of the smooth part measured against the mass.

Equations

• DivergenceFormProcess.Decay.localizedAgmonUpper nu mass Ks Kl = √2 * (nu + Ks + 2 * Kl * √(nu / mass))

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

theorem DivergenceFormProcess.Decay.two_mul_sq_le_localizedAgmonUpper_sq {nu mass Ks Kl : ℝ} (hnu : 0 < nu) (hKs : 0 ≤ Ks) (hKl : 0 ≤ Kl) : 2 * (nu + Ks) ^ 2 ≤ localizedAgmonUpper nu mass Ks Kl ^ 2

The effective constant dominates the size of the rough part.

theorem DivergenceFormProcess.Decay.eight_mul_div_le_localizedAgmonUpper_sq {nu mass Ks Kl : ℝ} (hnu : 0 < nu) (hmass : 0 < mass) (hKs : 0 ≤ Ks) (hKl : 0 ≤ Kl) : 8 * nu * Kl ^ 2 / mass ≤ localizedAgmonUpper nu mass Ks Kl ^ 2

The effective constant dominates the divergence of the smooth part measured against the mass.

theorem DivergenceFormProcess.Decay.localizedAgmonUpper_coefficient_bounds {nu mass Ks Kl : ℝ} (hnu : 0 < nu) (hmass : 0 < mass) (hKs : 0 ≤ Ks) (hKl : 0 ≤ Kl) : 4 * (nu + Ks) ^ 2 / nu + 4 * Kl ^ 2 / mass ≤ 3 * localizedAgmonUpper nu mass Ks Kl ^ 2 / nu ∧ 4 * (nu + Ks) ^ 2 / nu + 4 * Kl ^ 2 / mass ≤ 4 * localizedAgmonUpper nu mass Ks Kl ^ 2 / nu ∧ 4 * (nu + Ks) ^ 2 / nu ^ 2 + Kl ^ 2 / (nu * mass) ≤ 4 * localizedAgmonUpper nu mass Ks Kl ^ 2 / nu ^ 2

One numerical comparison supplies the mass and gradient effective-constant bounds.

theorem DivergenceFormProcess.Decay.agmonMass_normalize_effective_constant {nu mass Ks Kl kappa A B : ℝ} (hnu : 0 < nu) (hmass : 0 < mass) (hKs : 0 ≤ Ks) (hKl : 0 ≤ Kl) (hkappa : 8 * localizedAgmonUpper nu mass Ks Kl ^ 2 * kappa ^ 2 ≤ nu * mass) (hB : 0 ≤ B) (hbase : (4 * (nu + Ks) ^ 2 / nu + 4 * Kl ^ 2 / mass) * kappa ^ 2 ≤ 3 * mass / 8 → mass / 2 * A ≤ (4 * (nu + Ks) ^ 2 / nu + 4 * Kl ^ 2 / mass) * B) : mass / 2 * A ≤ 4 * localizedAgmonUpper nu mass Ks Kl ^ 2 / nu * B

Normalize an Agmon mass estimate at the effective constant and its rate budget.

The uniformly elliptic shape at the effective constant

theorem DivergenceFormProcess.Decay.agmonMass_localizedSplit_le {d : ℕ} {Om : Set (HCPolySupport.Vec d)} (hOmOpen : IsOpen Om) (hOmBdd : HCPolySupport.IsBoundedDomain Om) {a : HCPolySupport.CoeffField d} {ks kl : HCPolySupport.Vec d → HCPolySupport.Mat d} {z : HCPolySupport.H10Function Om} {g eta psi : HCPolySupport.Vec d → ℝ} {L : Set (HCPolySupport.Vec d)} {nu LamS Ks Kl mass kappa : ℝ} (hnu : 0 < nu) (hKs : 0 ≤ Ks) (hKl : 0 ≤ Kl) (hmass : 0 < mass) (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 z.toH1Function) (heta : ContDiff ℝ (↑⊤) eta) (hetaCompact : HasCompactSupport eta) (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 * z.toFun y ≤ -(mass * z.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, z.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, z.toFun y ^ 2 * (Real.exp (kappa * psi y) ^ 2 * HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ eta y) (HCPolySupport.basisVec i))

The localized Agmon mass estimate at the effective constant. With the effective upper constant the estimate takes exactly the form of the uniformly elliptic one, at lower constant nu, and so does its admissibility hypothesis.

The Caccioppoli gradient bound with a split antisymmetric part

theorem DivergenceFormProcess.Decay.setIntegral_gradSq_split_le {d : ℕ} {Om : Set (HCPolySupport.Vec d)} (hOmOpen : IsOpen Om) (hOmBdd : HCPolySupport.IsBoundedDomain Om) {a : HCPolySupport.CoeffField d} {ks kl : HCPolySupport.Vec d → HCPolySupport.Mat d} {z : HCPolySupport.H10Function Om} {g eta : HCPolySupport.Vec d → ℝ} {L : Set (HCPolySupport.Vec d)} {nu LamS Ks Kl mu M Ceta volLayer : ℝ} (hnu : 0 < nu) (hKs : 0 ≤ Ks) (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) (heta : ContDiff ℝ (↑⊤) eta) (hetaCompact : HasCompactSupport eta) (hetaL : tsupport eta ⊆ L) (hzero : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn Om, eta y ≠ 0 → g y = 0) (hMbound : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn Om, |z.toFun y| ≤ M) (hCeta : 0 ≤ Ceta) (hetaGrad : ∀ y ∈ Om, (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ eta y) (HCPolySupport.basisVec i)) ≤ Ceta) (hvolLayer : (MeasureTheory.volume {y : HCPolySupport.Vec d | y ∈ Om ∧ fderiv ℝ eta y ≠ 0}).toReal ≤ volLayer) (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) {W : Set (HCPolySupport.Vec d)} (hW : MeasurableSet W) (hWOm : W ⊆ Om) (hWeta : ∀ y ∈ W, eta y = 1) : ∫ (y : HCPolySupport.Vec d) in W, HCPolySupport.vecNormSq (z.grad y) ≤ (4 * (nu + Ks) ^ 2 / nu ^ 2 + Kl ^ 2 / (nu * mu)) * M ^ 2 * (Ceta * volLayer)

The Caccioppoli gradient bound with a split antisymmetric part. The mass term is retained and absorbs the part of the drift carried by the gradient of the localization, so the constant depends only on the size of the rough part and the divergence of the smooth part on the layer.

theorem DivergenceFormProcess.Decay.setIntegral_gradSq_localizedSplit_le {d : ℕ} {Om : Set (HCPolySupport.Vec d)} (hOmOpen : IsOpen Om) (hOmBdd : HCPolySupport.IsBoundedDomain Om) {a : HCPolySupport.CoeffField d} {ks kl : HCPolySupport.Vec d → HCPolySupport.Mat d} {z : HCPolySupport.H10Function Om} {g eta : HCPolySupport.Vec d → ℝ} {L : Set (HCPolySupport.Vec d)} {nu LamS Ks Kl mu M Ceta volLayer : ℝ} (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) (heta : ContDiff ℝ (↑⊤) eta) (hetaCompact : HasCompactSupport eta) (hetaL : tsupport eta ⊆ L) (hzero : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn Om, eta y ≠ 0 → g y = 0) (hMbound : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn Om, |z.toFun y| ≤ M) (hCeta : 0 ≤ Ceta) (hetaGrad : ∀ y ∈ Om, (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ eta y) (HCPolySupport.basisVec i)) ≤ Ceta) (hvolLayer : (MeasureTheory.volume {y : HCPolySupport.Vec d | y ∈ Om ∧ fderiv ℝ eta y ≠ 0}).toReal ≤ volLayer) (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) {W : Set (HCPolySupport.Vec d)} (hW : MeasurableSet W) (hWOm : W ⊆ Om) (hWeta : ∀ y ∈ W, eta y = 1) : ∫ (y : HCPolySupport.Vec d) in W, HCPolySupport.vecNormSq (z.grad y) ≤ 4 * localizedAgmonUpper nu mu Ks Kl ^ 2 / nu ^ 2 * M ^ 2 * (Ceta * volLayer)

The Caccioppoli gradient bound at the effective constant. With the effective upper constant the bound takes exactly the form of the uniformly elliptic one, at lower constant nu.