Coarse-graining support: Support.Sobolev.Foundations.PoincareLpKernel.SegmentChangeOfVariables

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

Segment change of variables for Riesz-kernel Poincare integrals

Pulls the segment-blend integrand φ(segmentBlend x t y) * ‖x - y‖ through a dilation change of variables into an integral against (1 - t)^(-(d+1)), optionally localised to a closed ball around x.

theorem HCPolySupport.setIntegral_segmentBlend_mul_norm_sub_eq_inv_pow_mul_setIntegral_scaled {d : ℕ} {U : Set (Vec d)} (hU_meas : MeasurableSet U) {x : Vec d} {t : ℝ} (ht1 : t < 1) {φ : Vec d → ℝ} : ∫ (y : Vec d) in U, φ (segmentBlend x t y) * ‖x - y‖ = ((1 - t) ^ (d + 1))⁻¹ * ∫ (z : Vec d) in translateSet x ((1 - t) • translateSet (-x) U), φ z * ‖z - x‖

theorem HCPolySupport.setIntegral_segmentBlend_mul_norm_sub_le_inv_pow_mul_setIntegral {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {x : Vec d} (hx : x ∈ U) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t < 1) {φ : Vec d → ℝ} (hφ_int : MeasureTheory.IntegrableOn (fun (z : Vec d) => φ z * ‖x - z‖) U MeasureTheory.volume) (hφ_nonneg : ∀ (z : Vec d), 0 ≤ φ z) : ∫ (y : Vec d) in U, φ (segmentBlend x t y) * ‖x - y‖ ≤ ((1 - t) ^ (d + 1))⁻¹ * ∫ (z : Vec d) in U, φ z * ‖x - z‖

theorem HCPolySupport.setIntegral_segmentBlend_mul_norm_sub_le_inv_pow_mul_setIntegral_inter_closedBall {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {x : Vec d} (hx : x ∈ U) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t < 1) {φ : Vec d → ℝ} (hφ_int : MeasureTheory.IntegrableOn (fun (z : Vec d) => φ z * ‖x - z‖) U MeasureTheory.volume) (hφ_nonneg : ∀ (z : Vec d), 0 ≤ φ z) : ∫ (y : Vec d) in U, φ (segmentBlend x t y) * ‖x - y‖ ≤ ((1 - t) ^ (d + 1))⁻¹ * ∫ (z : Vec d) in U ∩ Metric.closedBall x ((1 - t) * (2 * Classical.choose ⋯)), φ z * ‖x - z‖