Integrals of fields supported in a smaller cylinder

The product-coordinate integral of a field supported inside a target cylinder equals its set integral on that cylinder.

theorem ESS.bu_target_setIntegral_eq_product_integral {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {K : Set CKN.Foundation.Parabolic.ParabolicPoint} (hKsub : K ⊆ CKN.spaceTimeSet Ω I) (F : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hzero : ∀ z ∉ K, F z = 0) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω I, F z = ∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), F (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q)

For a scalar integrand supported in a subset of a target cylinder, the target set integral is the unrestricted product-coordinate integral.