Smooth-data calculus for the forced heat response

For a smooth compactly supported tensor source supported in positive times, the forced heat response and its first and second spatial derivatives and its time derivative decay like |x|^{-3} uniformly in time; the response solves the heat equation with divergence source and vanishes at time zero. These are the facts used by the energy estimates of lem:pv-stokes.

theorem ESS.abs_le_decay_of_hasCompactSupport {f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : Continuous f) (hfc : HasCompactSupport f) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), |f q| ≤ M / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm q.1) ^ 3

A continuous compactly supported space-time function is bounded by a multiple of (1 + |x|)^{-3}.

theorem ESS.exists_common_decay_constant {ι : Type u_1} [Finite ι] (f : ι → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (hf : ∀ (a : ι), ∃ (M : ℝ), 0 ≤ M ∧ ∀ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), |f a q| ≤ M / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm q.1) ^ 3) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (a : ι) (q : CKN.Foundation.Parabolic.Vec3 × ℝ), |f a q| ≤ M / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm q.1) ^ 3

A finite family of functions with (1 + |x|)^{-3} decay has a common decay constant.

noncomputable def ESS.vecTimeDiv (g : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (i : Fin 3) (q : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

The divergence ∑_j ∂_j g_ij of a space-time tensor on Vec3 × ℝ, with spatial derivatives written as directional derivatives.

Equations

• ESS.vecTimeDiv g i q = ∑ j : Fin 3, (fderiv ℝ (g i j) q) (CKN.basisVec j, 0)

theorem ESS.forcedHeat_eq_causalHeatConv_vecTimeDiv {G : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hG : ∀ (i j : Fin 3), ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) (hGc : ∀ (i j : Fin 3), HasCompactSupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) (i : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : forcedHeat G z i = causalHeatConv (vecTimeDiv (fun (i j : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => G i j p) i) z

For a smooth compactly supported tensor, the forced heat response is the causal heat potential of vecTimeDiv.

theorem ESS.vecTimeDiv_contDiff {g : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ∀ (i j : Fin 3), ContDiff ℝ (↑⊤) (g i j)) (i : Fin 3) : ContDiff ℝ (↑⊤) (vecTimeDiv g i)

The divergence of a smooth tensor is smooth.

theorem ESS.vecTimeDiv_hasCompactSupport {g : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hgc : ∀ (i j : Fin 3), HasCompactSupport (g i j)) (i : Fin 3) : HasCompactSupport (vecTimeDiv g i)

The divergence of a compactly supported smooth tensor has compact support.

theorem ESS.vecTimeDiv_response_decay {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)) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (i j k : Fin 3) (q : CKN.Foundation.Parabolic.Vec3 × ℝ), |causalHeatConv (vecTimeDiv g i) q| ≤ M / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm q.1) ^ 3 ∧ |(fderiv ℝ (causalHeatConv (vecTimeDiv g i)) q) (CKN.basisVec j, 0)| ≤ M / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm q.1) ^ 3 ∧ |(fderiv ℝ (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => (fderiv ℝ (causalHeatConv (vecTimeDiv g i)) p) (CKN.basisVec j, 0)) q) (CKN.basisVec k, 0)| ≤ M / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm q.1) ^ 3 ∧ |(fderiv ℝ (causalHeatConv (vecTimeDiv g i)) q) (0, 1)| ≤ M / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm q.1) ^ 3 ∧ |g i j q| ≤ M / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm q.1) ^ 3 ∧ |(fderiv ℝ (g i j) q) (CKN.basisVec k, 0)| ≤ M / (1 + CKN.Foundation.Parabolic.vec3EuclideanNorm q.1) ^ 3

The response causalHeatConv (vecTimeDiv g i), its first and second spatial derivatives, its time derivative, and the tensor with its spatial derivatives all decay like (1 + |x|)^{-3} with a common constant.