Heat Entropy Time

The regularized entropy integral differentiates along a smooth heat orbit.

theorem ESS.heatRegEnergy_integral_hasDerivAt {b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hb : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) (hbc : ∀ (i : Fin 3), HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) {t η : ℝ} (ht : 0 < t) (hη : 0 < η) : HasDerivAt (fun (s : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), heatRegEnergy η (heatConvVec3 s b x)) (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, heatRegTest η (heatConvVec3 t b x) i * CKN.Foundation.Heat.heatConv t (CKN.spatialLaplacian fun (y : CKN.Foundation.Parabolic.Vec3) => b y i) x) t

The regularized entropy integral differentiates along a smooth heat orbit.

theorem ESS.heatRegTest_comp_fderiv {η : ℝ} (hη : 0 < η) {h : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {x v : CKN.Foundation.Parabolic.Vec3} (hh : DifferentiableAt ℝ h x) (i : Fin 3) : (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => heatRegTest η (h y) i) x) v = (heatRegSq η (h x) ^ (1 / 2) - η) * (fderiv ℝ h x) v i + heatRegSq η (h x) ^ (-(1 / 2)) * heatRegDot (h x) ((fderiv ℝ h x) v) * h x i

The spatial derivative of the regularized entropy test along a smooth field.

theorem ESS.heatRegTest_comp_dissipation_nonneg {η : ℝ} (hη : 0 < η) {h : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {x v : CKN.Foundation.Parabolic.Vec3} (hh : DifferentiableAt ℝ h x) : 0 ≤ ∑ i : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => heatRegTest η (h y) i) x) v * (fderiv ℝ h x) v i

The regularized entropy-test derivative has nonnegative pairing with the directional derivative of a smooth vector field.

theorem ESS.heatRegTest_fderiv_abs_bound {η M D : ℝ} (hη : 0 < η) (hM : 0 ≤ M) (hD : 0 ≤ D) {v w : CKN.Foundation.Parabolic.Vec3} (hv : CKN.Foundation.Parabolic.vec3EuclideanNorm v ≤ M) (hw : ∀ (i : Fin 3), |w i| ≤ D) (i : Fin 3) : |(fderiv ℝ (fun (z : CKN.Foundation.Parabolic.Vec3) => heatRegTest η z i) v) w| ≤ M * D + 3 * M ^ 2 * D / η

A pointwise derivative bound for the regularized entropy test on bounded vectors and directions.