Kernel Basic

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

Riesz-kernel tools for convex-domain Poincare — basic estimates

This file defines the Riesz kernel (x, y) ↦ ‖x - y‖^(1 - d) and establishes its basic positivity, symmetry, and ball-localised L¹ bounds. The bounded- domain L¹ size is controlled by the radius of IsBoundedDomain.

noncomputable def CKN.rieszKernel {d : ℕ} (x y : Vec d) : ℝ

The order-1 Riesz kernel in dimension d.

Equations

• CKN.rieszKernel x y = ‖x - y‖ ^ (1 - ↑d)

theorem CKN.rieszKernel_nonneg {d : ℕ} (x y : Vec d) : 0 ≤ rieszKernel x y

theorem CKN.rieszKernel_symm {d : ℕ} (x y : Vec d) : rieszKernel x y = rieszKernel y x

instance CKN.instNontrivialVecNeZero {d : ℕ} [NeZero d] : Nontrivial (Vec d)

Cache Nontrivial (Vec d) once per section so tactic-level typeclass searches don't rediscover the NeZero → Nonempty → Nontrivial chain.

theorem CKN.rieszKernel_integrableOn_ball {d : ℕ} [NeZero d] {R : ℝ} : 0 < R → MeasureTheory.IntegrableOn (fun (x : Vec d) => ‖x‖ ^ (1 - ↑d)) (Metric.ball 0 R) MeasureTheory.volume

theorem CKN.integrableOn_rieszKernel_ball {d : ℕ} [NeZero d] {R : ℝ} (hR : 0 < R) (x : Vec d) (hx : x ∈ Metric.ball 0 R) : MeasureTheory.IntegrableOn (fun (y : Vec d) => rieszKernel x y) (Metric.ball 0 R) MeasureTheory.volume

theorem CKN.integral_rieszKernel_ball_le {d : ℕ} [NeZero d] {R : ℝ} (hR : 0 < R) (x : Vec d) (hx : x ∈ Metric.ball 0 R) : ∫ (y : Vec d) in Metric.ball 0 R, rieszKernel x y ≤ ↑d * (MeasureTheory.volume (Metric.ball 0 1)).toReal * (2 * R)

instance CKN.instNontrivialVecBounded {d : ℕ} [NeZero d] : Nontrivial (Vec d)

Cache Nontrivial (Vec d) once per section.

theorem CKN.IsBoundedDomain.integrableOn_rieszKernel {d : ℕ} {U : Set (Vec d)} [NeZero d] (hU : IsBoundedDomain U) {x : Vec d} (hx : x ∈ U) : MeasureTheory.IntegrableOn (fun (y : Vec d) => rieszKernel x y) U MeasureTheory.volume

theorem CKN.IsBoundedDomain.integral_rieszKernel_le {d : ℕ} {U : Set (Vec d)} [NeZero d] (hU : IsBoundedDomain U) {x : Vec d} (hx : x ∈ U) : ∫ (y : Vec d) in U, rieszKernel x y ≤ ↑d * (MeasureTheory.volume (Metric.ball 0 1)).toReal * (4 * Classical.choose hU)

theorem CKN.IsBoundedDomain.integrableOn_rieszKernel_right {d : ℕ} {U : Set (Vec d)} [NeZero d] (hU : IsBoundedDomain U) {y : Vec d} (hy : y ∈ U) : MeasureTheory.IntegrableOn (fun (x : Vec d) => rieszKernel x y) U MeasureTheory.volume

theorem CKN.IsBoundedDomain.integral_rieszKernel_right_le {d : ℕ} {U : Set (Vec d)} [NeZero d] (hU : IsBoundedDomain U) {y : Vec d} (hy : y ∈ U) : ∫ (x : Vec d) in U, rieszKernel x y ≤ ↑d * (MeasureTheory.volume (Metric.ball 0 1)).toReal * (4 * Classical.choose hU)

theorem CKN.integrableOn_prod_rieszKernel_of_isSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} [NeZero d] (hU : IsSobolevRegularDomain U) : MeasureTheory.IntegrableOn (fun (z : Vec d × Vec d) => rieszKernel z.1 z.2) (U ×ˢ U) (MeasureTheory.volume.prod MeasureTheory.volume)