Interior Basic

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.

def CKN.Foundation.Heat.q (z : Parabolic.Vec3) : ℝ

Squared Euclidean radius in native three-dimensional coordinates.

Equations

• CKN.Foundation.Heat.q z = ∑ i : Fin 3, z i ^ 2

theorem CKN.Foundation.Heat.q_pos {z : Parabolic.Vec3} (hz : z ≠ 0) : 0 < q z

theorem CKN.Foundation.Heat.q_eq_vec3Norm_sq (z : Parabolic.Vec3) : q z = Parabolic.vec3EuclideanNorm z ^ 2

theorem CKN.Foundation.Heat.hasFDerivAt_newtonianKernel {z : Parabolic.Vec3} (hz : z ≠ 0) : HasFDerivAt newtonianKernel ((4 * Real.pi)⁻¹ • (-1 / 2 * q z ^ (-1 / 2 - 1)) • ∑ i : Fin 3, (2 * z i) • ContinuousLinearMap.proj i) z

theorem CKN.Foundation.Heat.spatialDeriv_newtonianKernel_shift {x y : Parabolic.Vec3} (hxy : x - y ≠ 0) (i : Fin 3) : spatialDeriv (fun (z : Parabolic.Vec3) => newtonianKernel (x - z)) i y = (4 * Real.pi)⁻¹ * (x - y) i * q (x - y) ^ (-3 / 2)

noncomputable def CKN.Foundation.Heat.kernelDerivative (i : Fin 3) (z : Parabolic.Vec3) : ℝ

First derivative of the normalized Newtonian kernel, defined as zero at its singularity.

Equations

• CKN.Foundation.Heat.kernelDerivative i z = if z = 0 then 0 else (4 * Real.pi)⁻¹ * z i * CKN.Foundation.Heat.q z ^ (-3 / 2)

noncomputable def CKN.Foundation.Heat.eta (x₀ : Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) : Parabolic.Vec3 → ℝ

The smooth cutoff used in the annular harmonic representation.

Equations

• CKN.Foundation.Heat.eta x₀ hρ = CKN.mollifiedBallCutoff x₀ hρ

noncomputable def CKN.Foundation.Heat.kernelCutoffDerivative (x x₀ : Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (i : Fin 3) (y : Parabolic.Vec3) : ℝ

The Newtonian kernel times one cutoff derivative.

Equations

• CKN.Foundation.Heat.kernelCutoffDerivative x x₀ hρ i y = CKN.Foundation.Heat.newtonianKernel (x - y) * CKN.spatialDeriv (CKN.Foundation.Heat.eta x₀ hρ) i y

theorem CKN.Foundation.Heat.contDiff_spatialDeriv_two {f : Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i : Fin 3) : ContDiff ℝ (↑2) (spatialDeriv f i)

theorem CKN.Foundation.Heat.spatialDeriv_eta_eventually_zero (x x₀ : Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (hx : x ∈ euclideanBall x₀ (13 * ρ / 20)) (i : Fin 3) : ∀ᶠ (y : Parabolic.Vec3) in nhds x, spatialDeriv (eta x₀ hρ) i y = 0

theorem CKN.Foundation.Heat.kernelCutoffDerivative_contDiff (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 (x x₀ : Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (i : Fin 3) : HasCompactSupport (kernelCutoffDerivative x x₀ hρ i)

theorem CKN.Foundation.Heat.kernelCutoffDerivative_integrable_mul_left {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) => spatialDeriv h i y * kernelCutoffDerivative x x₀ hρ i y) MeasureTheory.volume

theorem CKN.Foundation.Heat.kernelCutoffDerivative_integrable_mul_right {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.integral_h_mul_kernelCutoffDerivative_spatialDeriv {h : Parabolic.Vec3 → ℝ} (hh : ContDiff ℝ (↑⊤) h) (x x₀ : Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (hx : x ∈ euclideanBall x₀ (13 * ρ / 20)) (i : Fin 3) : ∫ (y : Parabolic.Vec3), h y * spatialDeriv (kernelCutoffDerivative x x₀ hρ i) i y = -∫ (y : Parabolic.Vec3), spatialDeriv h i y * kernelCutoffDerivative x x₀ hρ i y

theorem CKN.Foundation.Heat.newtonianKernel_mul_compact_integrable {f : Parabolic.Vec3 → ℝ} (hf : Continuous f) (hfSupport : HasCompactSupport f) (x : Parabolic.Vec3) : MeasureTheory.Integrable (fun (y : Parabolic.Vec3) => newtonianKernel (x - y) * f y) MeasureTheory.volume

theorem CKN.Foundation.Heat.newtonianKernel_mul_compact_integrable_global {f : Parabolic.Vec3 → ℝ} (hf : Continuous f) (hfSupport : HasCompactSupport f) (x : Parabolic.Vec3) : MeasureTheory.Integrable (fun (y : Parabolic.Vec3) => newtonianKernel (x - y) * f y) MeasureTheory.volume

theorem CKN.Foundation.Heat.laplacian_compact_support {f : Parabolic.Vec3 → ℝ} (hf : HasCompactSupport f) : HasCompactSupport (spatialLaplacian f)

theorem CKN.Foundation.Heat.laplacian_compact_support_global {f : Parabolic.Vec3 → ℝ} (hf : HasCompactSupport f) : HasCompactSupport (spatialLaplacian f)

theorem CKN.Foundation.Heat.newtonianKernel_size_bound {z : Parabolic.Vec3} (hz : z ≠ 0) : |newtonianKernel z| ≤ (4 * Real.pi)⁻¹ * ‖z‖⁻¹

theorem CKN.Foundation.Heat.newtonianKernel_continuousAt {z : Parabolic.Vec3} (hz : z ≠ 0) : ContinuousAt newtonianKernel z

theorem CKN.Foundation.Heat.newtonianKernel_hasFDerivAt {z : Parabolic.Vec3} (hz : z ≠ 0) : HasFDerivAt newtonianKernel (fderiv ℝ newtonianKernel z) z

theorem CKN.Foundation.Heat.newtonianKernel_spatialDeriv_formula {z : Parabolic.Vec3} (hz : z ≠ 0) (i : Fin 3) : spatialDeriv newtonianKernel i z = -(4 * Real.pi)⁻¹ * z i * q z ^ (-3 / 2)

theorem CKN.Foundation.Heat.newtonianKernel_spatialDeriv_second_formula {z : Parabolic.Vec3} (hz : z ≠ 0) (i j : Fin 3) : spatialDeriv (spatialDeriv newtonianKernel i) j z = -(4 * Real.pi)⁻¹ * ((if i = j then 1 else 0) * q z ^ (-3 / 2) + z i * (-3 / 2 * q z ^ (-3 / 2 - 1) * (2 * z j)))

theorem CKN.Foundation.Heat.hasFDerivAt_newtonianKernel_spatialDeriv_formula {z : Parabolic.Vec3} (hz : z ≠ 0) (i : Fin 3) : HasFDerivAt (spatialDeriv newtonianKernel i) (-(4 * Real.pi)⁻¹ • (z i • (-3 / 2 * q z ^ (-3 / 2 - 1)) • ∑ k : Fin 3, (2 * z k) • ContinuousLinearMap.proj k + q z ^ (-3 / 2) • ContinuousLinearMap.proj i)) z

theorem CKN.Foundation.Heat.newtonianKernel_spatialDeriv_continuousAt {z : Parabolic.Vec3} (hz : z ≠ 0) (i : Fin 3) : ContinuousAt (spatialDeriv newtonianKernel i) z

theorem CKN.Foundation.Heat.newtonianKernel_spatialDeriv_second_continuousAt {z : Parabolic.Vec3} (hz : z ≠ 0) (i j : Fin 3) : ContinuousAt (spatialDeriv (spatialDeriv newtonianKernel i) j) z