Heat Entropy

The squared regularized magnitude used in lem:pv-heat-critical.

def ESS.heatRegSq (η : ℝ) (v : CKN.Foundation.Parabolic.Vec3) : ℝ

The squared regularized magnitude used in lem:pv-heat-critical.

Equations

• ESS.heatRegSq η v = ∑ i : Fin 3, v i ^ 2 + η ^ 2

def ESS.heatRegDot (v w : CKN.Foundation.Parabolic.Vec3) : ℝ

The coordinate dot product used by the entropy derivatives in lem:pv-heat-critical.

Equations

• ESS.heatRegDot v w = ∑ i : Fin 3, v i * w i

theorem ESS.heatRegSq_differentiableAt (η : ℝ) (v : CKN.Foundation.Parabolic.Vec3) : DifferentiableAt ℝ (heatRegSq η) v

The regularized squared magnitude is differentiable, as used in the entropy chain rules for lem:pv-heat-critical.

theorem ESS.heatRegSq_pos {η : ℝ} (hη : 0 < η) (v : CKN.Foundation.Parabolic.Vec3) : 0 < heatRegSq η v

Positive regularization makes the squared magnitude strictly positive in lem:pv-heat-critical.

noncomputable def ESS.heatRegG (η : ℝ) (v : CKN.Foundation.Parabolic.Vec3) : ℝ

A smooth regularization of |v|^(3/2) used in lem:pv-heat-critical.

Equations

• ESS.heatRegG η v = ESS.heatRegSq η v ^ (3 / 4) - η ^ (3 / 2)

noncomputable def ESS.heatRegTest (η : ℝ) (v : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.Vec3

The regularized |v|v entropy test used in lem:pv-heat-critical.

Equations

• ESS.heatRegTest η v i = (ESS.heatRegSq η v ^ (1 / 2) - η) * v i

noncomputable def ESS.heatRegEnergy (η : ℝ) (v : CKN.Foundation.Parabolic.Vec3) : ℝ

The nonnegative convex potential paired with heatRegTest.

Equations

• ESS.heatRegEnergy η v = 1 / 3 * ESS.heatRegSq η v ^ (3 / 2) - η / 2 * ESS.heatRegSq η v + η ^ 3 / 6

theorem ESS.heatRegG_contDiff {η : ℝ} (hη : 0 < η) : ContDiff ℝ (↑⊤) (heatRegG η)

The regularized critical profile is smooth for positive regularization, as used in lem:pv-heat-critical.

theorem ESS.heatRegTest_contDiff {η : ℝ} (hη : 0 < η) : ContDiff ℝ (↑⊤) (heatRegTest η)

The regularized entropy test is smooth in the vector variable.

theorem ESS.heatRegEnergy_contDiff {η : ℝ} (hη : 0 < η) : ContDiff ℝ (↑⊤) (heatRegEnergy η)

The regularized entropy potential is smooth in the vector variable, as used in the energy argument for lem:pv-heat-critical.

theorem ESS.heatRegTest_fderiv {η : ℝ} (hη : 0 < η) (v w : CKN.Foundation.Parabolic.Vec3) (i : Fin 3) : (fderiv ℝ (fun (z : CKN.Foundation.Parabolic.Vec3) => heatRegTest η z i) v) w = (heatRegSq η v ^ (1 / 2) - η) * w i + heatRegSq η v ^ (-(1 / 2)) * heatRegDot v w * v i

The derivative of the regularized entropy test.

theorem ESS.heatRegEnergy_fderiv {η : ℝ} (hη : 0 < η) (v w : CKN.Foundation.Parabolic.Vec3) : (fderiv ℝ (heatRegEnergy η) v) w = (heatRegSq η v ^ (1 / 2) - η) * heatRegDot v w

The regularized energy derivative pairs with the regularized test, as used in lem:pv-heat-critical.

theorem ESS.heatRegG_fderiv {η : ℝ} (hη : 0 < η) (v w : CKN.Foundation.Parabolic.Vec3) : (fderiv ℝ (heatRegG η) v) w = 3 / 2 * heatRegSq η v ^ (-(1 / 4)) * heatRegDot v w

The regularized critical profile's vector derivative, used in the spatial chain rule for lem:pv-heat-critical.

theorem ESS.heatRegG_differentiableAt {η : ℝ} (hη : 0 < η) (v : CKN.Foundation.Parabolic.Vec3) : DifferentiableAt ℝ (heatRegG η) v

The regularized critical profile is differentiable for positive regularization in lem:pv-heat-critical.

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

The spatial derivative of the regularized critical profile along a smooth vector field, used in the dissipation estimate for lem:pv-heat-critical.

theorem ESS.heatRegTest_pairing {η : ℝ} (v w : CKN.Foundation.Parabolic.Vec3) : ∑ i : Fin 3, heatRegTest η v i * w i = (heatRegSq η v ^ (1 / 2) - η) * heatRegDot v w

The regularized test pairs with the vector derivative of its energy in lem:pv-heat-critical.

theorem ESS.heatRegTest_dissipation_identity {η : ℝ} (hη : 0 < η) (v w : CKN.Foundation.Parabolic.Vec3) : ∑ i : Fin 3, (fderiv ℝ (fun (z : CKN.Foundation.Parabolic.Vec3) => heatRegTest η z i) v) w * w i = (heatRegSq η v ^ (1 / 2) - η) * ∑ i : Fin 3, w i ^ 2 + heatRegSq η v ^ (-(1 / 2)) * heatRegDot v w ^ 2

The entropy test derivative has a nonnegative quadratic dissipation.

theorem ESS.heatRegTest_dissipation_lower {η : ℝ} (hη : 0 < η) (v w : CKN.Foundation.Parabolic.Vec3) : (heatRegSq η v ^ (1 / 2) - η) * ∑ i : Fin 3, w i ^ 2 ≤ ∑ i : Fin 3, (fderiv ℝ (fun (z : CKN.Foundation.Parabolic.Vec3) => heatRegTest η z i) v) w * w i

The entropy dissipation controls the regularized weighted gradient.

theorem ESS.heatReg_root_ge_eta {η : ℝ} (hη : 0 < η) (v : CKN.Foundation.Parabolic.Vec3) : η ≤ heatRegSq η v ^ (1 / 2)

The regularized Euclidean root is at least its positive offset.

theorem ESS.heatRegEnergy_factor {η : ℝ} (hη : 0 < η) (v : CKN.Foundation.Parabolic.Vec3) : heatRegEnergy η v = (heatRegSq η v ^ (1 / 2) - η) ^ 2 * (2 * heatRegSq η v ^ (1 / 2) + η) / 6

A nonnegative factorization of the regularized entropy potential.

theorem ESS.heatRegEnergy_nonneg {η : ℝ} (hη : 0 < η) (v : CKN.Foundation.Parabolic.Vec3) : 0 ≤ heatRegEnergy η v

The regularized entropy potential is nonnegative.

theorem ESS.heatRegG_sq_le_energy {η : ℝ} (hη : 0 < η) (v : CKN.Foundation.Parabolic.Vec3) : heatRegG η v ^ 2 ≤ 27 * heatRegEnergy η v

The square of the regularized |v|^(3/2) is controlled by its entropy.

theorem ESS.heatReg_inv_rpow_half {η : ℝ} (hη : 0 < η) (v : CKN.Foundation.Parabolic.Vec3) : heatRegSq η v ^ (-(1 / 2)) = (heatRegSq η v ^ (1 / 2))⁻¹

The negative half power is the reciprocal square root used in the entropy derivative estimates for lem:pv-heat-critical.

theorem ESS.heatReg_gradient_bound {η : ℝ} (hη : 0 < η) (v w : CKN.Foundation.Parabolic.Vec3) : (fderiv ℝ (heatRegG η) v) w ^ 2 ≤ 9 / 2 * (heatRegSq η v ^ (1 / 2) - η) * ∑ i : Fin 3, w i ^ 2

The gradient of the regularized |v|^(3/2) is controlled by entropy dissipation.

theorem ESS.heatRegEnergy_le_mul_sum_sq {η M : ℝ} (hη : 0 < η) (hM : 0 ≤ M) (v : CKN.Foundation.Parabolic.Vec3) (hv : CKN.Foundation.Parabolic.vec3EuclideanNorm v ≤ M) : heatRegEnergy η v ≤ (3 * η + 2 * M) / 6 * ∑ i : Fin 3, v i ^ 2

A quadratic bound on the regularized entropy for bounded vector fields.

theorem ESS.heatReg_root_sub_eta_le_norm {η : ℝ} (hη : 0 < η) (v : CKN.Foundation.Parabolic.Vec3) : heatRegSq η v ^ (1 / 2) - η ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm v

The regularized root increment is bounded by the Euclidean vector norm.

theorem ESS.heatRegTest_abs_le_norm_sq {η : ℝ} (hη : 0 < η) (v : CKN.Foundation.Parabolic.Vec3) (i : Fin 3) : |heatRegTest η v i| ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm v ^ 2

Each regularized entropy-test component is bounded by the squared vector norm.