CaccioppoliAbsorbed

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

Young-absorbed Caccioppoli inequality

theorem DivergenceFormProcess.Form.cutoff_flux_young {d : ℕ} {lam Lam e p : ℝ} {A : HCPolySupport.Mat d} (z de : HCPolySupport.Vec d) (hA : HCPolySupport.IsEllipticMatrix lam Lam A) : |2 * e * p * HCPolySupport.vecDot (HCPolySupport.matVecMul A z) de| ≤ lam / 2 * (e ^ 2 * HCPolySupport.vecNormSq z) + 2 * Lam ^ 2 / lam * (p ^ 2 * HCPolySupport.vecNormSq de)

Young inequality for the cutoff flux cross term, with the explicit nonsymmetric ellipticity constant. Half of the elliptic energy is kept and the remainder is charged to the cutoff gradient.