Kernel Segment

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

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.

instance CKN.instNontrivialVecSegCV (d : ℕ) [NeZero d] : Nontrivial (Vec d)

File-level typeclass cache for Nontrivial (Vec d) under [NeZero d]. Repeated inference of this head class dominates the file (~7s cumulative typeclass before the cache). The cache fires during elaboration of theorems in this section even when their type signatures don't use [NeZero d], because the variable-block instance is in scope for typeclass search.

theorem CKN.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 CKN.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‖