Lp

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

Finite-p convex-domain Poincare scaffolding

This wrapper module will be the stable import target for the future bounded open convex domain L^p Poincare theorem family. For now it re-exports the first two implementation layers:

• segment geometry and smooth FTC along affine segments;
• the mean-minus-average integral identity.

The eventual theorem surface should live here once the nested integral estimates and the final convex-domain L^p bound are in place.

theorem CKN.integrableOn_integral_norm_fderiv_mul_norm_sub_along_segment_of_isSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) {u : Vec d → ℝ} (huDiff : ContDiff ℝ 1 u) (x : Vec d) : MeasureTheory.IntegrableOn (fun (y : Vec d) => ∫ (t : ℝ) in 0..1, ‖fderiv ℝ u (segmentBlend x t y)‖ * ‖x - y‖) U MeasureTheory.volume

theorem CKN.norm_sub_integralAverage_le_volumeAverage_integral_norm_fderiv_mul_norm_sub_along_segment {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {u : Vec d → ℝ} (hu : MeasureTheory.IntegrableOn u U MeasureTheory.volume) (huDiff : ContDiff ℝ 1 u) (x : Vec d) (hvol : 0 < (MeasureTheory.volume U).toReal) (hsegment : MeasureTheory.IntegrableOn (fun (y : Vec d) => ∫ (t : ℝ) in 0..1, ‖fderiv ℝ u (segmentBlend x t y)‖ * ‖x - y‖) U MeasureTheory.volume) : ‖u x - integralAverage U u‖ ≤ (MeasureTheory.volume U).toReal⁻¹ * ∫ (y : Vec d) in U, ∫ (t : ℝ) in 0..1, ‖fderiv ℝ u (segmentBlend x t y)‖ * ‖x - y‖

theorem CKN.norm_sub_average_le_gradient_segment_integral {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsSobolevRegularDomain U) {u : Vec d → ℝ} (hu : MeasureTheory.IntegrableOn u U MeasureTheory.volume) (huDiff : ContDiff ℝ 1 u) (x : Vec d) (hvol : 0 < (MeasureTheory.volume U).toReal) : ‖u x - integralAverage U u‖ ≤ (MeasureTheory.volume U).toReal⁻¹ * ∫ (y : Vec d) in U, ∫ (t : ℝ) in 0..1, ‖fderiv ℝ u (segmentBlend x t y)‖ * ‖x - y‖

theorem CKN.intervalIntegral_gradient_segment_le_riesz_integral {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {u : Vec d → ℝ} (huDiff : ContDiff ℝ 1 u) {x : Vec d} (hx : x ∈ U) : ∫ (t : ℝ) in 0..1, ∫ (y : Vec d) in U, ‖fderiv ℝ u (segmentBlend x t y)‖ * ‖x - y‖ ≤ (2 * Classical.choose ⋯) ^ d / ↑d * ∫ (z : Vec d) in U, ‖fderiv ℝ u z‖ * rieszKernel x z

theorem CKN.integral_gradient_segment_le_riesz_integral {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {u : Vec d → ℝ} (huDiff : ContDiff ℝ 1 u) {x : Vec d} (hx : x ∈ U) : ∫ (y : Vec d) in U, ∫ (t : ℝ) in 0..1, ‖fderiv ℝ u (segmentBlend x t y)‖ * ‖x - y‖ ≤ (2 * Classical.choose ⋯) ^ d / ↑d * ∫ (z : Vec d) in U, ‖fderiv ℝ u z‖ * rieszKernel x z

theorem CKN.norm_sub_average_le_gradient_riesz_integral {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) {x : Vec d} (hx : x ∈ U) (hvol : 0 < (MeasureTheory.volume U).toReal) : ‖u x - integralAverage U u‖ ≤ (MeasureTheory.volume U).toReal⁻¹ * ((2 * Classical.choose ⋯) ^ d / ↑d * ∫ (z : Vec d) in U, ‖fderiv ℝ u z‖ * rieszKernel x z)

theorem CKN.integral_rpow_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) {p : ℝ} (hp : 1 < p) (hvol : 0 < (MeasureTheory.volume U).toReal) : ∫ (x : Vec d) in U, ‖u x - integralAverage U u‖ ^ p ≤ ((MeasureTheory.volume U).toReal⁻¹ * ((2 * Classical.choose ⋯) ^ d / ↑d)) ^ p * ((↑d * (MeasureTheory.volume (Metric.ball 0 1)).toReal * (4 * Classical.choose ⋯)) ^ p * ∫ (y : Vec d) in U, ‖fderiv ℝ u y‖ ^ p)