OAI/Combinatorics/Coboundary/Skeleton.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Skeleton-weight identities and conversion of raw cosystolic estimates to the finite weighted norms.

  1. lemma OAI.CoboundaryExpanders.FatLadders.delta_image line 25
  2. lemma OAI.CoboundaryExpanders.FatLadders.norm_image line 35
  3. def OAI.CoboundaryExpanders.Complex.rawCochain line 58
  4. def OAI.CoboundaryExpanders.Complex.ofRaw line 61
  5. lemma OAI.CoboundaryExpanders.Complex.ofRaw_rawCochain line 63
  6. lemma OAI.CoboundaryExpanders.Complex.ofRaw_add line 68
  7. lemma OAI.CoboundaryExpanders.Complex.coboundary_ofRaw line 71
  8. lemma OAI.CoboundaryExpanders.Complex.cofaceCount_zero_of_not_mem line 93
  9. lemma OAI.CoboundaryExpanders.Complex.norm_ofRaw line 101
  10. lemma OAI.CoboundaryExpanders.Complex.normalizer_pos line 126
  11. lemma OAI.CoboundaryExpanders.Complex.raw_norm_eq_mul line 135
  12. theorem OAI.CoboundaryExpanders.Complex.cosystolic_of_raw line 142
  13. lemma OAI.CoboundaryExpanders.FatLadders.correction_image line 186
  14. lemma OAI.CoboundaryExpanders.CosetConstruction.labelled_cofaces line 251
  15. theorem OAI.CoboundaryExpanders.CosetConstruction.cosystolic_of_typed_raw line 277
  16. theorem OAI.CoboundaryExpanders.Complex.skeleton_cosystolic_of_ambient line 299
  17. theorem OAI.CoboundaryExpanders.Construction.actual_uniform_cosystolic line 325