OAI/RingTheory/BassTrace/SimplexVolume.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Euclidean coordinate simplex volume from the volume of the ℓ¹ ball and sign symmetry.

  1. def OAI.BassTrace.Sparse.standardSolidSimplex line 13
  2. def OAI.BassTrace.Sparse.l1UnitPolytope line 16
  3. def OAI.BassTrace.Sparse.signReflection line 18
  4. def OAI.BassTrace.Sparse.signChamber line 21
  5. lemma OAI.BassTrace.Sparse.measurableSet_standardSolidSimplex line 24
  6. lemma OAI.BassTrace.Sparse.signReflection_measurePreserving line 34
  7. lemma OAI.BassTrace.Sparse.measurableSet_signChamber line 45
  8. lemma OAI.BassTrace.Sparse.volume_signChamber line 49
  9. lemma OAI.BassTrace.Sparse.signChamber_mem_iff line 54
  10. lemma OAI.BassTrace.Sparse.union_signChamber line 87
  11. lemma OAI.BassTrace.Sparse.signChamber_aedisjoint line 102
  12. lemma OAI.BassTrace.Sparse.volume_l1UnitPolytope line 115
  13. theorem OAI.BassTrace.Sparse.volume_standardSolidSimplex line 129