Documentation

LeanPool.Feige.GrunbaumImport

Basic interface to the Grünbaum formalization #

This file registers the first, purely measure-theoretic part of the bridge between the coordinate-function model used by Feige and Mathlib's EuclideanSpace model used by Grunbaum.

source
def Feige.simplexToEuclidean (n : ℕ) :
(Fin n → ℝ) → Grunbaum.SimplexE n

The canonical passage from coordinate functions to Euclidean space.

Equations
Instances For
    source
    theorem Feige.measurable_simplexToEuclidean (n : ℕ) :
    Measurable (simplexToEuclidean n)
    source
    @[simp]
    theorem Feige.simplexToEuclidean_apply (n : ℕ) (x : Fin n → ℝ) (i : Fin n) :
    (simplexToEuclidean n x).ofLp i = x i
    source
    theorem Feige.simplexToEuclidean_mem_simplexSet_iff (n : ℕ) (x : Fin n → ℝ) :
    simplexToEuclidean n x ∈ Grunbaum.simplexSet n ↔ x ∈ fullSimplex (Fin n)

    The two projects use exactly the same standard simplex, modulo the canonical PiLp.toLp wrapper.

    source
    theorem Feige.simplexToEuclidean_preimage_simplexSet (n : ℕ) :
    simplexToEuclidean n ⁻¹' Grunbaum.simplexSet n = fullSimplex (Fin n)
    source
    theorem Feige.volume_simplexSet_eq_volume_fullSimplex (n : ℕ) :
    MeasureTheory.volume (Grunbaum.simplexSet n) = MeasureTheory.volume (fullSimplex (Fin n))

    Lebesgue volume of the simplex is unchanged by the canonical coordinate-function/Euclidean-space identification.

    source
    theorem Feige.volume_simplexSet_inter_eq_volume_fullSimplex_inter_preimage (n : ℕ) {A : Set (Grunbaum.SimplexE n)} (hA : MeasurableSet A) :
    MeasureTheory.volume (Grunbaum.simplexSet n ∩ A) = MeasureTheory.volume (fullSimplex (Fin n) ∩ simplexToEuclidean n ⁻¹' A)

    Transport of intersections with the standard simplex. This is the form needed to compare the two normalized halfspace-volume ratios.