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

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

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 HCPolySupport.rieszKernel {d : ℕ} (x y : Vec d) : ℝ

The order-1 Riesz kernel in dimension d.

Equations

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

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

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

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

theorem HCPolySupport.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 HCPolySupport.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)

theorem HCPolySupport.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 HCPolySupport.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 HCPolySupport.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 HCPolySupport.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 HCPolySupport.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)