Local integrability and continuity of translated-kernel integrals

Let k be a continuous kernel whose support lies in the closed ball of radius ε about the origin, so that k (· - y) is supported in the closed ball of radius ε about y. For a function g that is locally integrable on an open set Ω, the product x ↦ g x * k (x - y) is then integrable as soon as the ball closedBall y ε sits inside Ω, and the parametrised integral y ↦ ∫ x, g x * k (x - y) is continuous wherever the translated ball still fits inside Ω. These are the local-integrability and continuity inputs used in the Caffarelli–Kohn–Nirenberg paper (CKN) when a spatially localised kernel is slid against a locally integrable density.

theorem CKN.exists_delta_cthickening_subset {d : ℕ} {Ω : Set (Vec d)} (hΩ : IsOpen Ω) {ε : ℝ} {y₀ : Vec d} (hy₀ : Metric.closedBall y₀ ε ⊆ Ω) : ∃ (δ : ℝ), 0 < δ ∧ Metric.cthickening δ (Metric.closedBall y₀ ε) ⊆ Ω ∧ ∀ (y : Vec d), dist y y₀ ≤ δ → Metric.closedBall y ε ⊆ Metric.cthickening δ (Metric.closedBall y₀ ε)

Closed thickenings of a compact ball inside an open set. If the closed ball closedBall y₀ ε is contained in an open set Ω, then some positive radius δ has the property that the closed δ-thickening of that ball is still contained in Ω, and every translate of the ball whose centre lies within distance δ of y₀ is contained in that same thickening. This is the uniform room around closedBall y₀ ε used in the Caffarelli–Kohn–Nirenberg paper (CKN) to slide a localised kernel without leaving Ω.

theorem CKN.integrable_mul_translate {d : ℕ} {Ω : Set (Vec d)} {g k : Vec d → ℝ} (hg : MeasureTheory.LocallyIntegrableOn g Ω MeasureTheory.volume) (hk : Continuous k) {ε : ℝ} (hksupp : ∀ (z : Vec d), ε < ‖z‖ → k z = 0) {y : Vec d} (hy : Metric.closedBall y ε ⊆ Ω) : MeasureTheory.Integrable (fun (x : Vec d) => g x * k (x - y)) MeasureTheory.volume

Integrability of a translated kernel against a locally integrable function. If k is continuous and vanishes outside the closed ball of radius ε about the origin, and g is locally integrable on Ω, then for any closed ball closedBall y ε contained in Ω the product x ↦ g x * k (x - y) is integrable for Lebesgue measure. This is the local-integrability input in the Caffarelli–Kohn–Nirenberg paper (CKN) for a spatially localised kernel acted against a locally integrable density.

theorem CKN.continuousAt_integral_mul_translate {d : ℕ} {Ω : Set (Vec d)} (hΩ : IsOpen Ω) {g k : Vec d → ℝ} (hg : MeasureTheory.LocallyIntegrableOn g Ω MeasureTheory.volume) (hk : Continuous k) {ε : ℝ} (hksupp : ∀ (z : Vec d), ε < ‖z‖ → k z = 0) {y₀ : Vec d} (hy₀ : Metric.closedBall y₀ ε ⊆ Ω) : ContinuousAt (fun (y : Vec d) => ∫ (x : Vec d), g x * k (x - y)) y₀

Continuity of the translated-kernel integral. If k is continuous and vanishes outside the closed ball of radius ε about the origin, g is locally integrable on the open set Ω, and closedBall y₀ ε ⊆ Ω, then the parametrised integral y ↦ ∫ x, g x * k (x - y) is continuous at y₀. This is the continuity input in the Caffarelli–Kohn–Nirenberg paper (CKN) that lets a localised kernel be slid against a locally integrable density.