OAI/Geometry/Coboundary/Lattices.lean

GitHub source file

152 declarations, 0 contain sorry, 0 declared as axioms

Affine and rational lattices, polynomial congruence actions, and lattice-chain geometry.

  1. def OAI.CoboundaryExpanders.AffineLattices.level line 19
  2. lemma OAI.CoboundaryExpanders.AffineLattices.level_zero line 23
  3. lemma OAI.CoboundaryExpanders.AffineLattices.level_succ line 24
  4. lemma OAI.CoboundaryExpanders.AffineLattices.level_antitone line 26
  5. lemma OAI.CoboundaryExpanders.AffineLattices.level_le line 33
  6. def OAI.CoboundaryExpanders.AffineLattices.IsVertex line 36
  7. abbrev OAI.CoboundaryExpanders.AffineLattices.Vertex line 39
  8. instance OAI.CoboundaryExpanders.AffineLattices.(instance at line 41) line 41
  9. instance OAI.CoboundaryExpanders.AffineLattices.(instance at line 43) line 43
  10. lemma OAI.CoboundaryExpanders.AffineLattices.vertex_le line 45
  11. lemma OAI.CoboundaryExpanders.AffineLattices.vertex_normalized line 46
  12. lemma OAI.CoboundaryExpanders.AffineLattices.vertex_bounded line 47
  13. lemma OAI.CoboundaryExpanders.AffineLattices.vertex_shift_le line 48
  14. def OAI.CoboundaryExpanders.AffineLattices.base line 50
  15. def OAI.CoboundaryExpanders.AffineLattices.IsFace line 53
  16. def OAI.CoboundaryExpanders.AffineLattices.complex line 57
  17. lemma OAI.CoboundaryExpanders.AffineLattices.singleton_face line 65
  18. def OAI.CoboundaryExpanders.AffineLattices.ball line 76
  19. lemma OAI.CoboundaryExpanders.AffineLattices.ball_mono line 81
  20. def OAI.CoboundaryExpanders.AffineLattices.raise line 86
  21. lemma OAI.CoboundaryExpanders.AffineLattices.raise_val line 93
  22. lemma OAI.CoboundaryExpanders.AffineLattices.le_raise line 96
  23. lemma OAI.CoboundaryExpanders.AffineLattices.raise_good line 99
  24. lemma OAI.CoboundaryExpanders.AffineLattices.raise_ne line 102
  25. lemma OAI.CoboundaryExpanders.AffineLattices.insert_raise_face line 107
  26. lemma OAI.CoboundaryExpanders.AffineLattices.eliminate_maximal line 151
  27. lemma OAI.CoboundaryExpanders.AffineLattices.push_cycle_down line 214
  28. lemma OAI.CoboundaryExpanders.AffineLattices.push_ball_cycle line 245
  29. lemma OAI.CoboundaryExpanders.AffineLattices.ball_zero_face line 262
  30. theorem OAI.CoboundaryExpanders.AffineLattices.ball_exact line 277
  31. lemma OAI.CoboundaryExpanders.AffineLattices.finite_ball line 296
  32. theorem OAI.CoboundaryExpanders.AffineLattices.complex_exact line 313
  33. abbrev OAI.CoboundaryExpanders.RationalLattices.V line 330
  34. abbrev OAI.CoboundaryExpanders.RationalLattices.LatticeSpace line 331
  35. def OAI.CoboundaryExpanders.RationalLattices.uniformizer line 333
  36. lemma OAI.CoboundaryExpanders.RationalLattices.uniformizer_ne_zero line 334
  37. def OAI.CoboundaryExpanders.RationalLattices.shiftLinear line 337
  38. lemma OAI.CoboundaryExpanders.RationalLattices.shiftLinear_apply line 341
  39. def OAI.CoboundaryExpanders.RationalLattices.shift line 344
  40. def OAI.CoboundaryExpanders.RationalLattices.standard line 347
  41. lemma OAI.CoboundaryExpanders.RationalLattices.mem_standard line 361
  42. lemma OAI.CoboundaryExpanders.RationalLattices.mem_shift line 364
  43. lemma OAI.CoboundaryExpanders.RationalLattices.shift_standard_le line 368
  44. lemma OAI.CoboundaryExpanders.RationalLattices.shift_le_self line 376
  45. lemma OAI.CoboundaryExpanders.RationalLattices.standard_not_le_shift line 385
  46. abbrev OAI.CoboundaryExpanders.RationalLattices.Vertex line 400
  47. abbrev OAI.CoboundaryExpanders.RationalLattices.building line 401
  48. theorem OAI.CoboundaryExpanders.RationalLattices.building_exact line 404
  49. def OAI.CoboundaryExpanders.RationalLattices.positive line 415
  50. lemma OAI.CoboundaryExpanders.RationalLattices.eval_uniformizer line 418
  51. lemma OAI.CoboundaryExpanders.RationalLattices.positive_mul_uniformizer line 423
  52. lemma OAI.CoboundaryExpanders.RationalLattices.positive_injective line 433
  53. lemma OAI.CoboundaryExpanders.RationalLattices.positive_regular_iff line 441
  54. lemma OAI.CoboundaryExpanders.RationalLattices.positive_zero_of_uniformizer_dvd line 476
  55. lemma OAI.CoboundaryExpanders.RationalLattices.positive_C line 492
  56. lemma OAI.CoboundaryExpanders.RationalLattices.positive_X line 494
  57. def OAI.CoboundaryExpanders.Construction.cutPolynomialStabilizer line 502
  58. lemma OAI.CoboundaryExpanders.Construction.polynomialStabilizer_equation line 506
  59. lemma OAI.CoboundaryExpanders.Construction.polynomialStabilizer_upper line 520
  60. lemma OAI.CoboundaryExpanders.Construction.polynomialStabilizer_coefficient line 559
  61. theorem OAI.CoboundaryExpanders.Construction.cutPolynomialStabilizer_eq_localGroup line 584
  62. lemma OAI.CoboundaryExpanders.Construction.mem_polynomialStabilizer_of_equations line 620
  63. theorem OAI.CoboundaryExpanders.Construction.mem_localGroup_iff_cut_equations line 649
  64. def OAI.CoboundaryExpanders.RationalLattices.cutExponent line 666
  65. def OAI.CoboundaryExpanders.RationalLattices.cutLattice line 668
  66. def OAI.CoboundaryExpanders.RationalLattices.positiveMatrix line 682
  67. def OAI.CoboundaryExpanders.RationalLattices.CutRegular line 685
  68. lemma OAI.CoboundaryExpanders.RationalLattices.preserves_cut_iff line 689
  69. lemma OAI.CoboundaryExpanders.RationalLattices.regular_same line 717
  70. lemma OAI.CoboundaryExpanders.RationalLattices.regular_cut_equation line 728
  71. lemma OAI.CoboundaryExpanders.RationalLattices.regular_of_cut_equation line 751
  72. theorem OAI.CoboundaryExpanders.Construction.preserves_cutLattice_iff_localGroup line 784
  73. lemma OAI.CoboundaryExpanders.RationalLattices.cut_le_standard line 807
  74. lemma OAI.CoboundaryExpanders.RationalLattices.shift_standard_le_cut line 812
  75. lemma OAI.CoboundaryExpanders.RationalLattices.uniformizer_mul_ne_one line 821
  76. lemma OAI.CoboundaryExpanders.RationalLattices.single_mem_cut line 827
  77. lemma OAI.CoboundaryExpanders.RationalLattices.cut_not_le_shift line 834
  78. lemma OAI.CoboundaryExpanders.RationalLattices.cut_antitone line 841
  79. lemma OAI.CoboundaryExpanders.RationalLattices.cut_le_cut_iff line 849
  80. lemma OAI.CoboundaryExpanders.RationalLattices.cut_injective line 859
  81. def OAI.CoboundaryExpanders.RationalLattices.cutVertex line 863
  82. lemma OAI.CoboundaryExpanders.RationalLattices.cutVertex_injective line 867
  83. def OAI.CoboundaryExpanders.RationalLattices.baseChamber line 871
  84. lemma OAI.CoboundaryExpanders.RationalLattices.baseChamber_face line 874
  85. lemma OAI.CoboundaryExpanders.RationalLattices.baseChamber_card line 887
  86. def OAI.CoboundaryExpanders.AffineLattices.iterIso line 895
  87. lemma OAI.CoboundaryExpanders.AffineLattices.iterIso_apply line 899
  88. lemma OAI.CoboundaryExpanders.AffineLattices.level_map line 904
  89. lemma OAI.CoboundaryExpanders.AffineLattices.level_add line 909
  90. lemma OAI.CoboundaryExpanders.AffineLattices.level_mono line 914
  91. lemma OAI.CoboundaryExpanders.AffineLattices.level_injective line 917
  92. lemma OAI.CoboundaryExpanders.AffineLattices.level_reflect_le line 923
  93. lemma OAI.CoboundaryExpanders.AffineLattices.exists_normalized line 926
  94. lemma OAI.CoboundaryExpanders.AffineLattices.level_vertex_le line 947
  95. lemma OAI.CoboundaryExpanders.AffineLattices.normalized_unique line 950
  96. def OAI.CoboundaryExpanders.AffineLattices.Homothetic line 976
  97. lemma OAI.CoboundaryExpanders.AffineLattices.homothetic_refl line 978
  98. lemma OAI.CoboundaryExpanders.AffineLattices.homothetic_symm line 979
  99. lemma OAI.CoboundaryExpanders.AffineLattices.homothetic_trans line 981
  100. lemma OAI.CoboundaryExpanders.AffineLattices.homothetic_normalized_iff line 986
  101. lemma OAI.CoboundaryExpanders.AffineLattices.level_swap line 999
  102. lemma OAI.CoboundaryExpanders.AffineLattices.normalized_level_le line 1002
  103. def OAI.CoboundaryExpanders.AffineLattices.Compatible line 1016
  104. lemma OAI.CoboundaryExpanders.AffineLattices.compatible_symm line 1019
  105. lemma OAI.CoboundaryExpanders.AffineLattices.compatible_homothetic_left line 1023
  106. lemma OAI.CoboundaryExpanders.AffineLattices.compatible_homothetic line 1035
  107. lemma OAI.CoboundaryExpanders.AffineLattices.compatible_normalized_iff line 1040
  108. lemma OAI.CoboundaryExpanders.AffineLattices.isFace_iff_compatible line 1065
  109. lemma OAI.CoboundaryExpanders.AffineLattices.map_level line 1080
  110. lemma OAI.CoboundaryExpanders.AffineLattices.homothetic_map line 1086
  111. lemma OAI.CoboundaryExpanders.AffineLattices.homothetic_map_iff line 1091
  112. lemma OAI.CoboundaryExpanders.AffineLattices.compatible_map line 1099
  113. lemma OAI.CoboundaryExpanders.AffineLattices.exists_mapVertex line 1106
  114. def OAI.CoboundaryExpanders.AffineLattices.mapVertex line 1132
  115. lemma OAI.CoboundaryExpanders.AffineLattices.mapVertex_homothetic line 1138
  116. lemma OAI.CoboundaryExpanders.AffineLattices.mapVertex_injective line 1144
  117. lemma OAI.CoboundaryExpanders.AffineLattices.mapVertex_face line 1155
  118. def OAI.CoboundaryExpanders.RationalLattices.polynomialToStandard line 1175
  119. lemma OAI.CoboundaryExpanders.RationalLattices.polynomialToStandard_bijective line 1180
  120. def OAI.CoboundaryExpanders.RationalLattices.standardEquiv line 1191
  121. def OAI.CoboundaryExpanders.RationalLattices.standardBasis line 1194
  122. lemma OAI.CoboundaryExpanders.RationalLattices.shiftLinear_eq_smul line 1197
  123. lemma OAI.CoboundaryExpanders.RationalLattices.smul_pow_mem_level line 1201
  124. def OAI.CoboundaryExpanders.RationalLattices.boundedBasis line 1210
  125. lemma OAI.CoboundaryExpanders.RationalLattices.boundedBasis_rank line 1213
  126. def OAI.CoboundaryExpanders.RationalLattices.latticeBasis line 1242
  127. def OAI.CoboundaryExpanders.RationalLattices.constantVector line 1252
  128. def OAI.CoboundaryExpanders.RationalLattices.residueMap line 1257
  129. lemma OAI.CoboundaryExpanders.RationalLattices.residueMap_apply line 1260
  130. lemma OAI.CoboundaryExpanders.RationalLattices.residueMap_surjective line 1263
  131. lemma OAI.CoboundaryExpanders.RationalLattices.residueMap_smul_polynomial line 1269
  132. lemma OAI.CoboundaryExpanders.RationalLattices.residueMap_eq_zero_iff line 1276
  133. def OAI.CoboundaryExpanders.RationalLattices.residueKernel line 1305
  134. lemma OAI.CoboundaryExpanders.RationalLattices.residueKernel_eq line 1308
  135. def OAI.CoboundaryExpanders.RationalLattices.residueEquiv line 1312
  136. lemma OAI.CoboundaryExpanders.RationalLattices.residue_finrank line 1317
  137. lemma OAI.CoboundaryExpanders.RationalLattices.mem_level line 1328
  138. def OAI.CoboundaryExpanders.RationalLattices.positiveLinear line 1342
  139. lemma OAI.CoboundaryExpanders.RationalLattices.positiveLinear_apply line 1346
  140. lemma OAI.CoboundaryExpanders.RationalLattices.positiveLinear_mul line 1349
  141. lemma OAI.CoboundaryExpanders.RationalLattices.positiveLinear_one line 1353
  142. lemma OAI.CoboundaryExpanders.RationalLattices.positiveLinear_inv line 1357
  143. lemma OAI.CoboundaryExpanders.RationalLattices.positiveLinear_shift line 1364
  144. def OAI.CoboundaryExpanders.RationalLattices.positiveAction line 1368
  145. lemma OAI.CoboundaryExpanders.RationalLattices.mem_positiveAction line 1371
  146. lemma OAI.CoboundaryExpanders.RationalLattices.positiveAction_inv line 1375
  147. lemma OAI.CoboundaryExpanders.RationalLattices.positiveAction_shift line 1382
  148. lemma OAI.CoboundaryExpanders.RationalLattices.positiveAction_upper line 1397
  149. lemma OAI.CoboundaryExpanders.RationalLattices.positiveAction_lower line 1423
  150. def OAI.CoboundaryExpanders.RationalLattices.actVertex line 1432
  151. lemma OAI.CoboundaryExpanders.RationalLattices.actVertex_homothetic line 1437
  152. lemma OAI.CoboundaryExpanders.RationalLattices.actVertex_face line 1441