Solid simplex geometry and volume

def posSimplexFin (n : ℕ) (r : ℝ) : Set (Fin n → ℝ)

The positive simplex of radius r in coordinates indexed by Fin n: nonnegative vectors whose coordinate sum is at most r.

Equations

• posSimplexFin n r = {x : Fin n → ℝ | (∀ (i : Fin n), 0 ≤ x i) ∧ ∑ i : Fin n, x i ≤ r}

theorem measurableSet_posSimplexFin (n : ℕ) (r : ℝ) : MeasurableSet (posSimplexFin n r)

The finite-coordinate positive simplex is measurable.

theorem volume_posSimplexFin_zero (r : ℝ) (hr : 0 ≤ r) : MeasureTheory.volume (posSimplexFin 0 r) = ENNReal.ofReal r ^ 0 / ↑(Nat.factorial 0)

The volume formula for the zero-dimensional positive simplex.

def posSimplexFinSuccSlices (n : ℕ) (r : ℝ) : Set (ℝ × (Fin n → ℝ))

The product-coordinate presentation of posSimplexFin (n + 1) r, obtained by separating the zeroth coordinate.

Equations

• posSimplexFinSuccSlices n r = {p : ℝ × (Fin n → ℝ) | 0 ≤ p.1 ∧ (∀ (i : Fin n), 0 ≤ p.2 i) ∧ p.1 + ∑ i : Fin n, p.2 i ≤ r}

theorem measurableSet_posSimplexFinSuccSlices (n : ℕ) (r : ℝ) : MeasurableSet (posSimplexFinSuccSlices n r)

The product-coordinate presentation of a positive simplex is measurable.

theorem image_posSimplexFin_piFinSuccAbove (n : ℕ) (r : ℝ) : have e := MeasurableEquiv.piFinSuccAbove (fun (x : Fin (n + 1)) => ℝ) 0; ⇑e '' posSimplexFin (n + 1) r = posSimplexFinSuccSlices n r

Separating the zeroth coordinate maps a positive (n + 1)-simplex to its product-coordinate presentation.

theorem preimage_posSimplexFinSuccSlices_of_mem (n : ℕ) (r t : ℝ) (ht : t ∈ Set.Icc 0 r) : Prod.mk t ⁻¹' posSimplexFinSuccSlices n r = posSimplexFin n (r - t)

A slice of the product-coordinate presentation at t ∈ [0, r] is the positive simplex of radius r - t.

theorem preimage_posSimplexFinSuccSlices_eq_empty_of_not_mem (n : ℕ) (r t : ℝ) (ht : t ∉ Set.Icc 0 r) : Prod.mk t ⁻¹' posSimplexFinSuccSlices n r = ∅

Outside [0, r], the slices in the product-coordinate presentation are empty.

theorem lintegral_Icc_sub_pow_div_factorial (n : ℕ) (r : ℝ) (hr : 0 ≤ r) : ∫⁻ (t : ℝ) in Set.Icc 0 r, ENNReal.ofReal (r - t) ^ n / ↑n.factorial = ENNReal.ofReal r ^ (n + 1) / ↑(n + 1).factorial

The one-dimensional integral used in the positive-simplex volume induction.

theorem volume_posSimplexFin_succ (n : ℕ) (ih : ∀ (r : ℝ), 0 ≤ r → MeasureTheory.volume (posSimplexFin n r) = ENNReal.ofReal r ^ n / ↑n.factorial) (r : ℝ) (hr : 0 ≤ r) : MeasureTheory.volume (posSimplexFin (n + 1) r) = ENNReal.ofReal r ^ (n + 1) / ↑(n + 1).factorial

The induction step for the volume of a positive simplex, obtained by slicing off its first coordinate.

theorem volume_posSimplexFin (n : ℕ) (r : ℝ) (hr : 0 ≤ r) : MeasureTheory.volume (posSimplexFin n r) = ENNReal.ofReal r ^ n / ↑n.factorial

The n-dimensional volume of the positive simplex of radius r is r ^ n / n!.

def posSimplex (α : Type u_1) [Fintype α] (r : ℝ) : Set (α → ℝ)

The positive simplex of radius r indexed by an arbitrary finite type: nonnegative vectors whose coordinate sum is at most r.

Equations

• posSimplex α r = {x : α → ℝ | (∀ (i : α), 0 ≤ x i) ∧ ∑ i : α, x i ≤ r}

def posSimplexSlices {α : Type u_1} [Fintype α] (i : α) (r : ℝ) : Set (ℝ × ({ j : α // j ≠ i } → ℝ))

The product-coordinate presentation of a positive simplex obtained by separating the coordinate i.

Equations

• posSimplexSlices i r = {p : ℝ × ({ j : α // j ≠ i } → ℝ) | 0 ≤ p.1 ∧ (∀ (j : { j : α // j ≠ i }), 0 ≤ p.2 j) ∧ p.1 + ∑ j : { j : α // j ≠ i }, p.2 j ≤ r}

theorem posSimplex_eq_empty_of_neg {α : Type u_1} [Fintype α] {r : ℝ} (hr : r < 0) : posSimplex α r = ∅

A positive simplex of negative radius is empty.

theorem measurableSet_posSimplex (α : Type u_1) [Fintype α] (r : ℝ) : MeasurableSet (posSimplex α r)

A positive simplex is measurable.

theorem image_posSimplex_funSplitAt {α : Type u_1} [Fintype α] (i : α) (r : ℝ) : ⇑(Homeomorph.funSplitAt ℝ i) '' posSimplex α r = posSimplexSlices i r

Separating one coordinate identifies a positive simplex with its product-coordinate presentation.

theorem measurableSet_posSimplexSlices {α : Type u_1} [Fintype α] (i : α) (r : ℝ) : MeasurableSet (posSimplexSlices i r)

The product-coordinate presentation of a positive simplex is measurable.

theorem preimage_posSimplexSlices_of_mem {α : Type u_1} [Fintype α] (i : α) (r t : ℝ) (ht : t ∈ Set.Icc 0 r) : Prod.mk t ⁻¹' posSimplexSlices i r = posSimplex { j : α // j ≠ i } (r - t)

A slice of posSimplexSlices i r at a point of [0, r] is the positive simplex of radius r - t in the remaining coordinates.

theorem preimage_posSimplexSlices_eq_empty_of_not_mem {α : Type u_1} [Fintype α] (i : α) (r t : ℝ) (ht : t ∉ Set.Icc 0 r) : Prod.mk t ⁻¹' posSimplexSlices i r = ∅

Outside [0, r], every slice of posSimplexSlices i r is empty.

theorem volume_posSimplex (α : Type u_1) [Fintype α] (r : ℝ) (hr : 0 ≤ r) : MeasureTheory.volume (posSimplex α r) = ENNReal.ofReal r ^ Fintype.card α / ↑(Fintype.card α).factorial

The volume of the positive simplex indexed by α is r ^ Fintype.card α / (Fintype.card α)!.

theorem volume_posSimplex_toReal (α : Type u_1) [Fintype α] (r : ℝ) (hr : 0 ≤ r) : (MeasureTheory.volume (posSimplex α r)).toReal = r ^ Fintype.card α / ↑(Fintype.card α).factorial

Real-valued form of the positive-simplex volume formula.