OAI/Geometry/Coboundary/Windows.lean

GitHub source file

133 declarations, 0 contain sorry, 0 declared as axioms

Affine windows, residue chambers, lattice flags, and chamber parametrizations.

  1. structure OAI.CoboundaryExpanders.AffineWindow.Window line 17
  2. def OAI.CoboundaryExpanders.AffineWindow.pairCost line 21
  3. def OAI.CoboundaryExpanders.AffineWindow.length line 23
  4. lemma OAI.CoboundaryExpanders.AffineWindow.sub_not_dvd line 26
  5. lemma OAI.CoboundaryExpanders.AffineWindow.div_neg_nondiv line 32
  6. lemma OAI.CoboundaryExpanders.AffineWindow.pairCost_reverse line 45
  7. lemma OAI.CoboundaryExpanders.AffineWindow.pairCost_rotate line 60
  8. lemma OAI.CoboundaryExpanders.AffineWindow.pairCost_zero_of_bounds line 72
  9. lemma OAI.CoboundaryExpanders.AffineWindow.length_zero_of_bounds line 78
  10. lemma OAI.CoboundaryExpanders.AffineWindow.pairCost_eq_zero_iff line 86
  11. lemma OAI.CoboundaryExpanders.AffineWindow.pairCost_shift line 92
  12. def OAI.CoboundaryExpanders.AffineWindow.inversion line 97
  13. lemma OAI.CoboundaryExpanders.AffineWindow.inversion_append line 101
  14. lemma OAI.CoboundaryExpanders.AffineWindow.inversion_adjacent line 109
  15. lemma OAI.CoboundaryExpanders.AffineWindow.inversion_adjacent_increase line 119
  16. lemma OAI.CoboundaryExpanders.AffineWindow.inversion_rotate line 126
  17. lemma OAI.CoboundaryExpanders.AffineWindow.inversion_shift line 139
  18. lemma OAI.CoboundaryExpanders.AffineWindow.inversion_zero_iff line 148
  19. lemma OAI.CoboundaryExpanders.AffineWindow.consecutive_of_bounds line 165
  20. def OAI.CoboundaryExpanders.AffineWindow.pairs line 189
  21. def OAI.CoboundaryExpanders.AffineWindow.sortedCost line 193
  22. def OAI.CoboundaryExpanders.AffineWindow.disorder line 194
  23. lemma OAI.CoboundaryExpanders.AffineWindow.pairs_perm line 196
  24. lemma OAI.CoboundaryExpanders.AffineWindow.sortedCost_comm line 206
  25. lemma OAI.CoboundaryExpanders.AffineWindow.pairCost_decompose line 209
  26. lemma OAI.CoboundaryExpanders.AffineWindow.inversion_decompose line 218
  27. lemma OAI.CoboundaryExpanders.AffineWindow.disorder_zero_iff line 233
  28. theorem OAI.CoboundaryExpanders.AffineWindow.inversion_minimal_perm line 251
  29. lemma OAI.CoboundaryExpanders.AffineWindow.inversion_minimal_unique line 260
  30. lemma OAI.CoboundaryExpanders.AffineWindow.inversion_permute_middle line 270
  31. lemma OAI.CoboundaryExpanders.AffineWindow.inversion_sorted_middle line 284
  32. def OAI.CoboundaryExpanders.AffineWindow.periodicEnd line 297
  33. lemma OAI.CoboundaryExpanders.AffineWindow.periodicEnd_castSucc line 300
  34. lemma OAI.CoboundaryExpanders.AffineWindow.periodicEnd_last line 304
  35. lemma OAI.CoboundaryExpanders.AffineWindow.periodicEnd_zero line 308
  36. def OAI.CoboundaryExpanders.AffineWindow.descents line 313
  37. lemma OAI.CoboundaryExpanders.AffineWindow.periodicEnd_mono_iff line 316
  38. lemma OAI.CoboundaryExpanders.AffineWindow.last_ne_periodic_start line 322
  39. lemma OAI.CoboundaryExpanders.AffineWindow.inversion_zero_of_no_descents line 333
  40. theorem OAI.CoboundaryExpanders.AffineWindow.descents_nonempty line 352
  41. theorem OAI.CoboundaryExpanders.AffineWindow.descents_ne_univ line 359
  42. lemma OAI.CoboundaryExpanders.AffineWindow.inversion_zero_no_descents line 375
  43. lemma OAI.CoboundaryExpanders.AffineWindow.window_entry_consecutive line 402
  44. lemma OAI.CoboundaryExpanders.AffineWindow.same_residue_short_interval line 421
  45. lemma OAI.CoboundaryExpanders.AffineWindow.cyclic_cut_exponents line 433
  46. theorem OAI.CoboundaryExpanders.AffineWindow.zero_window_cut_flag line 457
  47. structure OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber line 489
  48. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.word line 501
  49. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.word_spec line 504
  50. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.increments line 510
  51. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.stage_degree line 535
  52. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.terminal line 549
  53. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.window line 556
  54. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.length line 559
  55. theorem OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.zero_flag line 561
  56. lemma OAI.CoboundaryExpanders.RationalLattices.exponent_cut line 577
  57. lemma OAI.CoboundaryExpanders.RationalLattices.shift_exponent line 596
  58. lemma OAI.CoboundaryExpanders.RationalLattices.level_exponent line 610
  59. lemma OAI.CoboundaryExpanders.RationalLattices.exponent_cut_level line 618
  60. theorem OAI.CoboundaryExpanders.RationalLattices.zero_pivots_common_orbit line 625
  61. lemma OAI.CoboundaryExpanders.RationalLattices.polynomialLattice_injective line 656
  62. lemma OAI.CoboundaryExpanders.RationalLattices.polynomialLattice_strict line 662
  63. lemma OAI.CoboundaryExpanders.RationalLattices.polynomialLattice_power_map line 668
  64. structure OAI.CoboundaryExpanders.RationalLattices.FullChamber line 683
  65. def OAI.CoboundaryExpanders.RationalLattices.FullChamber.topIndex line 691
  66. def OAI.CoboundaryExpanders.RationalLattices.FullChamber.stage line 693
  67. lemma OAI.CoboundaryExpanders.RationalLattices.FullChamber.stage_castSucc line 697
  68. lemma OAI.CoboundaryExpanders.RationalLattices.FullChamber.stage_last line 700
  69. lemma OAI.CoboundaryExpanders.RationalLattices.FullChamber.hasStage line 706
  70. lemma OAI.CoboundaryExpanders.RationalLattices.FullChamber.lower_stage line 712
  71. lemma OAI.CoboundaryExpanders.RationalLattices.FullChamber.stage_strict line 718
  72. def OAI.CoboundaryExpanders.RationalLattices.FullChamber.polynomialChamber line 734
  73. def OAI.CoboundaryExpanders.RationalLattices.FullChamber.length line 747
  74. lemma OAI.CoboundaryExpanders.RationalLattices.FullChamber.zero_pivots line 749
  75. theorem OAI.CoboundaryExpanders.RationalLattices.FullChamber.zero_common_orbit line 757
  76. lemma OAI.CoboundaryExpanders.RationalLattices.polynomialEmbedding_injective line 779
  77. lemma OAI.CoboundaryExpanders.RationalLattices.powerShift_map_embedding line 784
  78. lemma OAI.CoboundaryExpanders.RationalLattices.reciprocal_reflect line 800
  79. def OAI.CoboundaryExpanders.RationalLattices.reflectedMatrix line 806
  80. lemma OAI.CoboundaryExpanders.RationalLattices.reflectedMatrix_embedding line 809
  81. lemma OAI.CoboundaryExpanders.RationalLattices.reflectedLattice_map_embedding line 826
  82. lemma OAI.CoboundaryExpanders.RationalLattices.matrix_degree_bound line 843
  83. theorem OAI.CoboundaryExpanders.RationalLattices.homothetic_action_pivots line 851
  84. lemma OAI.CoboundaryExpanders.RationalLattices.diagonalExponents_cut line 887
  85. lemma OAI.CoboundaryExpanders.RationalLattices.orbit_cut_pivots line 914
  86. def OAI.CoboundaryExpanders.AffineWindow.cutDegree line 939
  87. lemma OAI.CoboundaryExpanders.AffineWindow.sum_indicator_lt line 941
  88. lemma OAI.CoboundaryExpanders.AffineWindow.sum_cut_shift line 946
  89. lemma OAI.CoboundaryExpanders.AffineWindow.sum_cutDegree line 951
  90. lemma OAI.CoboundaryExpanders.AffineWindow.cutDegree_succ line 956
  91. lemma OAI.CoboundaryExpanders.AffineWindow.cut_shift_identify line 978
  92. lemma OAI.CoboundaryExpanders.AffineWindow.flag_height line 986
  93. theorem OAI.CoboundaryExpanders.AffineWindow.inversion_zero_of_cut_flag line 996
  94. def OAI.CoboundaryExpanders.RationalLattices.OpposedVertex line 1042
  95. lemma OAI.CoboundaryExpanders.RationalLattices.opposed_pivots line 1047
  96. theorem OAI.CoboundaryExpanders.RationalLattices.opposed_flag_common_orbit line 1053
  97. theorem OAI.CoboundaryExpanders.RationalLattices.FullChamber.zero_of_cut_pivots line 1068
  98. theorem OAI.CoboundaryExpanders.RationalLattices.FullChamber.zero_iff_vertexwise_opposed line 1100
  99. lemma OAI.CoboundaryExpanders.finite_chain_enumeration line 1117
  100. theorem OAI.CoboundaryExpanders.RationalLattices.common_orbit_iff_induced line 1148
  101. abbrev OAI.CoboundaryExpanders.RationalLattices.ResidueInterval line 1197
  102. def OAI.CoboundaryExpanders.RationalLattices.liftResidue line 1199
  103. lemma OAI.CoboundaryExpanders.RationalLattices.liftResidue_le line 1218
  104. lemma OAI.CoboundaryExpanders.RationalLattices.shift_le_liftResidue line 1221
  105. lemma OAI.CoboundaryExpanders.RationalLattices.mem_liftResidue line 1229
  106. def OAI.CoboundaryExpanders.RationalLattices.intervalSubspace line 1235
  107. lemma OAI.CoboundaryExpanders.RationalLattices.mem_intervalSubspace line 1238
  108. lemma OAI.CoboundaryExpanders.RationalLattices.lift_intervalSubspace line 1241
  109. lemma OAI.CoboundaryExpanders.RationalLattices.intervalSubspace_lift line 1255
  110. def OAI.CoboundaryExpanders.RationalLattices.residueIntervalIso line 1266
  111. lemma OAI.CoboundaryExpanders.RationalLattices.interval_exists_normalized line 1292
  112. def OAI.CoboundaryExpanders.RationalLattices.intervalNormalize line 1301
  113. lemma OAI.CoboundaryExpanders.RationalLattices.intervalNormalize_homothetic line 1304
  114. lemma OAI.CoboundaryExpanders.RationalLattices.intervalNormalize_vertex line 1308
  115. lemma OAI.CoboundaryExpanders.RationalLattices.intervalNormalize_injOn line 1314
  116. lemma OAI.CoboundaryExpanders.RationalLattices.intervalNormalize_face line 1329
  117. lemma OAI.CoboundaryExpanders.covBy_finrank line 1351
  118. theorem OAI.CoboundaryExpanders.ambient_chain_complete_flag line 1361
  119. theorem OAI.CoboundaryExpanders.RationalLattices.ambient_face_extend line 1419
  120. lemma OAI.CoboundaryExpanders.finite_chain_enumeration_of_card line 1513
  121. def OAI.CoboundaryExpanders.RationalLattices.FullChamber.face line 1542
  122. lemma OAI.CoboundaryExpanders.RationalLattices.FullChamber.mem_face line 1543
  123. lemma OAI.CoboundaryExpanders.RationalLattices.FullChamber.vertex_injective line 1546
  124. lemma OAI.CoboundaryExpanders.RationalLattices.FullChamber.card_face line 1549
  125. lemma OAI.CoboundaryExpanders.RationalLattices.FullChamber.face_mem line 1553
  126. theorem OAI.CoboundaryExpanders.RationalLattices.ambient_face_in_chamber line 1568
  127. def OAI.CoboundaryExpanders.RationalLattices.codistanceStage line 1583
  128. lemma OAI.CoboundaryExpanders.RationalLattices.codistanceStage_mono line 1586
  129. lemma OAI.CoboundaryExpanders.RationalLattices.codistanceStage_downward line 1590
  130. lemma OAI.CoboundaryExpanders.RationalLattices.codistanceStage_exhaust line 1596
  131. lemma OAI.CoboundaryExpanders.RationalLattices.actVertex_injective line 1613
  132. lemma OAI.CoboundaryExpanders.RationalLattices.fullChamber_of_face_card line 1619
  133. theorem OAI.CoboundaryExpanders.RationalLattices.codistanceStage_zero line 1629