ZerothOrderTesting

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

Harmonic comparison with an additional scalar functional

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.harmonicComparison_gradientEnergy_with_test {d : ℕ} {W : Set (HCPolySupport.Vec d)} [MeasureTheory.IsFiniteMeasure (HCPolySupport.volumeMeasureOn W)] {a : HCPolySupport.CoeffField d} {u h : HCPolySupport.H1Function W} {rho : HCPolySupport.H10Function W} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} {delta alpha : ℝ} (hmeas : Measurable a) (ha : CoefficientIdentityDistanceLE W a delta) (halpha0 : 0 < alpha) (halpha1 : alpha < 1) (hdelta0 : 0 ≤ delta) (hdelta : delta ≤ smallContrastThreshold d alpha) {zeroth Z : ℝ} (htest : ∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.vecDot (HCPolySupport.matVecMul (a x) (u.grad x)) (rho.grad x) = zeroth - ∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.vecDot (f x) (rho.grad x)) (hzeroth : |zeroth| ≤ Z * √(∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.vecNormSq (rho.grad x))) (hZ : 0 ≤ Z) (hf : HCPolySupport.MemVectorL2 W f) (hh : IsUnitWeaklyHarmonicOn W h) (hgrad : ∀ (x : HCPolySupport.Vec d), h.grad x = u.grad x + rho.grad x) : √(∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.vecNormSq (rho.grad x)) ≤ 2 * delta * √(∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.vecNormSq (h.grad x)) + 2 * √(∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.vecNormSq (f x)) + 2 * Z

Harmonic comparison when the tested equation contains one additional scalar functional, quantified by Z times the comparison-gradient energy.