Spatial derivatives of the heat orbit of an L² datum

At a positive time the Gaussian convolution of an L² datum is differentiable, and its derivative is the convolution with the kernel derivative: smooth compactly supported approximants have this property, and their derivatives converge uniformly by the Cauchy–Schwarz bound for the kernel derivative. Consequently the heat orbit of a datum in J has measurable classical gradient on every slab, this gradient is a weak gradient at each positive time, and the heat orbit is divergence free. These are the measurability, weak-gradient and divergence clauses of the heat orbit in prop:pv-local-solution.

theorem ESS.heatConv_hasFDerivAt_of_memLp {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) {t : ℝ} (ht : 0 < t) (x : CKN.Foundation.Parabolic.Vec3) : HasFDerivAt (CKN.Foundation.Heat.heatConv t f) (∑ j : Fin 3, heatConvGrad t f j x • ContinuousLinearMap.proj j) x

At a positive time the Gaussian convolution of an L² datum is differentiable, with derivative given by convolution with the kernel derivatives.

theorem ESS.heatConv_fderiv_basisVec_of_memLp {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) {t : ℝ} (ht : 0 < t) (x : CKN.Foundation.Parabolic.Vec3) (j : Fin 3) : (fderiv ℝ (CKN.Foundation.Heat.heatConv t f) x) (CKN.basisVec j) = heatConvGrad t f j x

At a positive time the jth classical derivative of the Gaussian convolution of an L² datum is heatConvGrad.

theorem ESS.heatOrbit_spatialDeriv_eq {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) {t : ℝ} (ht : 0 < t) (x : CKN.Foundation.Parabolic.Vec3) (i j : Fin 3) : CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatOrbit a (y, t) i) j x = heatConvGrad t (fun (y : CKN.Foundation.Parabolic.Vec3) => a y i) j x

At a positive time the classical spatial derivatives of the heat orbit of an L² datum are the kernel-derivative convolutions of its components.

theorem ESS.isInJ_component_approx {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (ha : CKN.IsInJ a) : ∃ (aSeq : ℕ → CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3), (∀ (k : ℕ) (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => aSeq k x i) ∧ (∀ (k : ℕ) (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => aSeq k x i) ∧ (∀ (k : ℕ) (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => aSeq k y i) i x = 0) ∧ (∀ (i : Fin 3), Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm ((fun (x : CKN.Foundation.Parabolic.Vec3) => aSeq k x i) - fun (x : CKN.Foundation.Parabolic.Vec3) => a x i) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) ∧ Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => aSeq k x - a x) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

The smooth divergence-free approximants of a datum in J, component by component: each component is smooth, compactly supported and square integrable, and converges in L² to the corresponding component of the datum.

theorem ESS.heatOrbit_grad_aestronglyMeasurable {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (ha : CKN.IsInJ a) (τ : ℝ) : MeasureTheory.AEStronglyMeasurable (heatOrbit a) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ))) ∧ MeasureTheory.AEStronglyMeasurable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatOrbit a (y, z.2) i) j z.1) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 τ)))

(h1) The heat orbit of a datum in J and its classical spatial gradient are almost everywhere strongly measurable on every slab ℝ³ × (0, τ).

theorem ESS.heatOrbit_hasWeakGradientOn {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (ha : CKN.IsInJ a) {t : ℝ} (ht : 0 < t) (i : Fin 3) : CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => heatOrbit a (x, t) i) fun (x : CKN.Vec 3) (j : Fin 3) => CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatOrbit a (y, t) i) j x

(h4) At each positive time the classical spatial gradient of each component of the heat orbit of a datum in J is its weak gradient on ℝ³.

theorem ESS.heatOrbit_div_eq_zero {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (ha : CKN.IsInJ a) {t : ℝ} (ht : 0 < t) (x : CKN.Foundation.Parabolic.Vec3) : ∑ i : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatOrbit a (y, t) i) i x = 0

At each positive time the heat orbit of a datum in J is pointwise divergence free.

theorem ESS.heatOrbit_weak_div_eq_zero {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (ha : CKN.IsInJ a) {t : ℝ} (ht : 0 < t) (ψ : CKN.WeakTestFunction Set.univ) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, heatOrbit a (x, t) i * ψ.partialDeriv i x = 0

(h5) At each positive time the heat orbit of a datum in J is weakly divergence free on ℝ³.