Coarse-graining support: Support.Sobolev.Foundations.ZeroTraceAverages

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

theorem HCPolySupport.IsPotentialZeroTraceOn.integral_eq_zero {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {f : Vec d → Vec d} (hf : IsPotentialZeroTraceOn U f) : (fun (i : Fin d) => ∫ (x : Vec d) in U, f x i) = 0

theorem HCPolySupport.H10Function.averageGradient_eq_zero {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H10Function U) : u.averageGradient = 0

Zero-trace H¹ functions have vanishing componentwise average gradient.

theorem HCPolySupport.H10Function.averageGradient_eq_zero_of_isSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (_hU : IsSobolevRegularDomain U) (u : H10Function U) : u.averageGradient = 0

Domain-regularity wrapper for H10Function.averageGradient_eq_zero.

theorem HCPolySupport.cubeAverage_eq_neg_cubeAverage_grad_mul_centeredCoord_of_h10OnCube {d : ℕ} (Q : TriadicCube d) (u : H10Function (cubeSet Q)) (i : Fin d) : (cubeAverage Q fun (x : Vec d) => u.toFun x) = -cubeAverage Q fun (x : Vec d) => u.grad x i * (x i - cubeCenter Q i)

On a half-open cube, the scalar average of an H¹₀ function is a coordinate-gradient pairing against the centered coordinate.

theorem HCPolySupport.IsSolenoidalZeroNormalTraceOn.integral_eq_zero {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) {g : Vec d → Vec d} (hg : IsSolenoidalZeroNormalTraceOn U g) : (fun (i : Fin d) => ∫ (x : Vec d) in U, g x i) = 0

theorem HCPolySupport.cubeAverageVec_grad_eq_zero_of_h10OnCube {d : ℕ} (Q : TriadicCube d) (u : H10Function (cubeSet Q)) : (cubeAverageVec Q fun (x : Vec d) => u.grad x) = 0