LocalizedLocalL2

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

Local L² and gradient bounds with layer constants

The two consequences of the weighted energy estimate that the pointwise step consumes are restated so that the coefficient enters only on the transition layer of the localization.

• the exponentially weighted mass on an inner ball, from which the plain local L² bound is read;
• the Caccioppoli gradient bound on an inner ball.

Both are obtained from a weighted energy inequality supplied as a hypothesis, so the same proofs serve the estimate with a single antisymmetric part and the estimate with a split antisymmetric part.

Main results

• DivergenceFormProcess.Decay.setIntegral_sq_mul_exp_gradSq_layer_le
• DivergenceFormProcess.Decay.setIntegral_sq_le_exp_of_agmonMass
• DivergenceFormProcess.Decay.setIntegral_gradSq_le_of_localizedBound

The layer term

theorem DivergenceFormProcess.Decay.setIntegral_sq_mul_exp_gradSq_layer_le {d : ℕ} {Om : Set (HCPolySupport.Vec d)} (hOmOpen : IsOpen Om) (hOmBdd : HCPolySupport.IsBoundedDomain Om) {u : HCPolySupport.H1Function Om} {eta psi : HCPolySupport.Vec d → ℝ} {kappa M Ceta volLayer tA : ℝ} (hMbound : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn Om, |u.toFun y| ≤ M) (heta : ContDiff ℝ (↑⊤) eta) (hetaCompact : HasCompactSupport eta) (hpsi : ContDiff ℝ (↑⊤) psi) (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) (hkappa0 : 0 ≤ kappa) : ∫ (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)) ≤ M ^ 2 * Ceta * Real.exp (2 * (kappa * tA)) * volLayer

The exponentially weighted layer term is paid for by the maximum bound, the gradient bound of the localization, the phase on the layer and the volume of the layer.

From a weighted mass estimate to a local L² bound

theorem DivergenceFormProcess.Decay.setIntegral_sq_le_exp_of_agmonMass {d : ℕ} {Om : Set (HCPolySupport.Vec d)} (hOmOpen : IsOpen Om) (hOmBdd : HCPolySupport.IsBoundedDomain Om) {u : HCPolySupport.H1Function Om} {eta psi : HCPolySupport.Vec d → ℝ} {lam Lam mass kappa M Ceta volLayer tA tx : ℝ} (hlam : 0 < lam) (hmass : 0 < mass) (hMbound : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn Om, |u.toFun y| ≤ M) (heta : ContDiff ℝ (↑⊤) eta) (hetaCompact : HasCompactSupport eta) (hpsi : ContDiff ℝ (↑⊤) psi) (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) (hkappa0 : 0 ≤ kappa) (hagmon : mass / 2 * ∫ (y : HCPolySupport.Vec d) in Om, u.toFun y ^ 2 * (eta y ^ 2 * Real.exp (kappa * psi y) ^ 2) ≤ 4 * Lam ^ 2 / lam * ∫ (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))) {x : HCPolySupport.Vec d} {R : ℝ} (hinner : ∀ y ∈ HCPolySupport.euclideanBall x R, eta y = 1) (hphase : ∀ y ∈ HCPolySupport.euclideanBall x R, tx ≤ psi y) (rho : ℝ) : 0 < rho → rho ≤ R → HCPolySupport.euclideanBall x rho ⊆ Om → ∫ (y : HCPolySupport.Vec d) in HCPolySupport.euclideanBall x rho, u.toFun y ^ 2 ≤ (M * √(8 * Lam ^ 2 / (lam * mass) * Ceta * volLayer)) ^ 2 * Real.exp (-(2 * (kappa * (tx - tA))))

The contrast-free bridge, from a weighted mass estimate. Whatever supplies the exponentially weighted mass estimate, the plain L² mass on an inner ball is controlled by the layer data and the phase gap.

The localized local L² bound

The Caccioppoli gradient bound

theorem DivergenceFormProcess.Decay.setIntegral_gradSq_le_of_localizedBound {d : ℕ} {Om : Set (HCPolySupport.Vec d)} {u : HCPolySupport.H1Function Om} {eta : HCPolySupport.Vec d → ℝ} {S : ℝ} (heta : ContDiff ℝ (↑⊤) eta) (hetaCompact : HasCompactSupport eta) (hgrad : ∫ (y : HCPolySupport.Vec d) in Om, eta y ^ 2 * HCPolySupport.vecNormSq (u.grad y) ≤ S) {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 (u.grad y) ≤ S

The localized gradient energy dominates the gradient energy on any set where the localization is one.

theorem DivergenceFormProcess.Decay.setIntegral_sq_mul_gradSq_layer_le {d : ℕ} {Om : Set (HCPolySupport.Vec d)} (hOmOpen : IsOpen Om) (hOmBdd : HCPolySupport.IsBoundedDomain Om) {u : HCPolySupport.H1Function Om} {eta : HCPolySupport.Vec d → ℝ} {M Ceta volLayer : ℝ} (hMbound : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn Om, |u.toFun y| ≤ M) (heta : ContDiff ℝ (↑⊤) eta) (hetaCompact : HasCompactSupport eta) (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) : (∫ (y : HCPolySupport.Vec d) in Om, u.toFun y ^ 2 * HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ eta y) (HCPolySupport.basisVec i)) ≤ M ^ 2 * Ceta * volLayer

The unweighted layer term, the case of a constant weight.