The parabolic-point measure and product coordinates #
parabolicHomeomorph identifies CKN's ParabolicPoint with Vec3 × ℝ; it
preserves the Lebesgue measures in both directions.
The CKN parabolic measure transported through the product-coordinate homeomorphism.
Product Lebesgue measure transported to CKN's parabolic-point measure.
theorem
CKN.setIntegral_parabolic_to_product
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
:
∫ (p : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, F p = ∫ (q : Foundation.Parabolic.Vec3 × ℝ) in Ω ×ˢ I, F (Foundation.Parabolic.parabolicHomeomorph.symm q)
Set integrals on a space-time product agree in CKN and product coordinates.
theorem
CKN.locallyIntegrableOn_pi_eval
{X : Type u_1}
{ι : Type u_2}
{E : Type u_3}
[TopologicalSpace X]
[MeasurableSpace X]
[Fintype ι]
[NormedAddCommGroup E]
{s : Set X}
{f : X → ι → E}
{μ : MeasureTheory.Measure X}
(hf : MeasureTheory.LocallyIntegrableOn f s μ)
(i : ι)
:
MeasureTheory.LocallyIntegrableOn (fun (x : X) => f x i) s μ
Each coordinate of a locally integrable finite-product-valued function is locally integrable.