Heat Critical Estimate

The regularized entropy density of a smooth heat orbit is integrable at each positive time, as used in lem:pv-heat-critical.

theorem ESS.heatRegEnergy_heatConv_integrable {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 < η) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => heatRegEnergy η (heatConvVec3 t b x)) MeasureTheory.volume

The regularized entropy density of a smooth heat orbit is integrable at each positive time, as used in lem:pv-heat-critical.

theorem ESS.heatRegG_heatConv_spatial_grad_sq_le_dissipation {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 < η) (x : CKN.Foundation.Parabolic.Vec3) (j : Fin 3) : CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatRegG η (heatConvVec3 t b y)) j x ^ 2 ≤ 9 / 2 * ∑ i : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatRegTest η (heatConvVec3 t b y) i) j x * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatConvVec3 t b y i) j x

The regularized critical profile's directional gradient is controlled by the entropy-test dissipation, pointwise in space and time.

theorem ESS.heatRegEnergy_integral_deriv_eq_neg_dissipation {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 < η) : deriv (fun (s : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), heatRegEnergy η (heatConvVec3 s b x)) t = -∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatRegTest η (heatConvVec3 t b y) i) j x * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatConvVec3 t b y i) j x

The entropy-integral derivative equals minus the integrated spatial test dissipation for smooth compact data.

theorem ESS.heatRegG_heatConv_spatial_grad_sq_integrable {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 < η) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatRegG η (heatConvVec3 t b y)) j x ^ 2) MeasureTheory.volume

The spatial gradient of the regularized critical profile is square integrable for each positive time.

theorem ESS.heatRegG_heatConv_spatial_grad_sq_integral_le_dissipation {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 < η) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ j : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatRegG η (heatConvVec3 t b y)) j x ^ 2 ≤ 9 / 2 * ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatRegTest η (heatConvVec3 t b y) i) j x * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatConvVec3 t b y i) j x

Spatial integration of the gradient inequality compares its square integral with the integrated entropy-test dissipation.

theorem ESS.heatRegEnergy_time_dissipation_le_initial {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) {τ η : ℝ} (hτ : 0 < τ) (hη : 0 < η) : IntervalIntegrable (fun (t : ℝ) => ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatRegTest η (heatConvVec3 t b y) i) j x * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatConvVec3 t b y i) j x) MeasureTheory.volume 0 τ ∧ ∫ (t : ℝ) in 0..τ, ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatRegTest η (heatConvVec3 t b y) i) j x * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => heatConvVec3 t b y i) j x ≤ ∫ (x : CKN.Foundation.Parabolic.Vec3), heatRegEnergy η (b x)

Time integration of entropy dissipation is bounded by the initial regularized entropy, uniformly in the terminal time.