SimplexVolume.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Volumes of standard simplices and their products

The simplex-volume calculation below uses Tonelli's theorem and induction on the dimension. At first coordinate t, the remaining section is a simplex of radius r - t; its volume is integrated over 0 ≤ t ≤ r. The Euclidean versions use the measure-preserving equivalence between coordinate space and EuclideanSpace. The product formula is proved using the product Lebesgue measure under the canonical splitting of Fin (p + q).

def OAI.ProjectionCounterexample.coordinateSimplex line 31
Source documentation
The coordinate standard simplex with nonnegative coordinates and sum at most r.
```
def coordinateSimplex (n : ℕ) (r : ℝ) : Set (Fin n → ℝ) :=
…
```
theorem OAI.ProjectionCounterexample.coordinateSimplex_measurableSet line 34
theorem OAI.ProjectionCounterexample.coordinateSimplex_eq_empty_of_neg line 39
theorem OAI.ProjectionCounterexample.integral_simplex_slice line 46
theorem OAI.ProjectionCounterexample.volume_coordinateSimplex line 63
theorem OAI.ProjectionCounterexample.volume_unit_coordinateSimplex line 113
Source documentation
The standard simplex has ordinary Lebesgue volume 1 / n!.
```
theorem volume_unit_coordinateSimplex (n : ℕ) :
    volume (coordinateSimplex n 1) = ENNReal.ofReal (1 / (n.factorial : ℝ)) := by
…
```
Mentions: OAI.ProjectionCounterexample.coordinateSimplex
theorem OAI.ProjectionCounterexample.volume_linearImage_unit_coordinateSimplex line 118
Source documentation
Exact volume of a possibly degenerate linear image of the coordinate simplex.
```
theorem volume_linearImage_unit_coordinateSimplex (n : ℕ)
    (f : (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ)) :
    volume (f '' coordinateSimplex n 1) =
      ENNReal.ofReal (|LinearMap.det f| / (n.factorial : ℝ)) := by
…
```
Mentions: OAI.ProjectionCounterexample.coordinateSimplex

theorem OAI.ProjectionCounterexample.volume_unit_euclideanSimplex line 128

Source documentation

The same volume statement in Euclidean space with its canonical Euclidean measure.

theorem volume_unit_euclideanSimplex (n : ℕ) :
    volume {x : EuclideanSpace ℝ (Fin n) | (∀ i, 0 ≤ x i) ∧ ∑ i, x i ≤ 1} =
      ENNReal.ofReal (1 / (n.factorial : ℝ)) := by
…

theorem OAI.ProjectionCounterexample.realVolume_unit_euclideanSimplex line 138

Source documentation

Real-valued version of the Euclidean simplex volume.

theorem realVolume_unit_euclideanSimplex (n : ℕ) :
    (volume {x : EuclideanSpace ℝ (Fin n) |
      (∀ i, 0 ≤ x i) ∧ ∑ i, x i ≤ 1}).toReal = 1 / (n.factorial : ℝ) := by
…

def OAI.ProjectionCounterexample.coordinateSimplexProduct line 146
Source documentation
The coordinate product, with the first p and last q coordinates separated.
```
def coordinateSimplexProduct (p q : ℕ) : Set (Fin (p + q) → ℝ) :=
…
```
theorem OAI.ProjectionCounterexample.volume_coordinateSimplexProduct line 151
Source documentation
The product-volume identity uses the actual product Lebesgue measure.
```
theorem volume_coordinateSimplexProduct (p q : ℕ) :
    volume (coordinateSimplexProduct p q) =
      ENNReal.ofReal (1 / ((p.factorial : ℝ) * (q.factorial : ℝ))) := by
…
```
Mentions: OAI.ProjectionCounterexample.coordinateSimplexProduct

theorem OAI.ProjectionCounterexample.volume_euclideanSimplexProduct line 175

Source documentation

Product-simplex volume in the canonical Euclidean coordinates.

theorem volume_euclideanSimplexProduct (p q : ℕ) :
    volume {x : EuclideanSpace ℝ (Fin (p + q)) |
      ((∀ i : Fin p, 0 ≤ x (Fin.castAdd q i)) ∧
        ∑ i : Fin p, x (Fin.castAdd q i) ≤ 1) ∧
      ((∀ i : Fin q, 0 ≤ x (Fin.natAdd p i)) ∧
        ∑ i : Fin q, x (Fin.natAdd p i) ≤ 1)} =
      ENNReal.ofReal (1 / ((p.factorial : ℝ) * (q.factorial : ℝ))) := by
…