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

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

Smooth segment estimates for convex-domain Poincare

This file begins the genuinely analytic side of the convex-domain Poincare proof. The first step is the fundamental theorem of calculus along the affine segment joining y to x, expressed with the project-local map segmentBlend x t y = y + t • (x - y).

Unlike the ball proof in the De Giorgi development, these lemmas are not tied to any radial parametrization. They are the smooth, domain-agnostic segment estimates that the later convex-domain L^p argument will integrate in y and then in x.

theorem HCPolySupport.sub_eq_integral_fderiv_along_segment {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (x y : Vec d) : u x - u y = ∫ (t : ℝ) in 0..1, (fderiv ℝ u (segmentBlend x t y)) (x - y)

theorem HCPolySupport.norm_sub_le_integral_fderiv_along_segment {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (x y : Vec d) : ‖u x - u y‖ ≤ ∫ (t : ℝ) in 0..1, ‖(fderiv ℝ u (segmentBlend x t y)) (x - y)‖

theorem HCPolySupport.norm_sub_le_integral_norm_fderiv_mul_norm_sub_along_segment {d : ℕ} {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (x y : Vec d) : ‖u x - u y‖ ≤ ∫ (t : ℝ) in 0..1, ‖fderiv ℝ u (segmentBlend x t y)‖ * ‖x - y‖

theorem HCPolySupport.integral_derivativeDistanceAlongSegment_le_twoChoose_mul_segmentDerivativeNorm {d : ℕ} {U : Set (Vec d)} (hU : IsBoundedDomain U) {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) {x y : Vec d} (hx : x ∈ U) (hy : y ∈ U) : ∫ (t : ℝ) in 0..1, ‖fderiv ℝ u (segmentBlend x t y)‖ * ‖x - y‖ ≤ 2 * Classical.choose hU * ∫ (t : ℝ) in 0..1, ‖fderiv ℝ u (segmentBlend x t y)‖