The energy estimate for the smooth forced heat response

Testing the forced heat equation with the response itself gives, for every t₁ ≥ 0, ‖Z(t₁)‖₂² + ∫₀^{t₁} ‖∇Z‖₂² ≤ ∫₀^{t₁} ‖g‖₂², the smooth-data form of eq:pv-stokes-energy in lem:pv-stokes.

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

The quadratic entropy ½ |v|².

Equations

• ESS.halfSq v = 1 / 2 * ∑ i : Fin 3, v i * v i

theorem ESS.response_sq_window_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)) (a b : ℝ) : MeasureTheory.Integrable (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ i : Fin 3, ∑ j : Fin 3, responseGrad g j p i ^ 2) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc a b))) ∧ MeasureTheory.Integrable (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ i : Fin 3, ∑ j : Fin 3, g i j p ^ 2) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc a b))) ∧ MeasureTheory.Integrable (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∑ i : Fin 3, ∑ j : Fin 3, responseGrad g j p i * (responseGrad g j p i + g i j p)) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc a b)))

The response and its spatial gradient have space-time integrable squares on each finite window, and the squared tensor is integrable there.

theorem ESS.response_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}) {t₁ : ℝ} (ht₁ : 0 ≤ t₁) : (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, responseVec g (x, t₁) i ^ 2) + ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), ∑ i : Fin 3, ∑ j : Fin 3, responseGrad g j p i ^ 2 ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 t₁)) ≤ ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), ∑ i : Fin 3, ∑ j : Fin 3, g i j p ^ 2 ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc 0 t₁))

The energy estimate for the smooth forced heat response: for every t₁ ≥ 0, ‖Z(t₁)‖₂² + ∫_{(0,t₁]} ‖∇Z‖₂² ≤ ∫_{(0,t₁]} ‖g‖₂².