Mean subtraction for ball estimates

Adapted from CoarseGraining (LeanIntoHomogenization, 2026) with the author's permission. These identities separate the average bookkeeping from the analytic segment estimate.

theorem CKN.sub_integralAverage_eq_volumeAverage_sub {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeOn 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 CKN.norm_sub_integralAverage_le_volumeAverage_integral_norm_sub {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeOn 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‖