Coarse-graining support: Support.Sobolev.CubeEmbedding.PeelFubini

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

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 HCPolySupport.integral_peel_coord {n : ℕ} (i : Fin (n + 1)) {f : Vec (n + 1) → ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) : ∫ (x : Vec (n + 1)), f x = ∫ (z : Vec n) (t : ℝ), f (i.insertNth t z)

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).