OAI/Computability/WitnessedChoice/SupportGrid.lean

GitHub source file

129 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WitnessedChoice.BGS.iterationLoop_total line 13
  2. theorem OAI.WitnessedChoice.BGS.ordinaryIteration_total line 28
  3. theorem OAI.WitnessedChoice.BGS.collect_total line 32
  4. theorem OAI.WitnessedChoice.BGS.Sentence.cpt_boolean line 111
  5. abbrev WitnessedSeparation.Support.Scalar line 123
  6. abbrev WitnessedSeparation.Support.Plane line 125
  7. def WitnessedSeparation.Support.omega line 127
  8. theorem WitnessedSeparation.Support.omega_self line 129
  9. theorem WitnessedSeparation.Support.omega_zero_left line 131
  10. theorem WitnessedSeparation.Support.omega_zero_right line 133
  11. theorem WitnessedSeparation.Support.omega_add_left line 135
  12. theorem WitnessedSeparation.Support.omega_add_right line 138
  13. theorem WitnessedSeparation.Support.omega_neg_left line 141
  14. theorem WitnessedSeparation.Support.omega_neg_right line 144
  15. theorem WitnessedSeparation.Support.omega_swap line 147
  16. theorem WitnessedSeparation.Support.omega_smul_left line 150
  17. theorem WitnessedSeparation.Support.omega_smul_right line 153
  18. def WitnessedSeparation.Support.correction line 158
  19. theorem WitnessedSeparation.Support.correction_self line 161
  20. theorem WitnessedSeparation.Support.correction_zero_left line 164
  21. theorem WitnessedSeparation.Support.correction_zero_right line 167
  22. theorem WitnessedSeparation.Support.correction_add_left line 170
  23. theorem WitnessedSeparation.Support.correction_add_right line 174
  24. theorem WitnessedSeparation.Support.correction_neg_left line 178
  25. theorem WitnessedSeparation.Support.correction_neg_right line 182
  26. theorem WitnessedSeparation.Support.correction_swap line 186
  27. structure WitnessedSeparation.Support.H line 196
  28. instance WitnessedSeparation.Support.H.(instance at line 204) line 204
  29. instance WitnessedSeparation.Support.H.(instance at line 206) line 206
  30. instance WitnessedSeparation.Support.H.(instance at line 209) line 209
  31. theorem WitnessedSeparation.Support.H.one_face line 212
  32. theorem WitnessedSeparation.Support.H.one_flow line 215
  33. theorem WitnessedSeparation.Support.H.mul_face line 217
  34. theorem WitnessedSeparation.Support.H.mul_flow line 219
  35. theorem WitnessedSeparation.Support.H.inv_face line 223
  36. theorem WitnessedSeparation.Support.H.inv_flow line 226
  37. instance WitnessedSeparation.Support.H.(instance at line 228) line 228
  38. def WitnessedSeparation.Support.H.central line 233
  39. theorem WitnessedSeparation.Support.H.central_mul line 235
  40. theorem WitnessedSeparation.Support.H.central_zero line 239
  41. theorem WitnessedSeparation.Support.H.central_neg line 242
  42. theorem WitnessedSeparation.Support.H.central_commute line 245
  43. theorem WitnessedSeparation.Support.H.commutator line 249
  44. def WitnessedSeparation.Support.H.projectedAddSubgroup line 268
  45. def WitnessedSeparation.Support.H.centralAddSubgroup line 278
  46. def WitnessedSeparation.Support.H.projected line 290
  47. def WitnessedSeparation.Support.H.centralPart line 293
  48. theorem WitnessedSeparation.Support.H.mem_projected line 296
  49. theorem WitnessedSeparation.Support.H.mem_centralPart line 299
  50. theorem WitnessedSeparation.Support.H.commutator_mem_centralPart line 302
  51. theorem WitnessedSeparation.Support.H.stabilizer_isotropic line 310
  52. def WitnessedSeparation.Support.H.productEquiv line 317
  53. instance WitnessedSeparation.Support.H.(instance at line 323) line 323
  54. def WitnessedSeparation.Support.H.projectedLift line 326
  55. theorem WitnessedSeparation.Support.H.projectedLift_mem line 329
  56. theorem WitnessedSeparation.Support.H.projectedLift_face line 332
  57. theorem WitnessedSeparation.Support.H.mul_inv_of_face_eq line 335
  58. def WitnessedSeparation.Support.H.subgroupEquiv line 341
  59. theorem WitnessedSeparation.Support.H.subgroup_card line 374
  60. theorem WitnessedSeparation.Support.H.ambient_card line 383
  61. theorem WitnessedSeparation.Support.H.subgroup_index line 391
  62. def WitnessedSeparation.Support.diagonalForm line 406
  63. theorem WitnessedSeparation.Support.diagonalForm_apply line 433
  64. theorem WitnessedSeparation.Support.mem_diagonalForm_ker line 436
  65. def WitnessedSeparation.Support.diagonalKerEquiv line 468
  66. theorem WitnessedSeparation.Support.diagonalForm_finrank_ker line 489
  67. theorem WitnessedSeparation.Support.nonzero_blocks_le_codim line 496
  68. abbrev WitnessedSeparation.Grid.Scalar line 529
  69. abbrev WitnessedSeparation.Grid.Vertex line 531
  70. abbrev WitnessedSeparation.Grid.EdgeX line 533
  71. abbrev WitnessedSeparation.Grid.EdgeY line 535
  72. abbrev WitnessedSeparation.Grid.EdgeZ line 537
  73. abbrev WitnessedSeparation.Grid.Edge line 539
  74. abbrev WitnessedSeparation.Grid.FaceXY line 541
  75. abbrev WitnessedSeparation.Grid.FaceXZ line 543
  76. abbrev WitnessedSeparation.Grid.FaceYZ line 545
  77. abbrev WitnessedSeparation.Grid.Face line 547
  78. def WitnessedSeparation.Grid.ex line 551
  79. def WitnessedSeparation.Grid.ey line 553
  80. def WitnessedSeparation.Grid.ez line 555
  81. def WitnessedSeparation.Grid.tail line 557
  82. def WitnessedSeparation.Grid.head line 562
  83. def WitnessedSeparation.Grid.boundary line 567
  84. theorem WitnessedSeparation.Grid.boundary_single line 572
  85. def WitnessedSeparation.Grid.cycle line 583
  86. theorem WitnessedSeparation.Grid.boundary_cycle line 591
  87. def WitnessedSeparation.Grid.gradient line 597
  88. def WitnessedSeparation.Grid.curl line 599
  89. theorem WitnessedSeparation.Grid.single_mul_sum line 601
  90. theorem WitnessedSeparation.Grid.curl_xy line 608
  91. theorem WitnessedSeparation.Grid.curl_xz line 615
  92. theorem WitnessedSeparation.Grid.curl_yz line 622
  93. theorem WitnessedSeparation.Grid.curl_gradient line 629
  94. theorem WitnessedSeparation.Grid.curl_sub line 634
  95. def WitnessedSeparation.Grid.prefixSum line 638
  96. theorem WitnessedSeparation.Grid.prefix_zero line 641
  97. theorem WitnessedSeparation.Grid.prefix_step line 643
  98. def WitnessedSeparation.Grid.phi1 line 665
  99. def WitnessedSeparation.Grid.residual1 line 668
  100. def WitnessedSeparation.Grid.phi2 line 670
  101. def WitnessedSeparation.Grid.residual2 line 673
  102. def WitnessedSeparation.Grid.phi3 line 676
  103. def WitnessedSeparation.Grid.residual line 679
  104. theorem WitnessedSeparation.Grid.residual1_x line 682
  105. theorem WitnessedSeparation.Grid.residual2_x line 686
  106. theorem WitnessedSeparation.Grid.residual2_y line 691
  107. theorem WitnessedSeparation.Grid.residual_x line 696
  108. theorem WitnessedSeparation.Grid.residual_y line 701
  109. theorem WitnessedSeparation.Grid.residual_z line 706
  110. theorem WitnessedSeparation.Grid.curl_residual line 711
  111. theorem WitnessedSeparation.Grid.residual_as_gradient line 715
  112. theorem WitnessedSeparation.Grid.line_constant line 721
  113. theorem WitnessedSeparation.Grid.residual_y_witness line 730
  114. theorem WitnessedSeparation.Grid.residual_z_witness line 744
  115. def WitnessedSeparation.Grid.nonzeroSet line 765
  116. theorem WitnessedSeparation.Grid.mem_nonzeroSet line 768
  117. theorem WitnessedSeparation.Grid.card_le_product_of_witness line 771
  118. theorem WitnessedSeparation.Grid.card_le_two_products_of_witness line 785
  119. def WitnessedSeparation.Grid.badXY line 805
  120. def WitnessedSeparation.Grid.badXZ line 808
  121. def WitnessedSeparation.Grid.badYZ line 811
  122. def WitnessedSeparation.Grid.badSlice line 814
  123. theorem WitnessedSeparation.Grid.sum_badSlice line 817
  124. theorem WitnessedSeparation.Grid.exists_sparse_slice line 821
  125. theorem WitnessedSeparation.Grid.count_residual_y line 831
  126. theorem WitnessedSeparation.Grid.count_residual_z line 842
  127. theorem WitnessedSeparation.Grid.count_curl line 856
  128. theorem WitnessedSeparation.Grid.count_residual line 861
  129. theorem WitnessedSeparation.Grid.sparse_cochain line 880