OAI/Geometry/Coboundary/LatticeCones.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Bounded-chamber and codistance attachments, lattice acyclicity, and uniform positive coset exactness.

  1. theorem OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.based_at line 19
  2. theorem OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.normalization_core line 47
  3. def OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.RootInterval line 67
  4. def OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.normalizeModule line 69
  5. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.normalizeModule_of_bounded line 73
  6. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.rootInterval_bounded line 77
  7. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.normalizeModule_stage line 79
  8. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.normalizeModule_initial line 82
  9. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.normalizeModule_terminal line 85
  10. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.rootInterval_stage line 88
  11. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.normalizeModule_injective line 92
  12. def OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.liftModule line 119
  13. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.liftModule_normalize line 122
  14. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.liftModule_vertex line 128
  15. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.normalizeModule_stage_succ line 140
  16. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.descentCore_card line 151
  17. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.root_mem_core_iff line 155
  18. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.fixedStages_image line 166
  19. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.cut_rank_eq_core_card line 199
  20. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.fixed_stages_of_core line 227
  21. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.core_eq_of_window_fixed line 244
  22. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.fixedStages_top line 269
  23. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.fixedStages_bottom line 272
  24. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.fixedStages_interval line 276
  25. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.core_has_fixed_representative line 280
  26. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.lift_link_witness line 304
  27. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.normalized_link_lift line 316
  28. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.rooted_link_interval line 339
  29. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.normalized_link_map line 348
  30. theorem OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.codistanceLink_exact_of_rooted line 384
  31. theorem OAI.CoboundaryExpanders.RationalLattices.uniform_codistanceLink_exact line 412
  32. theorem OAI.CoboundaryExpanders.RationalLattices.codistanceBlock_relative_of_link line 448
  33. theorem OAI.CoboundaryExpanders.RationalLattices.codistanceStage_relative_of_links line 507
  34. theorem OAI.CoboundaryExpanders.RationalLattices.uniform_codistanceStage_zero_exact line 534
  35. lemma OAI.CoboundaryExpanders.RationalLattices.positive_power_equation line 554
  36. lemma OAI.CoboundaryExpanders.RationalLattices.mem_level_cut line 566
  37. lemma OAI.CoboundaryExpanders.RationalLattices.positiveAction_cut_le_exponents line 592
  38. lemma OAI.CoboundaryExpanders.RationalLattices.positiveAction_mul line 618
  39. lemma OAI.CoboundaryExpanders.RationalLattices.positiveAction_one line 631
  40. lemma OAI.CoboundaryExpanders.RationalLattices.actVertex_one line 635
  41. lemma OAI.CoboundaryExpanders.RationalLattices.actVertex_mul line 640
  42. lemma OAI.CoboundaryExpanders.Construction.U_diagonal_ne_zero line 655
  43. lemma OAI.CoboundaryExpanders.Construction.homothetic_cut_recognition line 662
  44. lemma OAI.CoboundaryExpanders.Construction.act_cut_eq_iff line 731
  45. def OAI.CoboundaryExpanders.Construction.oppositionVertex line 758
  46. lemma OAI.CoboundaryExpanders.Construction.oppositionVertex_mk line 765
  47. lemma OAI.CoboundaryExpanders.Construction.oppositionVertex_injective line 769
  48. lemma OAI.CoboundaryExpanders.Construction.oppositionVertex_face line 778
  49. def OAI.CoboundaryExpanders.Construction.opposition line 790
  50. lemma OAI.CoboundaryExpanders.Construction.opposition_mem_image line 799
  51. lemma OAI.CoboundaryExpanders.Construction.opposition_subcomplex line 809
  52. theorem OAI.CoboundaryExpanders.Construction.opposition_faces_eq_codistance_zero line 823
  53. theorem OAI.CoboundaryExpanders.Construction.uniform_infinite_coset_exact line 839
  54. theorem OAI.CoboundaryExpanders.Construction.uniform_infinite_coset_positive line 859
  55. theorem OAI.CoboundaryExpanders.reduction_to_actual_integral_pro_stability line 878