ExponentialWeight

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

Exponentially weighted mass estimate

The weight of the Agmon-type estimate is a localized exponential eta * chi, where eta is a smooth compactly supported localization inside the domain and chi is a smooth positive factor obeying the logarithmic gradient bound |grad chi| <= kappa * chi. The exponential chi = exp (kappa * psi) of a smooth function with |grad psi| <= 1 is the model case.

The mass form of the weighted energy inequality then absorbs the exponential contribution as soon as 8 * Lam ^ 2 * kappa ^ 2 <= lam * mass, leaving only the contribution of the localization gradient. This is the quantitative statement behind the exponential decay of a solution away from the region where the localization is not yet constant.

Main results

• DivergenceFormProcess.Decay.exponentialWeight_gradient_le

theorem DivergenceFormProcess.Decay.hasCompactSupport_gradSq {d : ℕ} {f : HCPolySupport.Vec d → ℝ} (hf : HasCompactSupport f) : HasCompactSupport fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ f x) (HCPolySupport.basisVec i)

The coordinate gradient of a smooth compactly supported function has compact support, and so does its squared norm.

theorem DivergenceFormProcess.Decay.continuous_gradSq {d : ℕ} {f : HCPolySupport.Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) : Continuous fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ f x) (HCPolySupport.basisVec i)

The squared coordinate gradient of a smooth function is continuous.

theorem DivergenceFormProcess.Decay.tsupport_mul_subset {d : ℕ} {eta chi : HCPolySupport.Vec d → ℝ} {V : Set (HCPolySupport.Vec d)} (hetaU : tsupport eta ⊆ V) : (tsupport fun (x : HCPolySupport.Vec d) => eta x * chi x) ⊆ V

Multiplying by a second factor does not enlarge the topological support.

theorem DivergenceFormProcess.Decay.isAdmissibleMultiplier_localized_of_tsupport_subset {d : ℕ} {U : Set (HCPolySupport.Vec d)} {eta chi : HCPolySupport.Vec d → ℝ} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (u : HCPolySupport.H1Function U) (heta : ContDiff ℝ (↑⊤) eta) (hetaCompact : HasCompactSupport eta) (hetaU : tsupport eta ⊆ U) (hchi : ContDiff ℝ (↑⊤) chi) : IsAdmissibleMultiplier U u fun (x : HCPolySupport.Vec d) => (eta x * chi x) ^ 2

The localized weight is admissible when the localization is supported in the domain.

theorem DivergenceFormProcess.Decay.contDiff_exponentialWeight {d : ℕ} {psi : HCPolySupport.Vec d → ℝ} (hpsi : ContDiff ℝ (↑⊤) psi) (kappa : ℝ) : ContDiff ℝ ↑⊤ fun (x : HCPolySupport.Vec d) => Real.exp (kappa * psi x)

The exponential of a smooth function is smooth.

theorem DivergenceFormProcess.Decay.exponentialWeight_gradient_le {d : ℕ} {psi : HCPolySupport.Vec d → ℝ} (hpsi : ContDiff ℝ (↑⊤) psi) {x : HCPolySupport.Vec d} (hpsiGrad : (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ psi x) (HCPolySupport.basisVec i)) ≤ 1) (kappa : ℝ) : (HCPolySupport.vecNormSq fun (i : Fin d) => (fderiv ℝ (fun (y : HCPolySupport.Vec d) => Real.exp (kappa * psi y)) x) (HCPolySupport.basisVec i)) ≤ kappa ^ 2 * Real.exp (kappa * psi x) ^ 2

The exponential weight of a smooth function obeys the logarithmic gradient bound with constant kappa at every point where the phase has unit gradient.

theorem DivergenceFormProcess.Decay.agmonRate_admissible {lam Lam mass : ℝ} (hlam : 0 ≤ lam) (hmass : 0 ≤ mass) (hLam : 0 < Lam) : 8 * Lam ^ 2 * (√(lam * mass) / (2 * √2 * Lam)) ^ 2 ≤ lam * mass

The canonical admissible rate. The Agmon rate sqrt (lam * mass) / (2 * sqrt 2 * Lam) saturates the absorption condition.