The regularized |Z| Z test for the forced heat response

Testing the forced heat equation with the regularized critical test heatRegTest η Z absorbs half of the forcing into the dissipation and leaves |Z| |g|²:

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

where D_j = ∑_i ∂_j[T_i(Z)] ∂_j Z_i is the entropy dissipation. This is the critical energy inequality in the proof of lem:pv-stokes.

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

The components of the derivative of the regularized critical test.

theorem ESS.heatRegTest_forcing_absorb {η : ℝ} (hη : 0 < η) (v a G : CKN.Foundation.Parabolic.Vec3) : -∑ i : Fin 3, (fderiv ℝ (heatRegTest η) v) a i * (a i + G i) ≤ -(1 / 2) * ∑ i : Fin 3, (fderiv ℝ (heatRegTest η) v) a i * a i + CKN.Foundation.Parabolic.vec3EuclideanNorm v * ∑ i : Fin 3, G i ^ 2

The pointwise absorption of the forcing: for the regularized critical test, -(∑_i (T'(v) a)_i (a_i + G_i)) ≤ -½ ∑_i (T'(v) a)_i a_i + |v| |G|².

theorem ESS.response_atom_bounds {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)) {T : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hT : ContDiff ℝ 1 T) (hT0 : T 0 = 0) : ∃ (A : ℝ), 0 ≤ A ∧ ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) (i j : Fin 3), |responseVec g p i| ≤ A / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm p.1) ^ 3 ∧ |responseGrad g j p i| ≤ A / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm p.1) ^ 3 ∧ |g i j p| ≤ A / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm p.1) ^ 3 ∧ |T (responseVec g p) i| ≤ A / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm p.1) ^ 3 ∧ |(fderiv ℝ T (responseVec g p)) (responseGrad g j p) i| ≤ A / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm p.1) ^ 3

Pointwise (1 + |x|)^{-3} bounds for the response, its spatial gradient, the tensor, and a C¹ test vanishing at the origin together with its derivative along the gradient.

theorem ESS.response_continuity {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)) {T : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hT : ContDiff ℝ 1 T) : Continuous (responseVec g) ∧ (∀ (j : Fin 3), Continuous (responseGrad g j)) ∧ ∀ (j : Fin 3), Continuous fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ T (responseVec g p)) (responseGrad g j p)

Continuity of the response, its gradient, and the derivative of a C¹ test along the gradient.