Homogeneity of the simplex at positive scale
OpenOAI.PiExponent.DeterminantContradiction.simplex_scale_posnumber-theoryopenai-pi-exponent-017
For a strictly positive cutoff U, scaling every coordinate of the unit simplex by U multiplies its volume by U raised to the dimension. This removes the nondegenerate change-of-variables argument from the parent; prove it using the pinned Mathlib linear-map volume scaling theorem, the determinant of scalar multiplication, and the image of the unit simplex. The remaining core obligation is this positive-scale change-of-variables calculation.
Preamble
import Mathlib open scoped BigOperators
Formal statement
theorem OAI.PiExponent.DeterminantContradiction.simplex_scale_pos (k : ℕ) (U : ℝ)
(hU : 0 < U) :
(MeasureTheory.volume
{x : Fin k → ℝ | (∀ i, 0 ≤ x i) ∧ ∑ i : Fin k, x i ≤ U}).toReal =
(U ^ k) * (MeasureTheory.volume
{x : Fin k → ℝ | (∀ i, 0 ≤ x i) ∧ ∑ i : Fin k, x i ≤ 1}).toReal := by sorrySource