Far Shell #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.Core.HeatPotential.measurable_heatPotentialSpatialKernel_translate
(i : Fin 3)
(w : Foundation.Parabolic.ParabolicPoint)
:
Measurable fun (v : Foundation.Parabolic.ParabolicPoint) => heatPotentialSpatialKernel i w v
def
CKN.Core.HeatPotential.heatPotentialFarShellSet
(z : Foundation.Parabolic.ParabolicPoint)
(r : ℝ)
(j : ℕ)
:
Far parabolic shell with the six-scale separation used in heat-kernel difference estimates.
Equations
Instances For
theorem
CKN.Core.HeatPotential.measurableSet_heatPotentialFarShellSet
(z : Foundation.Parabolic.ParabolicPoint)
(r : ℝ)
(j : ℕ)
:
theorem
CKN.Core.HeatPotential.heatPotential_far_shell_source_l1_bound
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
{z : Foundation.Parabolic.ParabolicPoint}
{r P θ : ℝ}
(hr : 0 < r)
(hP : 1 ≤ P)
(hPθ : P ≤ θ)
(hF : AEMeasurable F MeasureTheory.volume)
(j : ℕ)
:
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in heatPotentialFarShellSet z r j, ENNReal.ofReal |F w| ≤ ENNReal.ofReal (2 * (2 ^ (↑(↑j + 6) + 1) * r)) ^ (5 * (1 - 1 / θ)) * MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 1) ^ (1 - 1 / P) * Foundation.Parabolic.Morrey.morreyNorm P θ F
theorem
CKN.Core.HeatPotential.heatPotential_far_shell_kernel_separation
{z w v : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
{j : ℕ}
(hr : 0 < r)
(hw : w ∈ Metric.closedBall z r)
(hv : v ∈ heatPotentialFarShellSet z r j)
:
theorem
CKN.Core.HeatPotential.heatPotential_far_shell_rho_separation
{z w v : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
{j : ℕ}
(hr : 0 < r)
(hw : w ∈ Metric.closedBall z r)
(hv : v ∈ heatPotentialFarShellSet z r j)
:
theorem
CKN.Core.HeatPotential.heatPotential_spatial_kernel_difference_abs_le
{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))
:
|heatPotentialKernel p v - heatPotentialKernel (p'.1, p.2) v| ≤ 900000 / R ^ 4 * Foundation.Parabolic.vec3EuclideanNorm (p.1 - p'.1)
theorem
CKN.Core.HeatPotential.heatPotential_spatial_kernel_spatial_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.heatPotential_time_kernel_difference_abs_le
{p p' v : Foundation.Parabolic.ParabolicPoint}
{R : ℝ}
(hR : 0 < R)
(hp : p.2 ≤ p'.2)
(ht : 0 ≤ p.2 - v.2)
(hsep : ∀ s ∈ Set.Icc p.2 p'.2, R ≤ Foundation.Heat.rhoTwo (p'.1 - v.1) (s - v.2))
:
theorem
CKN.Core.HeatPotential.heatPotential_far_shell_spatial_kernel_difference_abs_le
{z p p' v : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
{j : ℕ}
(hr : 0 < r)
(hp : p ∈ Metric.closedBall z r)
(hp' : p' ∈ Metric.closedBall z r)
(hv : v ∈ heatPotentialFarShellSet z r j)
:
theorem
CKN.Core.HeatPotential.heatPotential_far_shell_spatial_kernel_spatial_difference_abs_le
{i : Fin 3}
{z p p' v : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
{j : ℕ}
(hr : 0 < r)
(hp : p ∈ Metric.closedBall z r)
(hp' : p' ∈ Metric.closedBall z r)
(hv : v ∈ heatPotentialFarShellSet z r j)
:
theorem
CKN.Core.HeatPotential.heatPotential_far_shell_kernel_abs_le
{z w v : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
{j : ℕ}
(hr : 0 < r)
(hw : w ∈ Metric.closedBall z r)
(hv : v ∈ heatPotentialFarShellSet z r j)
:
theorem
CKN.Core.HeatPotential.heatPotential_far_shell_spatial_kernel_abs_le
{i : Fin 3}
{z w v : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
{j : ℕ}
(hr : 0 < r)
(hw : w ∈ Metric.closedBall z r)
(hv : v ∈ heatPotentialFarShellSet z r j)
:
theorem
CKN.Core.HeatPotential.heatPotential_spatial_time_kernel_difference_abs_le
{i : Fin 3}
{p p' v : Foundation.Parabolic.ParabolicPoint}
{R : ℝ}
(hR : 0 < R)
(hp : p.2 ≤ p'.2)
(ht : 0 ≤ p.2 - v.2)
(hsep : ∀ s ∈ Set.Icc p.2 p'.2, R ≤ Foundation.Heat.rhoTwo (p'.1 - v.1) (s - v.2))
: