WeightedEnergy

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

Weighted energy inequality for a localized solution

The decay estimates of this directory rest on the Caccioppoli inequality obtained by testing -div (a grad u) = g with zeta ^ 2 * u, where zeta is a smooth compactly supported weight whose topological support lies in the domain. Unlike the De Giorgi cutoff test, no level truncation is involved: the estimate is applied to the solution itself, and the mass term produced by the forcing is what drives the decay. The Young inequality for the flux cross term is the one already used by the level-set estimate, DivergenceFormProcess.Form.cutoff_flux_young.

Main results

• DivergenceFormProcess.Decay.weightedEnergy_identity: the exact identity produced by the test zeta ^ 2 * u.

theorem DivergenceFormProcess.Decay.integrable_sq_mul_memLpTop {d : ℕ} {U : Set (HCPolySupport.Vec d)} {u : HCPolySupport.H1Function U} {F : HCPolySupport.Vec d → ℝ} (hF : MeasureTheory.MemLp F ⊤ (HCPolySupport.volumeMeasureOn U)) : MeasureTheory.Integrable (fun (x : HCPolySupport.Vec d) => u.toFun x ^ 2 * F x) (HCPolySupport.volumeMeasureOn U)

The square of an H¹ value against an essentially bounded weight is integrable.

theorem DivergenceFormProcess.Decay.sq_weight_smooth {d : ℕ} {zeta : HCPolySupport.Vec d → ℝ} (hzeta : ContDiff ℝ (↑⊤) zeta) (hzetaCompact : HasCompactSupport zeta) : (ContDiff ℝ ↑⊤ fun (x : HCPolySupport.Vec d) => zeta x ^ 2) ∧ HasCompactSupport fun (x : HCPolySupport.Vec d) => zeta x ^ 2

The square of a smooth compactly supported weight is a smooth compactly supported multiplier.

theorem DivergenceFormProcess.Decay.tsupport_sq_weight_subset {d : ℕ} {zeta : HCPolySupport.Vec d → ℝ} {V : Set (HCPolySupport.Vec d)} (hzetaU : tsupport zeta ⊆ V) : (tsupport fun (x : HCPolySupport.Vec d) => zeta x ^ 2) ⊆ V

Squaring does not enlarge the topological support.

theorem DivergenceFormProcess.Decay.isAdmissibleMultiplier_sq_of_tsupport_subset {d : ℕ} {U : Set (HCPolySupport.Vec d)} {zeta : HCPolySupport.Vec d → ℝ} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (u : HCPolySupport.H1Function U) (hzeta : ContDiff ℝ (↑⊤) zeta) (hzetaCompact : HasCompactSupport zeta) (hzetaU : tsupport zeta ⊆ U) : IsAdmissibleMultiplier U u fun (x : HCPolySupport.Vec d) => zeta x ^ 2

The squared weight is admissible whenever the weight is supported in the domain.

theorem DivergenceFormProcess.Decay.isAdmissibleMultiplier_sq_of_zeroTrace {d : ℕ} {U : Set (HCPolySupport.Vec d)} {zeta : HCPolySupport.Vec d → ℝ} (z : HCPolySupport.H10Function U) (hzeta : ContDiff ℝ (↑⊤) zeta) (hzetaCompact : HasCompactSupport zeta) : IsAdmissibleMultiplier U z.toH1Function fun (x : HCPolySupport.Vec d) => zeta x ^ 2

The squared weight is admissible for a factor with zero trace.

theorem DivergenceFormProcess.Decay.weightedEnergy_identity {d : ℕ} {U : Set (HCPolySupport.Vec d)} {zeta : HCPolySupport.Vec d → ℝ} {a : HCPolySupport.CoeffField d} {g : HCPolySupport.Vec d → ℝ} {u : HCPolySupport.H1Function U} (hsol : Form.IsScalarForcedWeakSolution a U g u) (hzeta : ContDiff ℝ (↑⊤) zeta) (hadm : IsAdmissibleMultiplier U u fun (x : HCPolySupport.Vec d) => zeta x ^ 2) : (∫ (x : HCPolySupport.Vec d) in U, zeta x ^ 2 * HCPolySupport.vecDot (HCPolySupport.matVecMul (a x) (u.grad x)) (u.grad x) + 2 * zeta x * u.toFun x * HCPolySupport.vecDot (HCPolySupport.matVecMul (a x) (u.grad x)) fun (i : Fin d) => (fderiv ℝ zeta x) (HCPolySupport.basisVec i)) = ∫ (x : HCPolySupport.Vec d) in U, g x * (zeta x ^ 2 * u.toFun x)

Testing -div (a grad u) = g with zeta ^ 2 * u gives the exact energy identity. No ellipticity estimate is used here.