Interior

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

Harmonic interior estimates from the Newtonian representation

Kernel and integration-by-parts infrastructure for the representation route.

theorem CKN.Foundation.Heat.newtonianKernel_spatialDeriv_second_size_bound {z : Parabolic.Vec3} (hz : z ≠ 0) (i j : Fin 3) : |spatialDeriv (spatialDeriv newtonianKernel i) j z| ≤ 4 * (4 * Real.pi)⁻¹ * (‖z‖ ^ 3)⁻¹

theorem CKN.Foundation.Heat.newtonianKernel_spatialDeriv_size_bound {z : Parabolic.Vec3} (hz : z ≠ 0) (i : Fin 3) : |spatialDeriv newtonianKernel i z| ≤ (4 * Real.pi)⁻¹ * (‖z‖ ^ 2)⁻¹

theorem CKN.Foundation.Heat.spatialDeriv_newtonianKernel_shift_eq_neg {x y : Parabolic.Vec3} (hxy : x - y ≠ 0) (i : Fin 3) : spatialDeriv (fun (z : Parabolic.Vec3) => newtonianKernel (x - z)) i y = -spatialDeriv newtonianKernel i (x - y)

theorem CKN.Foundation.Heat.spatialDeriv_kernelCutoffDerivative_at_x {x x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hx : x ∈ euclideanBall x₀ (13 * ρ / 20)) (i j : Fin 3) : spatialDeriv (kernelCutoffDerivative x x₀ hρ i) j x = 0

theorem CKN.Foundation.Heat.spatialDeriv_kernelCutoffDerivative_of_ne {x x₀ y : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hxy : x - y ≠ 0) (i j : Fin 3) : spatialDeriv (kernelCutoffDerivative x x₀ hρ i) j y = spatialDeriv (fun (z : Parabolic.Vec3) => newtonianKernel (x - z)) j y * spatialDeriv (eta x₀ hρ) i y + newtonianKernel (x - y) * spatialDeriv (spatialDeriv (eta x₀ hρ) i) j y

theorem CKN.Foundation.Heat.kernelCutoffDerivative_contDiff_one (x x₀ : Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (hx : x ∈ euclideanBall x₀ (13 * ρ / 20)) (i : Fin 3) : ContDiff ℝ (↑1) (kernelCutoffDerivative x x₀ hρ i)

theorem CKN.Foundation.Heat.kernelCutoffDerivative_hasCompactSupport_global (x x₀ : Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (i : Fin 3) : HasCompactSupport (kernelCutoffDerivative x x₀ hρ i)

theorem CKN.Foundation.Heat.kernelCutoffDerivative_integrable_mul_right_global {h : Parabolic.Vec3 → ℝ} (hh : ContDiff ℝ (↑⊤) h) (x x₀ : Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (hx : x ∈ euclideanBall x₀ (13 * ρ / 20)) (i : Fin 3) : MeasureTheory.Integrable (fun (y : Parabolic.Vec3) => h y * spatialDeriv (kernelCutoffDerivative x x₀ hρ i) i y) MeasureTheory.volume

theorem CKN.Foundation.Heat.eta_spatialDeriv_contDiff_two_global (x₀ : Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (i : Fin 3) : ContDiff ℝ (↑2) (spatialDeriv (eta x₀ hρ) i)

theorem CKN.Foundation.Heat.eta_spatialSecond_continuous_global (x₀ : Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (i : Fin 3) : Continuous (spatialDeriv (spatialDeriv (eta x₀ hρ) i) i)

theorem CKN.Foundation.Heat.smooth_harmonic_annular_representation_on_outer {H : Parabolic.Vec3 → ℝ} (hH : ContDiff ℝ (↑⊤) H) {x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hHarm : ∀ y ∈ euclideanBall x₀ (3 * ρ / 4), spatialLaplacian H y = 0) {x : Parabolic.Vec3} (hx : x ∈ euclideanBall x₀ (13 * ρ / 20)) : H x = (-∫ (y : Parabolic.Vec3), newtonianKernel (x - y) * (H y * spatialLaplacian (eta x₀ hρ) y)) + 2 * ∑ i : Fin 3, ∫ (y : Parabolic.Vec3), H y * spatialDeriv (kernelCutoffDerivative x x₀ hρ i) i y

A smooth harmonic function is represented in an inner ball by the annular terms obtained from the Newtonian representation and a mollified ball cutoff.

theorem CKN.Foundation.Heat.smooth_harmonic_annular_representation {H : Parabolic.Vec3 → ℝ} (hH : ContDiff ℝ (↑⊤) H) {x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (hHarm : ∀ y ∈ euclideanBall x₀ ρ, spatialLaplacian H y = 0) {x : Parabolic.Vec3} (hx : x ∈ euclideanBall x₀ (ρ / 4)) : H x = (-∫ (y : Parabolic.Vec3), newtonianKernel (x - y) * (H y * spatialLaplacian (eta x₀ hρ) y)) + 2 * ∑ i : Fin 3, ∫ (y : Parabolic.Vec3), H y * spatialDeriv (kernelCutoffDerivative x x₀ hρ i) i y