The heat equation for a cutoff of a local solution

If ∂ₜ z - Δ z = G in distributions on U × I and η is smooth and vanishes for x outside a compact subset of U, then w = ηz, extended by zero, solves ∂ₜ w - Δ w = ηG + (∂ₜη - Δη) z - 2 ∇η · ∇z in distributions on ℝ³ × I (lem:local-heat-gain, first step of the proof).

theorem ESS.spatialSecondPartial_mul_of_contDiff {A B : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hB : ContDiff ℝ (↑⊤) B) (j : Fin 3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.spatialSecondPartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => A q * B q) j j p = A p * CKN.spatialSecondPartial B j j p + 2 * (CKN.spatialPartial A j p * CKN.spatialPartial B j p) + B p * CKN.spatialSecondPartial A j j p

The second spatial derivative of a product of smooth fields.

theorem ESS.tsupport_mul_subset_of_compl {U K : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hK : IsCompact K) (hKU : K ⊆ U) {f φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), p.1 ∉ K → f p = 0) (hφ : tsupport φ ⊆ Set.univ ×ˢ I) : (tsupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => f p * φ p) ⊆ U ×ˢ I

A product with a field vanishing outside K × ℝ has topological support in U × I when the other factor is supported in ℝ³ × I and K ⊆ U.

theorem ESS.setIntegral_univ_prod_eq {U : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hI : MeasurableSet I) {F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), p.1 ∉ U → F p = 0) : ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ I, F p = ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in U ×ˢ I, F p

Set integrals over ℝ³ × I of integrands vanishing for x ∉ U are integrals over U × I.

theorem ESS.heatCutoff_equation {U K : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hIm : MeasurableSet I) (hK : IsCompact K) (hKU : K ⊆ U) {z G η : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {Dz : Fin 3 → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηK : ∀ x ∉ K, ∀ (t : ℝ), η (x, t) = 0) (hz : MeasureTheory.MemLp z 2 (MeasureTheory.volume.restrict (U ×ˢ I))) (hDz : ∀ (j : Fin 3), MeasureTheory.MemLp (Dz j) 2 (MeasureTheory.volume.restrict (U ×ˢ I))) (hG : MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict (U ×ˢ I))) (hweak : ∀ (j : Fin 3), IsSpaceTimeWeakPartial (U ×ˢ I) j z (Dz j)) (hheat : CKN.IsHeatSolutionOn U I z G) (φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ Set.univ ×ˢ I → ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ I, η p * z p * (-CKN.timePartial φ p - ∑ j : Fin 3, CKN.spatialSecondPartial φ j j p) = ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ I, (η p * G p + (CKN.timePartial η p - ∑ j : Fin 3, CKN.spatialSecondPartial η j j p) * z p - 2 * ∑ j : Fin 3, CKN.spatialPartial η j p * Dz j p) * φ p

The heat equation for a cutoff of a local distributional solution.

theorem ESS.IsSpaceTimeFamily.add {n : ℕ} {V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {B₁ B₂ : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h₁ : IsSpaceTimeFamily n V B₁) (h₂ : IsSpaceTimeFamily n V B₂) : IsSpaceTimeFamily n V fun (α : List (Fin 3)) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => B₁ α p + B₂ α p

Sums of space-time derivative families.

theorem ESS.IsSpaceTimeFamily.const_mul {n : ℕ} {V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {B : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : IsSpaceTimeFamily n V B) (c : ℝ) : IsSpaceTimeFamily n V fun (α : List (Fin 3)) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => c * B α p

Constant multiples of space-time derivative families.

theorem ESS.IsSpaceTimeFamily.congr_ae {n : ℕ} {V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {B B' : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : IsSpaceTimeFamily n V B) (hBB' : ∀ (α : List (Fin 3)), α.length ≤ n → B α =ᵐ[MeasureTheory.volume.restrict V] B' α) : IsSpaceTimeFamily n V B'

Almost everywhere modifications of space-time derivative families.

theorem ESS.IsSpaceTimeFamily.extend_univ {n : ℕ} {U K N : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} (hIm : MeasurableSet I) (hUm : MeasurableSet U) (hKU : K ⊆ U) (hN : IsOpen N) (hKN : K ⊆ N) {κ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hκ : ContDiff ℝ (↑⊤) κ) (hκc : HasCompactSupport κ) (hκU : tsupport κ ⊆ U) (hκN : ∀ x ∈ N, κ x = 1) {F : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : IsSpaceTimeFamily n (U ×ˢ I) F) (hFK : ∀ (α : List (Fin 3)), α.length ≤ n → ∀ (p : CKN.Foundation.Parabolic.Vec3 × ℝ), p.1 ∉ K → F α p = 0) : IsSpaceTimeFamily n (Set.univ ×ˢ I) F

A space-time derivative family on U × I whose members vanish for x outside a compact K ⊆ U is a family on ℝ³ × I. The cutoff κ equals one near K.