Auxiliary facts for the cutoff argument of lem:local-heat-gain

Leibniz families vanish where the multiplier and its spatial derivatives vanish, reduce to the second family where the multiplier is one near the point, and are strongly measurable. Space-time derivative families restrict to smaller orders, shifted words and smaller sets, and the distributional heat equation is insensitive to almost everywhere modification.

theorem ESS.stLeibniz_eq_zero_of_forall (α : List (Fin 3)) {A B : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {p : CKN.Foundation.Parabolic.Vec3 × ℝ} (hA : ∀ (γ : List (Fin 3)), A γ p = 0) : stLeibniz α A B p = 0

theorem ESS.stLeibniz_eq_of_unit (α : List (Fin 3)) {A B : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {p : CKN.Foundation.Parabolic.Vec3 × ℝ} (h1 : A [] p = 1) (h0 : ∀ (γ : List (Fin 3)), γ ≠ [] → A γ p = 0) : stLeibniz α A B p = B α p

theorem ESS.stLeibniz_stronglyMeasurable (α : List (Fin 3)) {A B : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hA : ∀ (γ : List (Fin 3)), MeasureTheory.StronglyMeasurable (A γ)) (hB : ∀ (γ : List (Fin 3)), MeasureTheory.StronglyMeasurable (B γ)) : MeasureTheory.StronglyMeasurable (stLeibniz α A B)

theorem ESS.IsSpaceTimeFamily.mono_order {n n' : ℕ} {V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {B : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : IsSpaceTimeFamily n V B) (hn : n' ≤ n) : IsSpaceTimeFamily n' V B

theorem ESS.IsSpaceTimeFamily.shift {n : ℕ} {V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {B : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : IsSpaceTimeFamily n V B) (hn : 1 ≤ n) (j : Fin 3) : IsSpaceTimeFamily (n - 1) V fun (γ : List (Fin 3)) => B (j :: γ)

theorem ESS.IsSpaceTimeWeakPartial.mono {V W : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)} {j : Fin 3} {f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : IsSpaceTimeWeakPartial V j f g) (hV : MeasurableSet V) (hWV : W ⊆ V) : IsSpaceTimeWeakPartial W j f g

Distributional spatial derivatives restrict to smaller measurable sets.

theorem CKN.IsHeatSolutionOn.congr_ae {U : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {z z' G G' : Foundation.Parabolic.Vec3 × ℝ → ℝ} (h : IsHeatSolutionOn U I z G) (hz : z =ᵐ[MeasureTheory.volume.restrict (U ×ˢ I)] z') (hG : G =ᵐ[MeasureTheory.volume.restrict (U ×ˢ I)] G') : IsHeatSolutionOn U I z' G'

The distributional heat equation is insensitive to almost everywhere modification.

theorem ESS.timePartial_separated {c : ℝ → ℝ} (hc : Differentiable ℝ c) (g : CKN.Foundation.Parabolic.Vec3 → ℝ) (x₀ : CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.timePartial (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => c q.2 * g (q.1 - x₀)) p = deriv c p.2 * g (p.1 - x₀)

The time derivative of a separated field.