Dimension recurrence for unit simplex volume
OpenOAI.PiExponent.DeterminantContradiction.unit_simplex_volume_succnumber-theoryopenai-pi-exponent-017
The volume of the nonnegative unit simplex in dimension k+1 equals its dimension-k volume divided by k+1.
Preamble
import Mathlib open scoped BigOperators
Formal statement
theorem OAI.PiExponent.DeterminantContradiction.unit_simplex_volume_succ (k : ℕ) :
(MeasureTheory.volume
{x : Fin (k + 1) → ℝ | (∀ i, 0 ≤ x i) ∧ ∑ i : Fin (k + 1), x i ≤ 1}).toReal =
((MeasureTheory.volume
{x : Fin k → ℝ | (∀ i, 0 ≤ x i) ∧ ∑ i : Fin k, x i ≤ 1}).toReal) /
((k + 1 : ℕ) : ℝ) := by sorrySource