Zero initial trace for solutions vanishing near the initial time

A square-integrable distributional solution of ∂ₜ u - Δ u = div H + f on ℝ³ × (a, b) that vanishes for t < a + δ has, for every spatial test ψ, a spatial pairing t ↦ ∫ u(x, t) ψ(x) dx with a continuous version on [a, b] vanishing at a: the pairing has an integrable distributional time derivative. This is the zero initial trace used with the energy estimate of lem:localized-vorticity-energy in the proof of lem:local-heat-gain.

theorem ESS.separatedTest_timePartial {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} {θ : ℝ → ℝ} (hθ : Differentiable ℝ θ) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.timePartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ q.1 * θ q.2) p = ψ p.1 * deriv θ p.2

The time derivative of a separated test ψ(x) θ(t).

theorem ESS.separatedTest_spatialPartial {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} {θ : ℝ → ℝ} (hψ : Differentiable ℝ ψ) (j : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.spatialPartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ q.1 * θ q.2) j p = θ p.2 * CKN.spatialDeriv ψ j p.1

The spatial derivative of a separated test ψ(x) θ(t).

theorem ESS.separatedTest_spatialSecondPartial {ψ : CKN.Foundation.Parabolic.Vec3 → ℝ} {θ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (j : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.spatialSecondPartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ q.1 * θ q.2) j j p = θ p.2 * CKN.spatialDeriv (CKN.spatialDeriv ψ j) j p.1

The second spatial derivative of a separated test ψ(x) θ(t).

theorem ESS.memLp_slab_of_space {a b : ℝ} {g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : MeasureTheory.MemLp (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => g p.1) 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))

(x, t) ↦ g(x) is square integrable on a slab for square integrable g.

theorem ESS.memLp_slab_of_test {a b : ℝ} {g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hg : Continuous g) (hgc : HasCompactSupport g) : MeasureTheory.MemLp (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => g p.1) 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))

Continuous compactly supported spatial functions are square integrable on slabs.

theorem ESS.exists_continuous_version_zero_trace {a b δ : ℝ} (hab : a < b) (hδ : 0 < δ) {P Q : ℝ → ℝ} (hPint : MeasureTheory.Integrable P (MeasureTheory.volume.restrict (Set.Ioo a b))) (hQint : MeasureTheory.Integrable Q (MeasureTheory.volume.restrict (Set.Ioo a b))) (hweakP : CKN.HasWeakDerivOn (Set.Ioo a b) P Q) (hP0 : ∀ t < a + δ, P t = 0) : ∃ (c : ℝ → ℝ), ContinuousOn c (Set.Icc a b) ∧ c a = 0 ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), c t = P t

A function on (a, b) with an integrable distributional derivative that vanishes near a has a continuous version on [a, b] vanishing at a.

theorem ESS.heatSolution_trace_zero {a b δ : ℝ} (hab : a < b) (hδ : 0 < δ) {u f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {H : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hH : ∀ (j : Fin 3), MeasureTheory.MemLp (H j) 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hweak : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, u p * (-CKN.timePartial φ p - ∑ j : Fin 3, CKN.spatialSecondPartial φ j j p) = ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, -∑ j : Fin 3, H j p * CKN.spatialPartial φ j p + f p * φ p) (hzero : ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), p.2 < a + δ → u p = 0) (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∃ (c : ℝ → ℝ), ContinuousOn c (Set.Icc a b) ∧ c a = ∫ (x : CKN.Foundation.Parabolic.Vec3), (fun (x : CKN.Foundation.Parabolic.Vec3) => 0) x * ψ x ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), c t = ∫ (x : CKN.Foundation.Parabolic.Vec3), u (x, t) * ψ x

A distributional solution on a slab vanishing near the initial time has a zero initial trace.