The critical energy inequality for the smooth forced heat response

For the regularized entropy heatRegEnergy η with gradient heatRegTest η, the whole-space identity and the pointwise absorption of the forcing give

∫ E_η(Z(t₁)) + ½ ∫₀^{t₁} ∑_j D_j ≤ ∫₀^{t₁} ∫ |Z| |g|²,

the regularized form of the critical inequality in lem:pv-stokes.

theorem ESS.abs_mul_le_decay_six {x y A B : ℝ} {z : CKN.Foundation.Parabolic.Vec3} (hA : 0 ≤ A) (hx : |x| ≤ A / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm z) ^ 3) (hy : |y| ≤ B / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm z) ^ 3) : |x * y| ≤ A * B / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm z) ^ 6

A product of two quantities with (1 + |x|)^{-3} bounds has a (1 + |x|)^{-6} bound.

theorem ESS.abs_double_sum_le_decay_six {F : Fin 3 → Fin 3 → ℝ} {C : ℝ} {z : CKN.Foundation.Parabolic.Vec3} (hF : ∀ (i j : Fin 3), |F i j| ≤ C / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm z) ^ 6) : |∑ i : Fin 3, ∑ j : Fin 3, F i j| ≤ 9 * C / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm z) ^ 6

A double sum over Fin 3 of quantities with a common (1 + |x|)^{-6} bound.

theorem ESS.heatRegEnergy_fderiv_eq_sum {η : ℝ} (hη : 0 < η) (v w : CKN.Foundation.Parabolic.Vec3) : (fderiv ℝ (heatRegEnergy η) v) w = ∑ i : Fin 3, heatRegTest η v i * w i

The regularized entropy has the regularized critical test as its gradient.

theorem ESS.heatRegEnergy_zero {η : ℝ} (hη : 0 < η) : heatRegEnergy η 0 = 0

The regularized entropy vanishes at the origin.

theorem ESS.heatRegTest_zero (η : ℝ) : heatRegTest η 0 = 0

The regularized critical test vanishes at the origin.

theorem ESS.response_critical_integrable {g : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ∀ (i j : Fin 3), ContDiff ℝ (↑⊤) (g i j)) (hgc : ∀ (i j : Fin 3), HasCompactSupport (g i j)) {η : ℝ} (hη : 0 < η) (a b : ℝ) : MeasureTheory.Integrable (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ i : Fin 3, ∑ j : Fin 3, (fderiv ℝ (heatRegTest η) (responseVec g p)) (responseGrad g j p) i * (responseGrad g j p i + g i j p)) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc a b))) ∧ MeasureTheory.Integrable (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ j : Fin 3, ∑ i : Fin 3, (fderiv ℝ (heatRegTest η) (responseVec g p)) (responseGrad g j p) i * responseGrad g j p i) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc a b))) ∧ MeasureTheory.Integrable (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Foundation.Parabolic.vec3EuclideanNorm (responseVec g p) * ∑ i : Fin 3, ∑ j : Fin 3, g i j p ^ 2) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc a b)))

The three integrands of the regularized critical inequality are integrable on every finite time window.

theorem ESS.response_critical_energy_le {g : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ∀ (i j : Fin 3), ContDiff ℝ (↑⊤) (g i j)) (hgc : ∀ (i j : Fin 3), HasCompactSupport (g i j)) (hgpos : ∀ (i j : Fin 3), tsupport (g i j) ⊆ {p : CKN.Foundation.Parabolic.Vec3 × ℝ | 0 < p.2}) {η : ℝ} (hη : 0 < η) {t₁ : ℝ} (ht₁ : 0 ≤ t₁) : (∫ (x : CKN.Foundation.Parabolic.Vec3), heatRegEnergy η (responseVec g (x, t₁))) + 1 / 2 * ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), ∑ j : Fin 3, ∑ i : Fin 3, (fderiv ℝ (heatRegTest η) (responseVec g p)) (responseGrad g j p) i * responseGrad g j p i ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 t₁)) ≤ ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.Foundation.Parabolic.vec3EuclideanNorm (responseVec g p) * ∑ i : Fin 3, ∑ j : Fin 3, g i j p ^ 2 ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 t₁))

The critical energy inequality for the forced heat response, regularized at level η > 0.