Far #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.Core.HeatPotential.heatKernel_fderiv_bound
{x : Foundation.Parabolic.Vec3}
{t R : ℝ}
(ht : 0 < t)
(hR : 0 < R)
(hsep : R ≤ Foundation.Heat.rhoTwo x t)
:
‖fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => Foundation.Heat.heatKernel y t) x‖ ≤ 900000 / R ^ 4
theorem
CKN.Core.HeatPotential.heatPotential_spatial_derivative_kernel_difference_abs_le
{i : Fin 3}
{p p' v : Foundation.Parabolic.ParabolicPoint}
{R : ℝ}
(hR : 0 < R)
(ht : 0 < p.2 - v.2)
(hsep : ∀ y ∈ segment ℝ p.1 p'.1, R ≤ Foundation.Heat.rhoTwo (y - v.1) (p.2 - v.2))
:
|heatPotentialSpatialKernel i p v - heatPotentialSpatialKernel i (p'.1, p.2) v| ≤ 60000000 / R ^ 5 * Foundation.Parabolic.vec3EuclideanNorm (p.1 - p'.1)
theorem
CKN.Core.HeatPotential.parabolic_ball_segment_mem
{z p p' y : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
(hp : p ∈ Metric.closedBall z r)
(hp' : p' ∈ Metric.closedBall z r)
(hy : y.1 ∈ segment ℝ p.1 p'.1)
(hytime : y.2 = p.2)
:
theorem
CKN.Core.HeatPotential.parabolic_ball_time_segment_mem
{z p p' : Foundation.Parabolic.ParabolicPoint}
{x : Foundation.Parabolic.Vec3}
{r s : ℝ}
(hr : 0 ≤ r)
(hp : p ∈ Metric.closedBall z r)
(hp' : p' ∈ Metric.closedBall z r)
(hx : Foundation.Parabolic.vec3EuclideanNorm (x - z.1) ≤ r)
(hs : s ∈ Set.Icc p.2 p'.2)
:
The source shells used by the far part start six dyadic scales outside the observation ball. The larger gap makes the causal kernel separation uniform after moving the observation point inside its ball.