Coordinate slicing of half-open unit cells in Vec d.

theorem AVenhance.Infra.Torus.integral_peel_coord {n : ℕ} (i : Fin (n + 1)) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : Homogenization.Vec (n + 1) → E} (hf : MeasureTheory.Integrable f MeasureTheory.volume) : ∫ (x : Homogenization.Vec (n + 1)), f x = ∫ (z : Homogenization.Vec n) (t : ℝ), f (i.insertNth t z)

Fubini along a selected coordinate, for any complete real normed target. This is the vector-valued extension of CoarseGraining's integral_peel_coord.

theorem AVenhance.Infra.Torus.mem_unitCell_insertNth_iff {n : ℕ} (i : Fin (n + 1)) (t : ℝ) (z : Homogenization.Vec n) : i.insertNth t z ∈ unitCell (n + 1) ↔ t ∈ Set.Ioc 0 1 ∧ z ∈ unitCell n

Inserting a coordinate into a vector lies in the unit cell exactly when both the peeled coordinate and the remaining vector lie in their cells.

theorem AVenhance.Infra.Torus.integral_unitCell_peel_coord {n : ℕ} (i : Fin (n + 1)) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : Homogenization.Vec (n + 1) → E} (hf : MeasureTheory.IntegrableOn f (unitCell (n + 1)) MeasureTheory.volume) : ∫ (x : Homogenization.Vec (n + 1)) in unitCell (n + 1), f x = ∫ (z : Homogenization.Vec n) in unitCell n, ∫ (t : ℝ) in Set.Ioc 0 1, f (i.insertNth t z)

Restricted-cell Fubini, peeling an arbitrary coordinate of Vec (n+1). The remaining variables are integrated over their own half-open unit cell.

theorem AVenhance.Infra.Torus.integral_unitCell2_peel_coord (i : Fin 2) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : Homogenization.Vec 2 → E} (hf : MeasureTheory.IntegrableOn f (unitCell 2) MeasureTheory.volume) : ∫ (x : Homogenization.Vec 2) in unitCell 2, f x = ∫ (z : Homogenization.Vec 1) in unitCell 1, ∫ (t : ℝ) in Set.Ioc 0 1, f (i.insertNth t z)

The two-dimensional instance of restricted-cell coordinate slicing.