The slicewise weak gradient of the rough forced heat response

Along a smooth approximation whose responses converge in the weighted L¹ sense and whose spatial gradients converge in L²(Q_τ), a fast subsequence converges on almost every time slice; passing the classical slice identities to the limit shows that for almost every time the limit gradient is the weak spatial gradient of the slice of the rough response, as required by the finite-energy class of prop:pv-local-solution.

theorem ESS.ae_slice_aestronglyMeasurable {X : Type u_1} [TopologicalSpace X] {ν : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite ν] {f : CKN.Foundation.Parabolic.Vec3 × ℝ → X} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.prod ν)) : ∀ᵐ (s : ℝ) ∂ν, MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, s)) MeasureTheory.volume

Almost every time slice of a measurable space-time function is measurable.

theorem ESS.ae_slice_of_ae {ν : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite ν] {P : CKN.Foundation.Parabolic.Vec3 × ℝ → Prop} (h : ∀ᵐ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.prod ν, P z) : ∀ᵐ (s : ℝ) ∂ν, ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), P (x, s)

A property holding almost everywhere on Vec3 × ℝ holds on almost every time slice.

theorem ESS.abs_le_mul_forcedHeatWeight_space {χ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hχ : Continuous χ) (hχc : HasCompactSupport χ) : ∃ (c : ℝ), 0 ≤ c ∧ ∀ (x : CKN.Foundation.Parabolic.Vec3), |χ x| ≤ c * forcedHeatWeight x

A continuous compactly supported function on Vec3 is dominated by a multiple of the weight forcedHeatWeight.

theorem ESS.exists_subseq_slice_tendsto {ν : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite ν] {f : ℕ → CKN.Foundation.Parabolic.Vec3 × ℝ → ENNReal} (hf : ∀ (k : ℕ), AEMeasurable (f k) (MeasureTheory.volume.prod ν)) (hlim : Filter.Tendsto (fun (k : ℕ) => ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), f k z ∂MeasureTheory.volume.prod ν) Filter.atTop (nhds 0)) : ∃ (m : ℕ → ℕ), ∀ᵐ (s : ℝ) ∂ν, Filter.Tendsto (fun (n : ℕ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), f (m n) (x, s)) Filter.atTop (nhds 0)

A sequence of nonnegative space-time functions whose integrals tend to zero has a subsequence whose slice integrals tend to zero for almost every time.

theorem ESS.forcedHeat_slice_grad_memLp {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) (s : ℝ) (i j : Fin 3) : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => forcedHeat G w i) j (x, s)) 2 MeasureTheory.volume

The slices of smooth forced heat responses are square integrable in space together with their spatial gradients.