OAI/RingTheory/BassTrace/BarycentricBounds.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BassTrace.BarycentricChains.cone_square line 21
  2. lemma OAI.BassTrace.BarycentricChains.vertices_image line 27
  3. lemma OAI.BassTrace.BarycentricChains.labelMap_basis_recursion line 32
  4. def OAI.BassTrace.BarycentricChains.filteredLabel line 40
  5. def OAI.BassTrace.BarycentricChains.filteredCount line 46
  6. lemma OAI.BassTrace.BarycentricChains.labelMap_eq_filtered line 50
  7. lemma OAI.BassTrace.BarycentricChains.eraseFace_injective line 92
  8. lemma OAI.BassTrace.BarycentricChains.filteredCount_eq_zero line 98
  9. lemma OAI.BassTrace.BarycentricChains.filteredCount_pos_level line 102
  10. lemma OAI.BassTrace.BarycentricChains.sum_facets_fiberwise line 108
  11. lemma OAI.BassTrace.BarycentricChains.incidencePairs_card_le line 124
  12. lemma OAI.BassTrace.BarycentricChains.filteredCount_sum_step line 140
  13. def OAI.BassTrace.BarycentricChains.ActualFlags.level line 176
  14. lemma OAI.BassTrace.BarycentricChains.ActualFlags.level_face line 179
  15. lemma OAI.BassTrace.BarycentricChains.ActualFlags.count_pos_zero line 182
  16. lemma OAI.BassTrace.BarycentricChains.ActualFlags.localFaces_erase line 205
  17. lemma OAI.BassTrace.BarycentricChains.ActualFlags.count_sum_step line 212
  18. lemma OAI.BassTrace.BarycentricChains.ActualFlags.count_sum_bound line 233
  19. def OAI.BassTrace.BarycentricChains.coneLeft line 261
  20. lemma OAI.BassTrace.BarycentricChains.cone_single_wedge line 266
  21. lemma OAI.BassTrace.BarycentricChains.cone_uniform_wedge line 272
  22. lemma OAI.BassTrace.BarycentricChains.norm_uniform_cone_wedge line 283
  23. lemma OAI.BassTrace.BarycentricChains.filteredLabel_norm line 302
  24. lemma OAI.BassTrace.BarycentricChains.norm_sign_complex_le line 353
  25. lemma OAI.BassTrace.BarycentricChains.labeled_chain_bound line 356
  26. lemma OAI.BassTrace.BarycentricChains.ActualFlags.singleton_mean line 416
  27. lemma OAI.BassTrace.BarycentricChains.ActualFlags.zeroFaces_card_le line 420
  28. lemma OAI.BassTrace.BarycentricChains.ActualFlags.zeroFaces_real_le_count line 440