The whole-space entropy identity for the smooth forced heat response

At each time, integrating by parts in space turns the entropy production ∑_i T_i(Z) ∂_t Z_i of the forced heat response into -∑_{i,j} ∂_j[T_i(Z)] (∂_j Z_i + g_ij). Combined with the time integration of entropy_integral_eq_window_integral, this is the identity behind the energy and critical estimates of lem:pv-stokes.

theorem ESS.fderiv_slice_apply {F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : Differentiable ℝ F) (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) (v : CKN.Foundation.Parabolic.Vec3) : (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => F (y, t)) x) v = (fderiv ℝ F (x, t)) (v, 0)

The spatial derivative of a time slice of a differentiable space-time function is the joint derivative in the corresponding spatial direction.

theorem ESS.fderiv_comp_slice_apply {T : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hT : Differentiable ℝ T) {U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hU : ∀ (k : Fin 3), Differentiable ℝ (U k)) (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) (v : CKN.Foundation.Parabolic.Vec3) (i : Fin 3) : (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => T (fun (k : Fin 3) => U k (y, t)) i) x) v = (fderiv ℝ T fun (k : Fin 3) => U k (x, t)) (fun (k : Fin 3) => (fderiv ℝ (U k) (x, t)) (v, 0)) i

Chain rule for a map applied to a time slice of a smooth vector field.

theorem ESS.integral_mul_fderiv_of_decay {f k : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : ContDiff ℝ 1 f) (hk : ContDiff ℝ 1 k) {A : ℝ} (hA : 0 ≤ A) (v : CKN.Foundation.Parabolic.Vec3) (hfb : ∀ (x : CKN.Foundation.Parabolic.Vec3), |f x| ≤ A / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm x) ^ 3) (hDfb : ∀ (x : CKN.Foundation.Parabolic.Vec3), |(fderiv ℝ f x) v| ≤ A / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm x) ^ 3) (hkb : ∀ (x : CKN.Foundation.Parabolic.Vec3), |k x| ≤ A / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm x) ^ 3) (hDkb : ∀ (x : CKN.Foundation.Parabolic.Vec3), |(fderiv ℝ k x) v| ≤ A / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm x) ^ 3) : ∫ (x : CKN.Foundation.Parabolic.Vec3), f x * (fderiv ℝ k x) v = -∫ (x : CKN.Foundation.Parabolic.Vec3), (fderiv ℝ f x) v * k x

Integration by parts on Vec3 for continuously differentiable functions with (1 + |x|)^{-3} decay together with their derivatives.

theorem ESS.response_production_identity {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) (t : ℝ) : ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, T (responseVec g (x, t)) i * (fderiv ℝ (causalHeatConv (vecTimeDiv g i)) (x, t)) (0, 1) = -∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, (fderiv ℝ T (responseVec g (x, t))) (responseGrad g j (x, t)) i * (responseGrad g j (x, t) i + g i j (x, t))

At each time, the entropy production of the forced heat response integrates by parts to -∑_{i,j} ∫ ∂_j[T_i(Z)] (∂_j Z_i + g_ij).

theorem ESS.vecTimeDiv_eq_zero_of_nonpos {g : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hgpos : ∀ (i j : Fin 3), tsupport (g i j) ⊆ {p : CKN.Foundation.Parabolic.Vec3 × ℝ | 0 < p.2}) (i : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) (hp : vecTimeDiv g i p ≠ 0) : 0 < p.2

The divergence of a tensor supported in positive times vanishes at nonpositive times.

theorem ESS.response_entropy_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) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), |∑ i : Fin 3, T (responseVec g p) i * (fderiv ℝ (causalHeatConv (vecTimeDiv g i)) p) (0, 1)| ≤ C / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm p.1) ^ 6 ∧ |∑ i : Fin 3, ∑ j : Fin 3, (fderiv ℝ T (responseVec g p)) (responseGrad g j p) i * (responseGrad g j p i + g i j p)| ≤ C / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm p.1) ^ 6

Pointwise (1 + |x|)^{-6} bounds for the entropy production and the dissipation integrand of the forced heat response.

theorem ESS.response_entropy_identity {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}) {Φ : CKN.Foundation.Parabolic.Vec3 → ℝ} {T : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hΦ : ContDiff ℝ 1 Φ) (hT : ContDiff ℝ 1 T) (hΦT : ∀ (v w : CKN.Foundation.Parabolic.Vec3), (fderiv ℝ Φ v) w = ∑ i : Fin 3, T v i * w i) (hΦ0 : Φ 0 = 0) (hT0 : T 0 = 0) {t₁ : ℝ} (ht₁ : 0 ≤ t₁) : ∫ (x : CKN.Foundation.Parabolic.Vec3), Φ (responseVec g (x, t₁)) = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), ∑ i : Fin 3, ∑ j : Fin 3, (fderiv ℝ T (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 0 t₁))

The whole-space entropy identity for the forced heat response: for a convex entropy Φ with gradient T and every t₁ ≥ 0, ∫ Φ(Z(t₁)) = -∫_{Vec3 × (0,t₁]} ∑_{i,j} ∂_j[T_i(Z)] (∂_j Z_i + g_ij).