Zero extension across the shifted time face

A field already supported in a smaller cylinder agrees pointwise with its zero extension from that cylinder.

theorem ESS.bu_setIntegral_eq_integral_of_zero_off (V : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)) (F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (hzero : ∀ q ∉ V, F q = 0) : ∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ) in V, F q = ∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), F q

A product-coordinate integrand that vanishes off a measurable set has the same unrestricted and restricted integral.

theorem ESS.bu_zeroExtend_eq_of_support_subset {E : Type} [Zero E] {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {K : Set CKN.Foundation.Parabolic.ParabolicPoint} (hKsub : K ⊆ CKN.spaceTimeSet Ω I) {f : CKN.Foundation.Parabolic.ParabolicPoint → E} (hfzero : ∀ z ∉ K, f z = 0) (q : CKN.Foundation.Parabolic.Vec3 × ℝ) : CKN.zeroExtendField (Ω ×ˢ I) (fun (r : CKN.Foundation.Parabolic.Vec3 × ℝ) => f (CKN.Foundation.Parabolic.parabolicHomeomorph.symm r)) q = f (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q)

If a field vanishes off a subset of a cylinder, zero extension from that cylinder leaves its product-coordinate representation unchanged.