Kernel Time

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

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

File-level instance providing Nontrivial (Vec d) under [NeZero d].

Time-collapse estimates for the Riesz-kernel Poincare integrand

Collects the intervalIntegral-level lemmas that bound the time-averaged segment-blend integrand against rieszKernel.

theorem CKN.intervalIntegral_inv_pow_if_norm_sub_le_mul_le_rieszKernel {d : ℕ} [NeZero d] {x z : Vec d} {R : ℝ} (hR : 0 < R) : (∫ (t : ℝ) in 0..1, ((1 - t) ^ (d + 1))⁻¹ * if ‖x - z‖ ≤ (1 - t) * R then ‖x - z‖ else 0) ≤ R ^ d / ↑d * rieszKernel x z

theorem CKN.setIntegral_inv_pow_setIntegral_inter_closedBall_le_rieszKernel {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU_meas : MeasurableSet U) {x : Vec d} {R : ℝ} (hR : 0 < R) {φ : Vec d → ℝ} (hφ_nonneg : ∀ (z : Vec d), 0 ≤ φ z) (hφ_meas : AEMeasurable φ (MeasureTheory.volume.restrict U)) (hφK_int : MeasureTheory.IntegrableOn (fun (z : Vec d) => φ z * rieszKernel x z) U MeasureTheory.volume) : ∫ (t : ℝ) in Set.Ioc 0 1, ((1 - t) ^ (d + 1))⁻¹ * ∫ (z : Vec d) in U ∩ Metric.closedBall x ((1 - t) * R), φ z * ‖x - z‖ ≤ R ^ d / ↑d * ∫ (z : Vec d) in U, φ z * rieszKernel x z

theorem CKN.intervalIntegrable_inv_pow_setIntegral_inter_closedBall {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU_meas : MeasurableSet U) {x : Vec d} {R : ℝ} (hR : 0 < R) {φ : Vec d → ℝ} (hφ_nonneg : ∀ (z : Vec d), 0 ≤ φ z) (hφ_meas : AEMeasurable φ (MeasureTheory.volume.restrict U)) (hφK_int : MeasureTheory.IntegrableOn (fun (z : Vec d) => φ z * rieszKernel x z) U MeasureTheory.volume) : IntervalIntegrable (fun (t : ℝ) => ((1 - t) ^ (d + 1))⁻¹ * ∫ (z : Vec d) in U ∩ Metric.closedBall x ((1 - t) * R), φ z * ‖x - z‖) MeasureTheory.volume 0 1

theorem CKN.intervalIntegral_inv_pow_setIntegral_inter_closedBall_le_rieszKernel {d : ℕ} [NeZero d] {U : Set (Vec d)} (hU_meas : MeasurableSet U) {x : Vec d} {R : ℝ} (hR : 0 < R) {φ : Vec d → ℝ} (hφ_nonneg : ∀ (z : Vec d), 0 ≤ φ z) (hφ_meas : AEMeasurable φ (MeasureTheory.volume.restrict U)) (hφK_int : MeasureTheory.IntegrableOn (fun (z : Vec d) => φ z * rieszKernel x z) U MeasureTheory.volume) : ∫ (t : ℝ) in 0..1, ((1 - t) ^ (d + 1))⁻¹ * ∫ (z : Vec d) in U ∩ Metric.closedBall x ((1 - t) * R), φ z * ‖x - z‖ ≤ R ^ d / ↑d * ∫ (z : Vec d) in U, φ z * rieszKernel x z