OAI/MeasureTheory/Falconer/Slicing/GramSchmidtVolume.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The Gram volume is the product of successive residual lengths

  1. theorem OAI.Falconer.gram_volume_eq_abs_basis_det line 12
  2. theorem OAI.Falconer.gramSchmidt_basis_diagonal_abs line 19
  3. theorem OAI.Falconer.gram_volume_eq_residual_product line 42
  4. theorem OAI.Falconer.small_gram_volume_has_small_residual line 51