Coordinate-peeling Fubini on Vec d #
Reusable slicing lemma: an integral over Vec (n+1) = Fin (n+1) → ℝ against
Lebesgue volume equals the iterated integral obtained by peeling off a chosen
coordinate i as the inner one-dimensional line integral (the remaining
coordinates outer). The line through z : Vec n in direction i is
t ↦ i.insertNth t z.
This is the tool into which the single-face reflection transport feeds its per-line one-dimensional integration by parts.
theorem
Homogenization.integral_peel_coord
{n : ℕ}
(i : Fin (n + 1))
{f : Vec (n + 1) → ℝ}
(hf : MeasureTheory.Integrable f MeasureTheory.volume)
:
Coordinate-peeling Fubini.
For f : Vec (n+1) → ℝ integrable against volume and a coordinate i, the
integral equals the iterated integral with the i-th coordinate innermost:
∫ x, f x = ∫ z, ∫ t, f (i.insertNth t z).