OAI/RingTheory/BassTrace/ZeroStrata.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BassTrace.Sparse.affineSpan_simplex_constraints line 22
  2. lemma OAI.BassTrace.Sparse.mem_sourceInterior_of_positive line 40
  3. lemma OAI.BassTrace.Sparse.probability_mem_own_sourceInterior line 70
  4. lemma OAI.BassTrace.Sparse.zero_mem_sourceTop_interior line 92
  5. lemma OAI.BassTrace.Sparse.count_chart_image line 120
  6. lemma OAI.BassTrace.Sparse.GraphGeometry.zero_count_ball_le line 164
  7. lemma OAI.BassTrace.Sparse.GraphGeometry.exists_finite_simplex_ball_cover line 199
  8. lemma OAI.BassTrace.Sparse.GraphGeometry.expected_zero_count_bound line 267
  9. lemma OAI.BassTrace.Sparse.zero_inter_simplex_finite line 355
  10. theorem OAI.BassTrace.Sparse.GraphGeometry.exists_sparse_zero_strata line 426