Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.SummationByParts

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

Summation by parts for weak interior difference quotients

This file keeps the measure-theoretic finite-difference integration by parts separate from DifferenceQuotient.lean, which is already close to the project file-size cap. The key point is that the identity below assumes only the integrability needed to expand the Lebesgue integrals, so it can be used with an H¹ representative rather than a smooth compactly supported function.

theorem HCPolySupport.integral_forwardDifference_mul_eq_neg_integral_mul_of_integrable {d : ℕ} {u v : Vec d → ℝ} (h : ℝ) (i : Fin d) (hshiftInt : MeasureTheory.Integrable (fun (x : Vec d) => u (euclideanCoordShift h i x) * v x) MeasureTheory.volume) (huvInt : MeasureTheory.Integrable (fun (x : Vec d) => u x * v x) MeasureTheory.volume) (hbackShiftInt : MeasureTheory.Integrable (fun (x : Vec d) => u x * v (euclideanCoordShift (-h) i x)) MeasureTheory.volume) : ∫ (x : Vec d), euclideanForwardDifferenceQuotient h i u x * v x = -∫ (x : Vec d), u x * euclideanBackwardDifferenceQuotient h i v x

Whole-space finite-difference summation by parts under explicit integrability hypotheses.

This is the weak-solution version of integral_forwardDifference_mul_eq_neg_integral_mul_backwardDifference: the left factor need not be smooth or compactly supported.