Coarse-graining support:

Support.Sobolev.Foundations.CubeCalderonZygmund.H1CutoffIntegrationByParts

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.CubeCalderonZygmund.h1_cutoff_integration_by_parts {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (r v : H1Function U) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_compact : HasCompactSupport η) (hη_sub : tsupport η ⊆ U) : ∫ (x : Vec d) in U, v.toFun x * vecDot (r.grad x) (euclideanGradient η x) = (-∫ (x : Vec d) in U, r.toFun x * vecDot (v.grad x) (euclideanGradient η x)) - ∫ (x : Vec d) in U, r.toFun x * v.toFun x * euclideanCoordLaplacian η x

Integration by parts for two H¹ functions after multiplying by a smooth compactly supported cutoff. Neither function is assumed to have zero trace.