OAI/Geometry/Coboundary/Chambers.lean

GitHub source file

164 declarations, 0 contain sorry, 0 declared as axioms

Bounded and full chambers, codistance, descent cores, and their affine-window descriptions.

  1. lemma OAI.CoboundaryExpanders.PolynomialVectors.powerLinear_injective line 15
  2. lemma OAI.CoboundaryExpanders.PolynomialVectors.powerShift_strictMono line 21
  3. lemma OAI.CoboundaryExpanders.PolynomialVectors.powerShift_mono line 23
  4. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.nextIndex line 28
  5. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.rotateStage line 29
  6. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.rotateStage_castSucc line 32
  7. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.rotateStage_last line 36
  8. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.rotateStage_has line 39
  9. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.rotateStage_strict line 44
  10. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.rotateStage_lower line 58
  11. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.rotate line 67
  12. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.step_degree line 78
  13. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.word_eq_iff line 94
  14. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.rotate_word line 103
  15. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.rotate_window_castSucc line 139
  16. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.rotate_window_last line 147
  17. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.window_mod line 156
  18. theorem OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.rotate_length line 163
  19. lemma OAI.CoboundaryExpanders.PolynomialVectors.leading_combination_max line 186
  20. lemma OAI.CoboundaryExpanders.PolynomialVectors.combination_lowest_pivot line 217
  21. lemma OAI.CoboundaryExpanders.PolynomialVectors.lowest_vector_mem_panel line 249
  22. lemma OAI.CoboundaryExpanders.PolynomialVectors.combination_pivot_degree line 290
  23. lemma OAI.CoboundaryExpanders.PolynomialVectors.span_hasPivots line 312
  24. lemma OAI.CoboundaryExpanders.PolynomialVectors.span_pivotDegree line 317
  25. def OAI.CoboundaryExpanders.PolynomialVectors.diagonalFamily line 328
  26. def OAI.CoboundaryExpanders.PolynomialVectors.diagonalModule line 331
  27. lemma OAI.CoboundaryExpanders.PolynomialVectors.diagonal_leading line 334
  28. lemma OAI.CoboundaryExpanders.PolynomialVectors.diagonal_hasPivots line 343
  29. lemma OAI.CoboundaryExpanders.PolynomialVectors.diagonal_pivotDegree line 348
  30. lemma OAI.CoboundaryExpanders.PolynomialVectors.diagonal_antitone line 354
  31. lemma OAI.CoboundaryExpanders.PolynomialVectors.diagonal_le_span line 368
  32. lemma OAI.CoboundaryExpanders.PolynomialVectors.diagonal_eq_span line 374
  33. lemma OAI.CoboundaryExpanders.PolynomialVectors.diagonal_eq_powerShift line 385
  34. lemma OAI.CoboundaryExpanders.PolynomialVectors.diagonal_injective line 394
  35. lemma OAI.CoboundaryExpanders.PolynomialVectors.diagonal_strictAnti line 404
  36. def OAI.CoboundaryExpanders.PolynomialVectors.wordPrefix line 410
  37. lemma OAI.CoboundaryExpanders.PolynomialVectors.wordPrefix_strict line 413
  38. lemma OAI.CoboundaryExpanders.PolynomialVectors.wordPrefix_zero line 429
  39. lemma OAI.CoboundaryExpanders.PolynomialVectors.wordPrefix_last line 432
  40. def OAI.CoboundaryExpanders.PolynomialVectors.diagonalChamber line 437
  41. lemma OAI.CoboundaryExpanders.PolynomialVectors.diagonalChamber_word line 451
  42. lemma OAI.CoboundaryExpanders.PolynomialVectors.diagonalChamber_window line 463
  43. theorem OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.diagonal_representation line 474
  44. lemma OAI.CoboundaryExpanders.PolynomialVectors.prefix_first_swap line 502
  45. theorem OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.first_panel_lower line 522
  46. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.ext_stage line 591
  47. lemma OAI.CoboundaryExpanders.RationalLattices.FullChamber.panel_realization line 605
  48. theorem OAI.CoboundaryExpanders.RationalLattices.FullChamber.first_panel_previous line 681
  49. lemma OAI.CoboundaryExpanders.PolynomialVectors.powerShift_add line 707
  50. lemma OAI.CoboundaryExpanders.PolynomialVectors.powerShift_zero line 719
  51. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.scale line 727
  52. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.scale_word line 737
  53. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.scale_window line 743
  54. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.scale_length line 749
  55. lemma OAI.CoboundaryExpanders.RationalLattices.polynomial_map_le_standard line 765
  56. def OAI.CoboundaryExpanders.RationalLattices.PolyBounded line 770
  57. lemma OAI.CoboundaryExpanders.RationalLattices.PolyBounded.mono line 773
  58. lemma OAI.CoboundaryExpanders.RationalLattices.PolyBounded.powerShift line 778
  59. lemma OAI.CoboundaryExpanders.RationalLattices.polyBounded_vertex line 785
  60. lemma OAI.CoboundaryExpanders.RationalLattices.normalizedPolynomial_exists line 790
  61. def OAI.CoboundaryExpanders.RationalLattices.normalizedPolynomial line 799
  62. lemma OAI.CoboundaryExpanders.RationalLattices.normalizedPolynomial_spec line 802
  63. lemma OAI.CoboundaryExpanders.RationalLattices.normalizedPolynomial_homothetic line 807
  64. lemma OAI.CoboundaryExpanders.RationalLattices.normalizedPolynomial_eq line 812
  65. lemma OAI.CoboundaryExpanders.RationalLattices.normalizedPolynomial_vertex line 818
  66. lemma OAI.CoboundaryExpanders.RationalLattices.normalizedPolynomial_power line 823
  67. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.stage_bounded line 834
  68. def OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.vertex line 837
  69. def OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.face line 839
  70. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.vertex_homothetic line 841
  71. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.nonterminal_ne line 844
  72. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.vertex_injective line 848
  73. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.card_face line 879
  74. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.face_mem line 883
  75. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.reroot line 909
  76. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.reroot_zero line 911
  77. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.reroot_succ line 912
  78. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.reroot_stage line 914
  79. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.reroot_top line 930
  80. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.reroot_length line 934
  81. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.rotate_bounded line 947
  82. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.scale_vertex line 948
  83. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.scale_face line 951
  84. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.rotate_vertex line 957
  85. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.rotate_face line 978
  86. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.reroot_bounded line 991
  87. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.reroot_face line 995
  88. lemma OAI.CoboundaryExpanders.RationalLattices.homothetic_interval_eq line 1010
  89. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.stage_top_le line 1024
  90. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.mapped_lower line 1027
  91. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.mapped_nonterminal line 1032
  92. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.stage_eq_of_vertex_eq line 1040
  93. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.eq_of_face_of_top line 1053
  94. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.full_vertex line 1082
  95. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.full_face line 1088
  96. theorem OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.normalization line 1094
  97. theorem OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.rooted_panel_previous line 1137
  98. theorem OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.full_rooted_panel_previous line 1161
  99. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.reroot_window_nonwrap line 1177
  100. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.reroot_period line 1198
  101. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.reroot_vertex_nonwrap line 1204
  102. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.last_root_window_one line 1211
  103. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.last_root_vertex_one line 1219
  104. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.reroot_window_zero line 1233
  105. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.reroot_window_one line 1237
  106. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.reroot_vertex_one line 1251
  107. theorem OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.descent_panel_previous line 1264
  108. def OAI.CoboundaryExpanders.RationalLattices.FullChamber.descentCore line 1278
  109. lemma OAI.CoboundaryExpanders.RationalLattices.FullChamber.descentCore_subset line 1281
  110. lemma OAI.CoboundaryExpanders.RationalLattices.FullChamber.descentCore_nonempty line 1285
  111. lemma OAI.CoboundaryExpanders.RationalLattices.FullChamber.descentCore_ne_face line 1294
  112. theorem OAI.CoboundaryExpanders.RationalLattices.FullChamber.face_missing_descent_previous line 1305
  113. theorem OAI.CoboundaryExpanders.AffineWindow.inversion_sorted_blocks line 1320
  114. lemma OAI.CoboundaryExpanders.AffineWindow.sorted_blocks_eq_of_zero line 1335
  115. theorem OAI.CoboundaryExpanders.AffineWindow.inversion_sorted_blocks_minimum line 1345
  116. def OAI.CoboundaryExpanders.AffineWindow.slice line 1364
  117. lemma OAI.CoboundaryExpanders.AffineWindow.mem_slice line 1366
  118. lemma OAI.CoboundaryExpanders.AffineWindow.slice_nodup line 1380
  119. lemma OAI.CoboundaryExpanders.AffineWindow.slice_eq_take_drop line 1388
  120. lemma OAI.CoboundaryExpanders.AffineWindow.slice_pairwise line 1396
  121. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.shared_stage_prefix line 1412
  122. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.same_top_window line 1422
  123. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.window_injective line 1425
  124. theorem OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.window_slice_perm line 1432
  125. lemma OAI.CoboundaryExpanders.AffineWindow.slice_append line 1461
  126. lemma OAI.CoboundaryExpanders.AffineWindow.slice_self line 1471
  127. lemma OAI.CoboundaryExpanders.AffineWindow.slice_full line 1472
  128. def OAI.CoboundaryExpanders.AffineWindow.blocks line 1474
  129. lemma OAI.CoboundaryExpanders.AffineWindow.flatten_blocks line 1476
  130. lemma OAI.CoboundaryExpanders.AffineWindow.blocks_forallâ‚‚ line 1489
  131. theorem OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.fixed_stage_length line 1510
  132. theorem OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.fixed_stage_minimum line 1529
  133. lemma OAI.CoboundaryExpanders.AffineWindow.fin_mono_of_steps line 1541
  134. lemma OAI.CoboundaryExpanders.AffineWindow.slices_sorted_of_descents line 1547
  135. def OAI.CoboundaryExpanders.AffineWindow.cutSet line 1589
  136. lemma OAI.CoboundaryExpanders.AffineWindow.cuts_enumeration line 1591
  137. theorem OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.descent_minimum line 1617
  138. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.increments_card line 1643
  139. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.stage_index_eq line 1649
  140. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.vertex_index_eq line 1662
  141. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.shared_vertex_stage line 1668
  142. def OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.descentCore line 1677
  143. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.full_descentCore line 1681
  144. theorem OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.core_minimum_same_top line 1688
  145. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.rotate_window_of_lt line 1706
  146. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.rotate_descent_iff line 1710
  147. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.scale_descentCore line 1742
  148. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.rotate_descentCore line 1756
  149. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.reroot_descentCore line 1772
  150. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.descentCore_subset line 1786
  151. lemma OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.descentCore_nonempty line 1791
  152. theorem OAI.CoboundaryExpanders.RationalLattices.BoundedChamber.core_minimum line 1801
  153. theorem OAI.CoboundaryExpanders.RationalLattices.FullChamber.core_minimum line 1840
  154. theorem OAI.CoboundaryExpanders.RationalLattices.FullChamber.core_not_previous line 1845
  155. theorem OAI.CoboundaryExpanders.RationalLattices.FullChamber.previous_iff_missing_core line 1851
  156. lemma OAI.CoboundaryExpanders.RationalLattices.FullChamber.core_eq_of_contains line 1864
  157. lemma OAI.CoboundaryExpanders.RationalLattices.FullChamber.core_eq_of_new_intersection line 1879
  158. def OAI.CoboundaryExpanders.RationalLattices.codistanceBlock line 1895
  159. lemma OAI.CoboundaryExpanders.RationalLattices.codistanceBlock_downward line 1897
  160. lemma OAI.CoboundaryExpanders.RationalLattices.codistanceBlock_old_iff line 1902
  161. lemma OAI.CoboundaryExpanders.RationalLattices.codistanceBlock_intersection line 1908
  162. theorem OAI.CoboundaryExpanders.RationalLattices.codistanceStage_successor line 1919
  163. def OAI.CoboundaryExpanders.RationalLattices.codistanceLink line 1933
  164. lemma OAI.CoboundaryExpanders.RationalLattices.codistanceBlock_join line 1935