OAI/RingTheory/BassTrace/MarkedArea.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BassTrace.Sparse.Cuts.MarkedFamily.trace_space line 20
  2. lemma OAI.BassTrace.Sparse.Cuts.MarkedFamily.localConstancy_inter line 27
  3. def OAI.BassTrace.Sparse.Cuts.MarkedFamily.localArea line 40
  4. lemma OAI.BassTrace.Sparse.Cuts.MarkedFamily.localArea_locallyConstant line 44
  5. lemma OAI.BassTrace.Sparse.Cuts.MarkedFamily.localArea_lt_top line 50
  6. lemma OAI.BassTrace.Sparse.IsLocallyConstant.lintegral_lt_top line 103
  7. def OAI.BassTrace.Sparse.simplexEnumeration line 133
  8. def OAI.BassTrace.Sparse.simplexVertices line 136
  9. def OAI.BassTrace.Sparse.simplexCoordinates line 139
  10. lemma OAI.BassTrace.Sparse.simplexCoordinates_sum line 143
  11. def OAI.BassTrace.Sparse.simplexGraph line 154
  12. lemma OAI.BassTrace.Sparse.simplexGraph_connected line 158
  13. def OAI.BassTrace.Sparse.SourceTop line 165
  14. instance OAI.BassTrace.Sparse.(instance at line 168) line 168
  15. def OAI.BassTrace.Sparse.sourceInterior line 171
  16. def OAI.BassTrace.Sparse.originalArea line 174
  17. lemma OAI.BassTrace.Sparse.originalArea_locallyConstant line 182
  18. lemma OAI.BassTrace.Sparse.originalArea_lt_top line 190
  19. lemma OAI.BassTrace.Sparse.sourceTop_stabilizer_finite line 202
  20. def OAI.BassTrace.Sparse.normalizedArea line 214
  21. lemma OAI.BassTrace.Sparse.normalizedArea_lt_top line 222
  22. lemma OAI.BassTrace.Sparse.normalizedArea_filtration_lt_top line 239
  23. lemma OAI.BassTrace.Sparse.exists_nearMinimizer line 255