OAI/Geometry/Coboundary/ChamberCones.lean

GitHub source file

122 declarations, 0 contain sorry, 0 declared as axioms

Finite pivots, polynomial residue-chamber links, and exactness via finite joins.

  1. def OAI.CoboundaryExpanders.FinitePivots.Leading line 17
  2. def OAI.CoboundaryExpanders.FinitePivots.HasPivot line 20
  3. def OAI.CoboundaryExpanders.FinitePivots.prefSpace line 23
  4. lemma OAI.CoboundaryExpanders.FinitePivots.exists_leading line 29
  5. lemma OAI.CoboundaryExpanders.FinitePivots.leading_single line 44
  6. lemma OAI.CoboundaryExpanders.FinitePivots.eq_top_of_pivots line 50
  7. lemma OAI.CoboundaryExpanders.FinitePivots.disjoint_prefix_iff line 86
  8. theorem OAI.CoboundaryExpanders.FinitePivots.isCompl_prefix_iff line 103
  9. lemma OAI.CoboundaryExpanders.PolynomialVectors.C_smul_vector line 141
  10. def OAI.CoboundaryExpanders.PolynomialVectors.selectedSection line 145
  11. lemma OAI.CoboundaryExpanders.PolynomialVectors.selectedSection_leading line 151
  12. def OAI.CoboundaryExpanders.PolynomialVectors.selectedResidue line 176
  13. lemma OAI.CoboundaryExpanders.PolynomialVectors.selectedSection_polynomial line 180
  14. lemma OAI.CoboundaryExpanders.PolynomialVectors.constant_remainder_mem_diagonal line 184
  15. lemma OAI.CoboundaryExpanders.PolynomialVectors.selectedSection_mem_of_combination line 204
  16. theorem OAI.CoboundaryExpanders.PolynomialVectors.selectedResidue_pivot_iff line 226
  17. theorem OAI.CoboundaryExpanders.PolynomialVectors.selectedResidue_opposed_iff line 261
  18. lemma OAI.CoboundaryExpanders.PolynomialVectors.X_smul_mem_diagonal line 278
  19. lemma OAI.CoboundaryExpanders.PolynomialVectors.selectedSection_mem_span line 292
  20. lemma OAI.CoboundaryExpanders.PolynomialVectors.selectedSection_injective line 299
  21. lemma OAI.CoboundaryExpanders.PolynomialVectors.selectedSection_mem_diagonal_iff line 309
  22. lemma OAI.CoboundaryExpanders.PolynomialVectors.combination_sub_selected_mem line 328
  23. lemma OAI.CoboundaryExpanders.PolynomialVectors.polynomial_smul_section_mod line 346
  24. def OAI.CoboundaryExpanders.PolynomialVectors.liftSelected line 359
  25. lemma OAI.CoboundaryExpanders.PolynomialVectors.diagonal_le_liftSelected line 376
  26. lemma OAI.CoboundaryExpanders.PolynomialVectors.liftSelected_le_span line 381
  27. lemma OAI.CoboundaryExpanders.PolynomialVectors.selectedResidue_liftSelected line 386
  28. lemma OAI.CoboundaryExpanders.PolynomialVectors.liftSelected_selectedResidue line 400
  29. def OAI.CoboundaryExpanders.PolynomialVectors.selectedIntervalEquiv line 416
  30. def OAI.CoboundaryExpanders.FinitePivots.prefEquiv line 444
  31. lemma OAI.CoboundaryExpanders.FinitePivots.prefSpace_finrank line 471
  32. def OAI.CoboundaryExpanders.FinitePivots.prefixFlag line 475
  33. lemma OAI.CoboundaryExpanders.FinitePivots.prefixFlag_opposed_iff line 482
  34. abbrev OAI.CoboundaryExpanders.PolynomialVectors.SelectedInterval line 493
  35. lemma OAI.CoboundaryExpanders.PolynomialVectors.selectedInterval_hasPivots line 497
  36. def OAI.CoboundaryExpanders.PolynomialVectors.PrefixPattern line 504
  37. lemma OAI.CoboundaryExpanders.PolynomialVectors.prefixPattern_iff_good line 509
  38. def OAI.CoboundaryExpanders.PolynomialVectors.prefixPatternComplex line 531
  39. lemma OAI.CoboundaryExpanders.PolynomialVectors.prefixPattern_faces_equiv line 539
  40. theorem OAI.CoboundaryExpanders.PolynomialVectors.uniform_polynomial_residue_exactness line 568
  41. def OAI.CoboundaryExpanders.PolynomialVectors.selectedIncrements line 588
  42. lemma OAI.CoboundaryExpanders.PolynomialVectors.selected_pivot_bounds line 593
  43. lemma OAI.CoboundaryExpanders.PolynomialVectors.selectedIncrements_mono line 607
  44. lemma OAI.CoboundaryExpanders.PolynomialVectors.selectedIncrements_strict line 616
  45. lemma OAI.CoboundaryExpanders.PolynomialVectors.full_chain_card line 639
  46. theorem OAI.CoboundaryExpanders.PolynomialVectors.selected_flag_permutation line 646
  47. lemma OAI.CoboundaryExpanders.PolynomialVectors.selectedIncrements_card line 655
  48. lemma OAI.CoboundaryExpanders.PolynomialVectors.selectedIncrements_prefix_iff line 661
  49. lemma OAI.CoboundaryExpanders.PolynomialVectors.fin_prefix_card line 677
  50. theorem OAI.CoboundaryExpanders.PolynomialVectors.selected_flag_good_iff line 687
  51. lemma OAI.CoboundaryExpanders.PolynomialVectors.full_word_refl_iff line 721
  52. def OAI.CoboundaryExpanders.PolynomialVectors.selectedWord line 759
  53. lemma OAI.CoboundaryExpanders.PolynomialVectors.selectedWord_spec line 764
  54. lemma OAI.CoboundaryExpanders.PolynomialVectors.selectedWord_refl_iff line 772
  55. def OAI.CoboundaryExpanders.PolynomialVectors.pivotWeight line 781
  56. lemma OAI.CoboundaryExpanders.PolynomialVectors.pivotWeight_mod line 784
  57. lemma OAI.CoboundaryExpanders.PolynomialVectors.pivotWeight_strict line 792
  58. lemma OAI.CoboundaryExpanders.PolynomialVectors.pivotWeight_residues line 799
  59. theorem OAI.CoboundaryExpanders.PolynomialVectors.selected_refinement_length line 810
  60. theorem OAI.CoboundaryExpanders.PolynomialVectors.selected_refinement_minimum_iff line 824
  61. theorem OAI.CoboundaryExpanders.PolynomialVectors.prefix_face_complete_refinement line 853
  62. theorem OAI.CoboundaryExpanders.PolynomialVectors.prefix_face_iff_minimum_refinement line 899
  63. lemma OAI.CoboundaryExpanders.PolynomialVectors.diagonalFamily_union line 931
  64. lemma OAI.CoboundaryExpanders.PolynomialVectors.diagonalModule_union line 937
  65. def OAI.CoboundaryExpanders.PolynomialVectors.wordSlice line 942
  66. lemma OAI.CoboundaryExpanders.PolynomialVectors.wordSlice_injective line 944
  67. lemma OAI.CoboundaryExpanders.PolynomialVectors.mem_wordSlice_image line 951
  68. lemma OAI.CoboundaryExpanders.PolynomialVectors.wordPrefix_disjoint_slice line 965
  69. lemma OAI.CoboundaryExpanders.PolynomialVectors.wordPrefix_union_slice line 973
  70. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.blockBasis line 984
  71. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.blockDegree line 986
  72. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.blockBasis_leading line 988
  73. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.block_upper line 993
  74. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.block_lower line 996
  75. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.block_weight line 1001
  76. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.sorted_block_selection line 1007
  77. theorem OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.fixed_stage_minimum_iff_window line 1031
  78. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.word_eq_of_window_eq line 1051
  79. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.stage_degree_eq_of_word_eq line 1057
  80. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.blockIndex line 1062
  81. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.blockIndex_zero line 1064
  82. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.blockIndex_last line 1065
  83. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.blockIndex_left line 1067
  84. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.blockIndex_right line 1070
  85. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.blockFlag line 1074
  86. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.blockFlag_strict line 1084
  87. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.blockFlag_prefix_of_word line 1094
  88. theorem OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.prescribed_refinement line 1117
  89. theorem OAI.CoboundaryExpanders.PolynomialVectors.finite_simultaneous_basis line 1149
  90. theorem OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.face_prescribed_refinement line 1212
  91. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.HasProfile line 1245
  92. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.stage_hasProfile line 1248
  93. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.top_hasProfile line 1249
  94. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.profile_increments line 1251
  95. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.profile_unique line 1258
  96. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.profile_rank_antitone line 1265
  97. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.profile_compare line 1279
  98. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.prefixPattern_iff_profile line 1290
  99. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.profile_stage_le_top line 1347
  100. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.stage_hasProfile_of_window line 1350
  101. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.cuts_interval line 1357
  102. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.fixedStages line 1385
  103. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.IntervalProfile line 1388
  104. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.intervalProfile_interval line 1391
  105. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.intervalProfile_compare_fixed line 1395
  106. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.intervalProfile_not_fixed line 1405
  107. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.rootedMinimumLink line 1419
  108. theorem OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.rootedMinimumLink_iff line 1429
  109. theorem OAI.CoboundaryExpanders.PolynomialVectors.uniform_polynomial_residue_cones line 1506
  110. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.ProfileBetween line 1533
  111. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.profileIntervalComplex line 1535
  112. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.profileInterval_empty line 1540
  113. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.profileInterval_faces_selected line 1549
  114. def OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.profileIntervalCone line 1577
  115. theorem OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.uniform_profileInterval_cones line 1609
  116. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.profileBetween_unique line 1631
  117. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.profileBetween_compare line 1645
  118. theorem OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.rootedMinimumLink_exact_of_join line 1655
  119. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.sum_gaps line 1727
  120. theorem OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.uniform_rootedMinimumLink_exact line 1739
  121. lemma OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.ext_top_stage line 1786
  122. theorem OAI.CoboundaryExpanders.PolynomialVectors.ResidueChamber.exists_unscale line 1795