Subordination #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
The third spatial derivative is integrated in the heat-time variable. This is the explicit kernel corresponding to a degree-one pressure multiplier.
noncomputable def
CKN.Foundation.Heat.subordinatedKernel
(j l m : Fin 3)
(x : Parabolic.Vec3)
(t : ℝ)
:
Subordinated third-derivative heat kernel, integrated over times above the current time.
Equations
Instances For
noncomputable def
CKN.Foundation.Heat.subordinatedKernelSpatialDerivative
(j l m i : Fin 3)
(x : Parabolic.Vec3)
(t : ℝ)
:
Spatial derivative of the subordinated kernel via the fourth heat-kernel derivative.
Equations
Instances For
theorem
CKN.Foundation.Heat.subordinatedKernel_causal
{j l m : Fin 3}
{x : Parabolic.Vec3}
{t : ℝ}
(ht : t ≤ 0)
:
theorem
CKN.Foundation.Heat.subordinatedKernel_integrable
{j l m : Fin 3}
{x : Parabolic.Vec3}
{t : ℝ}
(ht : 0 < t)
:
MeasureTheory.IntegrableOn (fun (s : ℝ) => heatKernelSpaceThirdDerivative x s m j l) (Set.Ioi t) MeasureTheory.volume
theorem
CKN.Foundation.Heat.subordinatedKernel_abs_le_rho_inv_four
{j l m : Fin 3}
{x : Parabolic.Vec3}
{t : ℝ}
(ht : 0 < t)
:
theorem
CKN.Foundation.Heat.subordinatedKernelSpatialDerivative_abs_le_rho_inv_five
{j l m i : Fin 3}
{x : Parabolic.Vec3}
{t : ℝ}
(ht : 0 < t)
:
theorem
CKN.Foundation.Heat.subordinatedKernel_timeDerivative_abs_le_rho_inv_six
{j l m : Fin 3}
{x : Parabolic.Vec3}
{t : ℝ}
(ht : 0 < t)
:
theorem
CKN.Foundation.Heat.subordinatedKernelSpatialDerivative_causal
{j l m i : Fin 3}
{x : Parabolic.Vec3}
{t : ℝ}
(ht : t ≤ 0)
:
theorem
CKN.Foundation.Heat.subordinatedKernel_two_point_abs_le
{j l m : Fin 3}
{x y : Parabolic.Vec3}
{t R : ℝ}
(ht : 0 < t)
(hR : 0 < R)
(hx : R ≤ rhoTwo x t)
(hy : R ≤ rhoTwo y t)
: