Time cutoffs of whole-space heat solutions

The whole-space form of lem:local-heat-gain, used in prop:lps-smoothing, multiplies a solution of ∂ₜ z - Δ z = G on ℝ³ × I by a smooth cutoff c(t) depending on time only. Spatial derivatives commute with the cutoff, so a space-time derivative family D of z gives the family c D of c z, and c z solves ∂ₜ (c z) - Δ (c z) = c G + c' z on ℝ³ × I. The squared norms are controlled by the bounds for c and c'.

theorem ESS.spatialPartial_timeFun (c : ℝ → ℝ) (j : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.spatialPartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => c q.2) j p = 0

A function of time alone has vanishing spatial derivatives.

theorem ESS.IsSpaceTimeWeakPartial.time_mul {V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {j : Fin 3} {f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : IsSpaceTimeWeakPartial V j f g) {c : ℝ → ℝ} (hc : ContDiff ℝ (↑⊤) c) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict V)) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict V)) : IsSpaceTimeWeakPartial V j (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => c p.2 * f p) fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => c p.2 * g p

The distributional spatial derivative of c(t) f is c(t) ∂_j f.

theorem ESS.memLp_time_mul {V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict V)) {c : ℝ → ℝ} (hc : Continuous c) {L : ℝ} (hcL : ∀ (t : ℝ), |c t| ≤ L) : MeasureTheory.MemLp (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => c p.2 * f p) 2 (MeasureTheory.volume.restrict V)

A bounded continuous function of time keeps square integrability.

theorem ESS.IsSpaceTimeFamily.time_mul {n : ℕ} {V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {B : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hB : IsSpaceTimeFamily n V B) {c : ℝ → ℝ} (hc : ContDiff ℝ (↑⊤) c) {L : ℝ} (hcL : ∀ (t : ℝ), |c t| ≤ L) : IsSpaceTimeFamily n V fun (α : List (Fin 3)) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => c p.2 * B α p

Multiplication by a smooth bounded function of time maps a space-time derivative family to a space-time derivative family.

theorem CKN.IsHeatSolutionOn.time_mul {I : Set ℝ} {z G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hz : MeasureTheory.MemLp z 2 (MeasureTheory.volume.restrict (Set.univ ×ˢ I))) (hG : MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict (Set.univ ×ˢ I))) (hheat : IsHeatSolutionOn Set.univ I z G) {c : ℝ → ℝ} (hc : ContDiff ℝ (↑⊤) c) : IsHeatSolutionOn Set.univ I (fun (p : Foundation.Parabolic.Vec3 × ℝ) => c p.2 * z p) fun (p : Foundation.Parabolic.Vec3 × ℝ) => c p.2 * G p + deriv c p.2 * z p

lem:local-heat-gain on the whole space, first step: if ∂ₜ z - Δ z = G on ℝ³ × I and c is a smooth function of time, then ∂ₜ (c z) - Δ (c z) = c G + c' z on ℝ³ × I.

theorem ESS.integral_sq_time_mul_le {V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict V)) {c : ℝ → ℝ} (hc : Continuous c) (hc1 : ∀ (t : ℝ), |c t| ≤ 1) : ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in V, (c p.2 * f p) ^ 2 ≤ ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in V, f p ^ 2

The square integral of c(t) f with |c| ≤ 1 is at most that of f.

theorem ESS.integral_sq_time_mul_add_le {V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict V)) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict V)) {c d : ℝ → ℝ} (hc : Continuous c) (hd : Continuous d) (hc1 : ∀ (t : ℝ), |c t| ≤ 1) {L : ℝ} (hdL : ∀ (t : ℝ), |d t| ≤ L) : ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in V, (c p.2 * g p + d p.2 * f p) ^ 2 ≤ (2 * ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in V, g p ^ 2) + 2 * L ^ 2 * ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in V, f p ^ 2

The square integral of c(t) g + d(t) f with |c| ≤ 1 and |d| ≤ L is at most 2 ‖g‖² + 2 L² ‖f‖².