Energy identities for the smooth forced heat response

For a smooth compactly supported tensor supported in positive times, a convex entropy Φ with gradient T satisfies the whole-space identity

∫ Φ(Z(t₁)) = -∫₀^{t₁} ∑_{i,j} ∫ ∂_j[T_i(Z)] (∂_j Z_i + g_ij),

obtained from the fundamental theorem of calculus in time, Fubini, and an integration by parts in space. It is the common core of the energy and critical estimates of lem:pv-stokes.

noncomputable def ESS.responseVec (g : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.Foundation.Parabolic.Vec3

The response vector Z(p) to the tensor g at a space-time point.

Equations

• ESS.responseVec g p k = ESS.causalHeatConv (ESS.vecTimeDiv g k) p

noncomputable def ESS.responseGrad (g : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (j : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.Foundation.Parabolic.Vec3

The spatial derivative ∂_j Z(p) of the response vector.

Equations

• ESS.responseGrad g j p k = (fderiv ℝ (ESS.causalHeatConv (ESS.vecTimeDiv g k)) p) (CKN.basisVec j, 0)

theorem ESS.exists_linear_bound_of_contDiff {T : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hT : ContDiff ℝ 1 T) (hT0 : T 0 = 0) (R : ℝ) : ∃ (L : ℝ), 0 ≤ L ∧ ∀ (v : CKN.Foundation.Parabolic.Vec3), ‖v‖ ≤ R → ‖T v‖ ≤ L * ‖v‖ ∧ ‖fderiv ℝ T v‖ ≤ L

A continuously differentiable map vanishing at the origin grows at most linearly, with bounded derivative, on each ball.

theorem ESS.integrable_mul_of_decay {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hfb : ∀ (x : CKN.Foundation.Parabolic.Vec3), |f x| ≤ A / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm x) ^ 3) (hgb : ∀ (x : CKN.Foundation.Parabolic.Vec3), |g x| ≤ B / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm x) ^ 3) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => f x * g x) MeasureTheory.volume

A product of two functions with (1 + |x|)^{-3} decay is integrable on Vec3.

theorem ESS.integrable_window_of_decay {F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : Continuous F) {a b C : ℝ} (hC : 0 ≤ C) (hb : ∀ (x : CKN.Foundation.Parabolic.Vec3), ∀ t ∈ Set.Ioc a b, |F (x, t)| ≤ C / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm x) ^ 6) : MeasureTheory.Integrable F (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc a b)))

A space-time function bounded by C (1 + |x|)^{-6} on a finite time window is integrable on the window.

theorem ESS.entropy_eq_time_integral {Φ : CKN.Foundation.Parabolic.Vec3 → ℝ} {T : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hΦ : ContDiff ℝ 1 Φ) (hT : Continuous T) (hΦT : ∀ (v w : CKN.Foundation.Parabolic.Vec3), (fderiv ℝ Φ v) w = ∑ i : Fin 3, T v i * w i) (hΦ0 : Φ 0 = 0) {U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hU : ∀ (i : Fin 3), ContDiff ℝ 1 (U i)) (hU0 : ∀ (i : Fin 3) (x : CKN.Foundation.Parabolic.Vec3), U i (x, 0) = 0) (x : CKN.Foundation.Parabolic.Vec3) (t₁ : ℝ) : (Φ fun (i : Fin 3) => U i (x, t₁)) = ∫ (t : ℝ) in 0..t₁, ∑ i : Fin 3, T (fun (k : Fin 3) => U k (x, t)) i * (fderiv ℝ (U i) (x, t)) (0, 1)

The fundamental theorem of calculus along each spatial point for an entropy of a smooth vector field vanishing at time zero.

theorem ESS.entropy_integral_eq_window_integral {Φ : CKN.Foundation.Parabolic.Vec3 → ℝ} {T : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hΦ : ContDiff ℝ 1 Φ) (hT : Continuous T) (hΦT : ∀ (v w : CKN.Foundation.Parabolic.Vec3), (fderiv ℝ Φ v) w = ∑ i : Fin 3, T v i * w i) (hΦ0 : Φ 0 = 0) {U : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hU : ∀ (i : Fin 3), ContDiff ℝ 1 (U i)) (hU0 : ∀ (i : Fin 3) (x : CKN.Foundation.Parabolic.Vec3), U i (x, 0) = 0) {t₁ C : ℝ} (ht₁ : 0 ≤ t₁) (hC : 0 ≤ C) (hb : ∀ (x : CKN.Foundation.Parabolic.Vec3), ∀ t ∈ Set.Ioc 0 t₁, |∑ i : Fin 3, T (fun (k : Fin 3) => U k (x, t)) i * (fderiv ℝ (U i) (x, t)) (0, 1)| ≤ C / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm x) ^ 6) : (∫ (x : CKN.Foundation.Parabolic.Vec3), Φ fun (i : Fin 3) => U i (x, t₁)) = ∫ (t : ℝ) in 0..t₁, ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, T (fun (k : Fin 3) => U k (x, t)) i * (fderiv ℝ (U i) (x, t)) (0, 1)

Fubini form of entropy_eq_time_integral: the spatial integral of the entropy at time t₁ is the time integral of the spatial production.