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

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

Integral identities for convex-domain Poincare

This file collects the first measure-theoretic identities behind the future convex-domain mean-zero Poincare proof. At this stage we only need the basic algebra that rewrites u x - average_U u as the normalized average of the differences u x - u y.

theorem HCPolySupport.sub_integralAverage_eq_volumeAverage_sub {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {u : Vec d → ℝ} (hu : MeasureTheory.IntegrableOn u U MeasureTheory.volume) (x : Vec d) (hvol : 0 < (MeasureTheory.volume U).toReal) : u x - integralAverage U u = (MeasureTheory.volume U).toReal⁻¹ * ∫ (y : Vec d) in U, u x - u y

theorem HCPolySupport.norm_sub_integralAverage_le_volumeAverage_integral_norm_sub {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {u : Vec d → ℝ} (hu : MeasureTheory.IntegrableOn u U MeasureTheory.volume) (x : Vec d) (hvol : 0 < (MeasureTheory.volume U).toReal) : ‖u x - integralAverage U u‖ ≤ (MeasureTheory.volume U).toReal⁻¹ * ∫ (y : Vec d) in U, ‖u x - u y‖