Slicing and scaling standard-simplex integrals

theorem MeasureTheory.volume_preserving_funSplitAt {ι : Type u} [Fintype ι] (i : ι) : MeasurePreserving (⇑(Homeomorph.funSplitAt ℝ i)) volume (volume.prod volume)

Splitting one coordinate from a finite real coordinate space preserves product Lebesgue measure.

def MeasureTheory.stdSimplexDoubleComplementEquiv {ι : Type u} (i j : ι) (hij : i ≠ j) : { q : { q : ι // q ≠ i } // q ≠ ⟨j, ⋯⟩ } ≃ { q : { q : ι // q ≠ j } // q ≠ ⟨i, hij⟩ }

Reindexing the coordinates left after deleting two distinct indices in opposite orders.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.lintegral_posSimplex_scale {α : Type u_1} [Fintype α] (i : α) (c : ℝ) (hc : 0 < c) (g : ({ j : α // j ≠ i } → ℝ) → ENNReal) : ∫⁻ (y : { j : α // j ≠ i } → ℝ) in posSimplex { j : α // j ≠ i } c, g y = ENNReal.ofReal (c ^ (Fintype.card α - 1)) * ∫⁻ (x : { j : α // j ≠ i } → ℝ) in posSimplex { j : α // j ≠ i } 1, g (c • x)

Scaling a positive-simplex slice in the nonnegative integral.

theorem MeasureTheory.stdSimplexCoordMap_split_eq {ι : Type u} [Fintype ι] (i j : ι) (hij : i ≠ j) (t : ℝ) (v : { q : ι // q ≠ i } → ℝ) (h_sum : ∑ q : { q : ι // q ≠ i }, v q = 1) : let C := { q : { q : ι // q ≠ j } // q ≠ ⟨i, hij⟩ }; have e := stdSimplexDoubleComplementEquiv i j hij; stdSimplexCoordMap j ((Homeomorph.funSplitAt ℝ ⟨i, hij⟩).symm (t, fun (q : C) => (1 - t) * v ↑(e.symm q))) = stdSimplexCoordMap i fun (q : { j : ι // j ≠ i }) => (1 - t) * v q

Equivalence of the nested-slice coordinate map and the directly scaled coordinate map.

theorem MeasureTheory.integral_posSimplex_inner_slice {ι : Type u} [Fintype ι] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (i j : ι) (hij : i ≠ j) (t : ℝ) (ht : t ∈ Set.Ico 0 1) (f : (ι → ℝ) → E) : let C := { q : { q : ι // q ≠ j } // q ≠ ⟨i, hij⟩ }; ∫ (y : C → ℝ) in posSimplex C (1 - t), f (stdSimplexCoordMap j ((Homeomorph.funSplitAt ℝ ⟨i, hij⟩).symm (t, y))) = (1 - t) ^ (Fintype.card ι - 2) • ∫ (v : { q : ι // q ≠ i } → ℝ) in Convexity.StdSimplex.coordinateSet ℝ { q : ι // q ≠ i }, f (stdSimplexCoordMap i fun (q : { j : ι // j ≠ i }) => (1 - t) * v q) ∂Measure.stdSimplexMeasure

Evaluates the inner sliced integral by reindexing the double-complement and scaling.

theorem MeasureTheory.lintegral_posSimplex_inner_slice {ι : Type u} [Fintype ι] (i j : ι) (hij : i ≠ j) (t : ℝ) (ht : t ∈ Set.Ico 0 1) (f : (ι → ℝ) → ENNReal) : let C := { q : { q : ι // q ≠ j } // q ≠ ⟨i, hij⟩ }; ∫⁻ (y : C → ℝ) in posSimplex C (1 - t), f (stdSimplexCoordMap j ((Homeomorph.funSplitAt ℝ ⟨i, hij⟩).symm (t, y))) = ENNReal.ofReal ((1 - t) ^ (Fintype.card ι - 2)) * ∫⁻ (v : { q : ι // q ≠ i } → ℝ) in Convexity.StdSimplex.coordinateSet ℝ { q : ι // q ≠ i }, f (stdSimplexCoordMap i fun (q : { j : ι // j ≠ i }) => (1 - t) * v q) ∂Measure.stdSimplexMeasure

Evaluates a nonnegative inner sliced integral by reindexing the double complement and scaling.

theorem MeasureTheory.lintegral_stdSimplex_split_at {ι : Type u} [Fintype ι] (i : ι) [Nontrivial ι] (f : (ι → ℝ) → ENNReal) (hf : Measurable f) : ∫⁻ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, f u ∂Measure.stdSimplexMeasure = ∫⁻ (t : ℝ) in Set.Icc 0 1, ENNReal.ofReal ((1 - t) ^ (Fintype.card ι - 2)) * ∫⁻ (v : { j : ι // j ≠ i } → ℝ) in Convexity.StdSimplex.coordinateSet ℝ { j : ι // j ≠ i }, f (stdSimplexCoordMap i fun (j : { j : ι // j ≠ i }) => (1 - t) * v j) ∂Measure.stdSimplexMeasure

Tonelli reduction of a nonnegative integral over the standard simplex after separating one coordinate. Unlike integral_stdSimplex_split_at, no integrability hypothesis is required.

theorem MeasureTheory.integral_stdSimplex_split_at {ι : Type u} [Fintype ι] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (i : ι) [Nontrivial ι] (f : (ι → ℝ) → E) (hf : IntegrableOn f (Convexity.StdSimplex.coordinateSet ℝ ι) Measure.stdSimplexMeasure) : ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, f u ∂Measure.stdSimplexMeasure = ∫ (t : ℝ) in Set.Icc 0 1, (1 - t) ^ (Fintype.card ι - 2) • ∫ (v : { j : ι // j ≠ i } → ℝ) in Convexity.StdSimplex.coordinateSet ℝ { j : ι // j ≠ i }, f (stdSimplexCoordMap i fun (j : { j : ι // j ≠ i }) => (1 - t) * v j) ∂Measure.stdSimplexMeasure

Evaluates an integral over the standard simplex by separating out the i-th coordinate. This theorem provides the standard Fubini reduction (integration by slices) for the simplex. It expresses the integral of a function f over the $(k-1)$-simplex (where $k$ is card ι) as an iterated integral:

1. An outer 1D integral over the isolated coordinate $t \in [0, 1]$.
2. An inner integral over the $(k-2)$-simplex of the remaining coordinates $v$. Because the remaining coordinates are subject to the constraint $\sum v = 1 - t$, they are scaled by $(1 - t)$ to map them back to a standard unit $(k-1)$-simplex. This change of variables introduces a Jacobian determinant factor of $(1 - t)^{k - 2}$.