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

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

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 HCPolySupport.integrableOn_integral_norm_fderiv_along_segment_of_isSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) {u : Vec d → ℝ} (huDiff : ContDiff ℝ (↑⊤) u) (x : Vec d) : MeasureTheory.IntegrableOn (fun (y : Vec d) => ∫ (t : ℝ) in 0..1, ‖fderiv ℝ u (segmentBlend x t y)‖) U MeasureTheory.volume

theorem HCPolySupport.integrableOn_integral_norm_fderiv_mul_norm_sub_along_segment_of_isSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) {u : Vec d → ℝ} (huDiff : ContDiff ℝ (↑⊤) 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 HCPolySupport.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 ℝ (↑⊤) 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 HCPolySupport.distanceFromIntegralAverage_le_volumeAverage_segmentDerivativeDistance {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsSobolevRegularDomain U) {u : Vec d → ℝ} (hu : MeasureTheory.IntegrableOn u U MeasureTheory.volume) (huDiff : ContDiff ℝ (↑⊤) 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 HCPolySupport.intervalSetIntegral_segmentDerivativeDistance_le_rieszKernel {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {u : Vec d → ℝ} (huDiff : ContDiff ℝ (↑⊤) 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 HCPolySupport.setIntervalIntegral_segmentDerivativeDistance_le_rieszKernel {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {u : Vec d → ℝ} (huDiff : ContDiff ℝ (↑⊤) 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 HCPolySupport.averageDeviation_le_averageDerivativeNorm_mul_rieszKernel {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 ℝ (↑⊤) 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 HCPolySupport.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 ℝ (↑⊤) 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)

theorem HCPolySupport.norm_sub_integralAverage_le_two_mul_choose_mul_volumeAverage_integral_norm_fderiv_along_segment {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsSobolevRegularDomain U) {u : Vec d → ℝ} (hu : MeasureTheory.IntegrableOn u U MeasureTheory.volume) (huDiff : ContDiff ℝ (↑⊤) u) {x : Vec d} (hx : x ∈ U) (hvol : 0 < (MeasureTheory.volume U).toReal) (hsegmentMul : MeasureTheory.IntegrableOn (fun (y : Vec d) => ∫ (t : ℝ) in 0..1, ‖fderiv ℝ u (segmentBlend x t y)‖ * ‖x - y‖) U MeasureTheory.volume) (hsegment : MeasureTheory.IntegrableOn (fun (y : Vec d) => ∫ (t : ℝ) in 0..1, ‖fderiv ℝ u (segmentBlend x t y)‖) U MeasureTheory.volume) : ‖u x - integralAverage U u‖ ≤ (MeasureTheory.volume U).toReal⁻¹ * (2 * Classical.choose ⋯ * ∫ (y : Vec d) in U, ∫ (t : ℝ) in 0..1, ‖fderiv ℝ u (segmentBlend x t y)‖)

theorem HCPolySupport.averageDeviation_le_twoChoose_mul_averageSegmentDerivativeNorm {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsSobolevRegularDomain U) {u : Vec d → ℝ} (hu : MeasureTheory.IntegrableOn u U MeasureTheory.volume) (huDiff : ContDiff ℝ (↑⊤) 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 ⋯ * ∫ (y : Vec d) in U, ∫ (t : ℝ) in 0..1, ‖fderiv ℝ u (segmentBlend x t y)‖)