IntegratedCoercivity

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

Integrated coercivity at the printed contrast

This is the measure-theoretic form of the corrected first line of the energy test. Integrability is kept explicit so it can be supplied by the weak-test module without strengthening the a.e. L^∞ coefficient carrier.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.integral_half_vecNormSq_le_coefficientEnergy {d : ℕ} {W : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {alpha : ℝ} (halpha0 : 0 < alpha) (halpha1 : alpha < 1) (ha : CoefficientIdentityDistanceLE W a (smallContrastThreshold d alpha)) (hleft : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => 1 / 2 * HCPolySupport.vecNormSq (G x)) W MeasureTheory.volume) (hright : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => HCPolySupport.vecDot (G x) (HCPolySupport.matVecMul (a x) (G x))) W MeasureTheory.volume) : ∫ (x : HCPolySupport.Vec d) in W, 1 / 2 * HCPolySupport.vecNormSq (G x) ≤ ∫ (x : HCPolySupport.Vec d) in W, HCPolySupport.vecDot (G x) (HCPolySupport.matVecMul (a x) (G x))