Lp One

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.integral_norm_sub_integralAverage_le_bound_of_isOpenBoundedConvexDomain {d : ℕ} [NeZero d] {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsOpenBoundedConvexDomain U) {u : Vec d → ℝ} (hu : MeasureTheory.IntegrableOn u U MeasureTheory.volume) (huDiff : ContDiff ℝ 1 u) (hvol : 0 < (MeasureTheory.volume U).toReal) : ∫ (x : Vec d) in U, ‖u x - integralAverage U u‖ ≤ (MeasureTheory.volume U).toReal⁻¹ * ((2 * Classical.choose ⋯) ^ d / ↑d) * (↑d * (MeasureTheory.volume (Metric.ball 0 1)).toReal * (4 * Classical.choose ⋯)) * ∫ (y : Vec d) in U, ‖fderiv ℝ u y‖