ZerothOrderEnergy #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Energy comparison with a bounded scalar source #
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Ported.harmonicComparison_normalizedEnergy_zerothOrder
{d : ℕ}
[NeZero d]
(z : HCPolySupport.Vec d)
{r : ℝ}
(hr : 0 < r)
{a : HCPolySupport.CoeffField d}
{u h : HCPolySupport.H1Function (HCPolySupport.euclideanBall z r)}
{rho : HCPolySupport.H10Function (HCPolySupport.euclideanBall z r)}
{g : HCPolySupport.Vec d → ℝ}
{f : HCPolySupport.Vec d → HCPolySupport.Vec d}
{delta alpha : ℝ}
(hmeas : Measurable a)
(ha : CoefficientIdentityDistanceLE (HCPolySupport.euclideanBall z r) a delta)
(halpha0 : 0 < alpha)
(halpha1 : alpha < 1)
(hdelta0 : 0 ≤ delta)
(hdelta : delta ≤ smallContrastThreshold d alpha)
(hu : IsMatrixDivFormWeakSolutionZerothOrderOn a (HCPolySupport.euclideanBall z r) u g f)
(hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (HCPolySupport.euclideanBall z r)))
(hf : HCPolySupport.MemVectorL2 (HCPolySupport.euclideanBall z r) f)
(hh : IsUnitWeaklyHarmonicOn (HCPolySupport.euclideanBall z r) h)
(hgrad : ∀ (x : HCPolySupport.Vec d), h.grad x = u.grad x + rho.grad x)
:
vectorNormalizedL2On (HCPolySupport.euclideanBall z r) rho.grad ≤ 2 * delta * vectorNormalizedL2On (HCPolySupport.euclideanBall z r) h.grad + 2 * vectorNormalizedL2On (HCPolySupport.euclideanBall z r) f + 4 * unitCubeDirichletPoincareExplicit d * ↑d * r * Section4.Support.normalizedL2On (HCPolySupport.euclideanBall z r) g
Normalized harmonic comparison with the extra Poincaré-priced scalar source.