OAI/Combinatorics/Coboundary/FatLadders.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

Balanced chamber weights, fat ladders, degeneracy, and cochain counting.

  1. inductive OAI.CoboundaryExpanders.FatLadders.Path line 20
  2. lemma OAI.CoboundaryExpanders.FatLadders.Path.fat line 27
  3. lemma OAI.CoboundaryExpanders.FatLadders.Path.subset line 28
  4. lemma OAI.CoboundaryExpanders.FatLadders.Path.start line 32
  5. def OAI.CoboundaryExpanders.FatLadders.NoBad line 36
  6. def OAI.CoboundaryExpanders.FatLadders.Minimal line 40
  7. lemma OAI.CoboundaryExpanders.FatLadders.Path.erase_fat line 43
  8. lemma OAI.CoboundaryExpanders.FatLadders.Path.erase_path line 58
  9. theorem OAI.CoboundaryExpanders.FatLadders.exchange line 80
  10. abbrev OAI.CoboundaryExpanders.FatLadders.k line 98
  11. def OAI.CoboundaryExpanders.FatLadders.indicator line 100
  12. def OAI.CoboundaryExpanders.FatLadders.delta line 102
  13. lemma OAI.CoboundaryExpanders.FatLadders.path_indicator_le_support line 104
  14. theorem OAI.CoboundaryExpanders.FatLadders.localized_boundary_support line 110
  15. lemma OAI.CoboundaryExpanders.FatLadders.indicator_vanish line 130
  16. theorem OAI.CoboundaryExpanders.FatLadders.exists_minimal_path line 134
  17. lemma OAI.CoboundaryExpanders.FatLadders.minimal_nonempty line 149
  18. def OAI.CoboundaryExpanders.FatLadders.level line 162
  19. lemma OAI.CoboundaryExpanders.FatLadders.mem_level line 164
  20. def OAI.CoboundaryExpanders.FatLadders.atom line 167
  21. def OAI.CoboundaryExpanders.FatLadders.norm line 170
  22. def OAI.CoboundaryExpanders.FatLadders.starSum line 173
  23. def OAI.CoboundaryExpanders.FatLadders.starNorm line 176
  24. lemma OAI.CoboundaryExpanders.FatLadders.atom_nonneg line 180
  25. lemma OAI.CoboundaryExpanders.FatLadders.norm_nonneg line 183
  26. lemma OAI.CoboundaryExpanders.FatLadders.starNorm_nonneg line 185
  27. lemma OAI.CoboundaryExpanders.FatLadders.atom_add_le line 193
  28. lemma OAI.CoboundaryExpanders.FatLadders.starNorm_add_le line 200
  29. lemma OAI.CoboundaryExpanders.FatLadders.starSum_mono line 209
  30. lemma OAI.CoboundaryExpanders.FatLadders.subsets_card_le line 218
  31. lemma OAI.CoboundaryExpanders.FatLadders.sum_star_le line 223
  32. lemma OAI.CoboundaryExpanders.FatLadders.ladder_difference line 242
  33. lemma OAI.CoboundaryExpanders.FatLadders.ladder_star_difference line 250
  34. def OAI.CoboundaryExpanders.FatLadders.minimalFaces line 261
  35. lemma OAI.CoboundaryExpanders.FatLadders.norm_le_ladders line 264
  36. def OAI.CoboundaryExpanders.FatLadders.NearMinimal line 291
  37. def OAI.CoboundaryExpanders.FatLadders.LinkCorrection line 296
  38. lemma OAI.CoboundaryExpanders.FatLadders.ladder_local_estimate line 303
  39. lemma OAI.CoboundaryExpanders.FatLadders.starNorm_eq_zero_of_card line 337
  40. lemma OAI.CoboundaryExpanders.FatLadders.boundary_star_estimate line 344
  41. theorem OAI.CoboundaryExpanders.FatLadders.fat_ladder_inequality line 366
  42. theorem OAI.CoboundaryExpanders.FatLadders.small_set_expansion line 410
  43. def OAI.CoboundaryExpanders.FatLadders.chamberWeight line 429
  44. lemma OAI.CoboundaryExpanders.FatLadders.chamberWeight_nonneg line 433
  45. lemma OAI.CoboundaryExpanders.FatLadders.chamberWeight_mono line 442
  46. lemma OAI.CoboundaryExpanders.FatLadders.count_cofaces line 454
  47. theorem OAI.CoboundaryExpanders.FatLadders.chamberWeight_balance line 472
  48. structure OAI.CoboundaryExpanders.FatLadders.Balanced line 496
  49. lemma OAI.CoboundaryExpanders.FatLadders.chamberWeight_balanced line 502
  50. lemma OAI.CoboundaryExpanders.FatLadders.choose_le_two_pow line 511
  51. lemma OAI.CoboundaryExpanders.FatLadders.Balanced.star_le line 514
  52. lemma OAI.CoboundaryExpanders.FatLadders.Balanced.weight_eq_zero_of_base line 527
  53. lemma OAI.CoboundaryExpanders.FatLadders.sum_children line 542
  54. def OAI.CoboundaryExpanders.FatLadders.Collision line 565
  55. lemma OAI.CoboundaryExpanders.FatLadders.Collision.card line 570
  56. lemma OAI.CoboundaryExpanders.FatLadders.Collision.base_lt line 581
  57. def OAI.CoboundaryExpanders.FatLadders.collisionMass line 590
  58. def OAI.CoboundaryExpanders.FatLadders.thinBases line 593
  59. lemma OAI.CoboundaryExpanders.FatLadders.collisionMass_nonneg line 596
  60. lemma OAI.CoboundaryExpanders.FatLadders.bad_face_cover line 604
  61. theorem OAI.CoboundaryExpanders.FatLadders.bad_mass_le line 641
  62. lemma OAI.CoboundaryExpanders.FatLadders.level_eq_filter line 672
  63. lemma OAI.CoboundaryExpanders.FatLadders.sum_thinBases line 677
  64. theorem OAI.CoboundaryExpanders.FatLadders.degeneracy_estimate line 690
  65. lemma OAI.CoboundaryExpanders.FatLadders.atom_indicator line 738
  66. def OAI.CoboundaryExpanders.FatLadders.fatAt line 742
  67. def OAI.CoboundaryExpanders.FatLadders.fatFamily line 748
  68. lemma OAI.CoboundaryExpanders.FatLadders.fatFamily_cap line 751
  69. lemma OAI.CoboundaryExpanders.FatLadders.fatFamily_recurrence line 754
  70. lemma OAI.CoboundaryExpanders.FatLadders.fatFamily_top_norm line 775
  71. theorem OAI.CoboundaryExpanders.FatLadders.fat_markov line 789
  72. def OAI.CoboundaryExpanders.FatLadders.fatBudget line 820
  73. lemma OAI.CoboundaryExpanders.FatLadders.fatBudget_pos line 824
  74. def OAI.CoboundaryExpanders.FatLadders.fatThreshold line 830
  75. lemma OAI.CoboundaryExpanders.FatLadders.fatThreshold_pos line 832
  76. theorem OAI.CoboundaryExpanders.FatLadders.fat_mass_bound line 835
  77. lemma OAI.CoboundaryExpanders.FatLadders.fat_empty_false line 871
  78. lemma OAI.CoboundaryExpanders.FatLadders.atom_le_weight line 890
  79. lemma OAI.CoboundaryExpanders.FatLadders.starNorm_le_starSum line 893
  80. def OAI.CoboundaryExpanders.FatLadders.LocalMixing line 896
  81. lemma OAI.CoboundaryExpanders.FatLadders.fat_thin_children line 901
  82. theorem OAI.CoboundaryExpanders.FatLadders.fat_degeneracy_bound line 918
  83. theorem OAI.CoboundaryExpanders.FatLadders.exists_mixing_tolerance line 959