OAI/Computability/WitnessedChoice/GridAction.lean

GitHub source file

123 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WitnessedSeparation.Grid.pairing line 11
  2. theorem OAI.WitnessedSeparation.Grid.pairing_single line 16
  3. theorem OAI.WitnessedSeparation.Grid.pairing_boundary line 25
  4. abbrev OAI.WitnessedSeparation.Grid.FlowSpace line 37
  5. def OAI.WitnessedSeparation.Grid.flowCycle line 39
  6. theorem OAI.WitnessedSeparation.Grid.pairing_gradient_flow line 41
  7. theorem OAI.WitnessedSeparation.Grid.pairing_sub line 45
  8. theorem OAI.WitnessedSeparation.Grid.exists_representative line 50
  9. theorem OAI.WitnessedSeparation.Grid.curl_representative line 71
  10. abbrev OAI.WitnessedSeparation.Grid.BoxGroup line 77
  11. def OAI.WitnessedSeparation.Grid.faceCodim line 79
  12. def OAI.WitnessedSeparation.Grid.flowCodim line 83
  13. theorem OAI.WitnessedSeparation.Grid.curl_count_le_codim line 87
  14. theorem OAI.WitnessedSeparation.Grid.sparse_annihilator line 103
  15. theorem OAI.WitnessedSeparation.Grid.subgroup_support_edges line 115
  16. theorem OAI.WitnessedSeparation.Grid.box_subgroup_index line 166
  17. theorem OAI.WitnessedSeparation.Grid.orbit_card_eq_power line 170
  18. theorem OAI.WitnessedSeparation.Grid.small_orbit_support_edges line 177
  19. theorem OAI.WitnessedSeparation.Grid.sum_subtype_zero line 218
  20. abbrev OAI.WitnessedSeparation.Grid.EdgeFaces line 225
  21. def OAI.WitnessedSeparation.Grid.localCycle line 227
  22. abbrev OAI.WitnessedSeparation.Grid.LocalGroup line 229
  23. def OAI.WitnessedSeparation.Grid.restrictGroup line 231
  24. theorem OAI.WitnessedSeparation.Grid.restrictGroup_face line 245
  25. theorem OAI.WitnessedSeparation.Grid.restrictGroup_flow line 248
  26. def OAI.WitnessedSeparation.Grid.incident line 251
  27. instance OAI.WitnessedSeparation.Grid.(instance at line 253) line 253
  28. abbrev OAI.WitnessedSeparation.Grid.IncidentEdges line 256
  29. def OAI.WitnessedSeparation.Grid.epsilon line 258
  30. theorem OAI.WitnessedSeparation.Grid.boundary_eval line 261
  31. theorem OAI.WitnessedSeparation.Grid.epsilon_eq_zero line 270
  32. theorem OAI.WitnessedSeparation.Grid.sum_incident line 276
  33. abbrev OAI.WitnessedSeparation.Grid.LocalStates line 283
  34. def OAI.WitnessedSeparation.Grid.Compatible line 285
  35. theorem OAI.WitnessedSeparation.Grid.compatible_iff_extend line 290
  36. def OAI.WitnessedSeparation.Grid.divergence line 306
  37. structure OAI.WitnessedSeparation.Grid.Configuration line 309
  38. theorem OAI.WitnessedSeparation.Grid.Configuration.ext line 314
  39. def OAI.WitnessedSeparation.Grid.actState line 320
  40. theorem OAI.WitnessedSeparation.Grid.actState_compatible line 323
  41. theorem OAI.WitnessedSeparation.Grid.actState_divergence line 329
  42. def OAI.WitnessedSeparation.Grid.actConfiguration line 354
  43. instance OAI.WitnessedSeparation.Grid.(instance at line 360) line 360
  44. abbrev OAI.WitnessedSeparation.Grid.Atom line 375
  45. def OAI.WitnessedSeparation.Grid.actAtom line 378
  46. instance OAI.WitnessedSeparation.Grid.(instance at line 382) line 382
  47. instance OAI.WitnessedSeparation.Grid.(instance at line 403) line 403
  48. instance OAI.WitnessedSeparation.Grid.(instance at line 407) line 407
  49. inductive OAI.WitnessedSeparation.Grid.AtomRelation line 409
  50. theorem OAI.WitnessedSeparation.Grid.AtomRelation.map line 423
  51. theorem OAI.WitnessedSeparation.Grid.AtomRelation.map_iff line 435
  52. def OAI.WitnessedSeparation.Grid.atomInput line 442
  53. theorem OAI.WitnessedSeparation.Grid.head_ne_tail line 451
  54. theorem OAI.WitnessedSeparation.Grid.sum_boundary line 467
  55. def OAI.WitnessedSeparation.Grid.edgeAxis line 476
  56. theorem OAI.WitnessedSeparation.Grid.head_injective_on_axis line 481
  57. theorem OAI.WitnessedSeparation.Grid.tail_injective_on_axis line 487
  58. theorem OAI.WitnessedSeparation.Grid.exists_head_or_tail line 493
  59. theorem OAI.WitnessedSeparation.Grid.degree_le_six line 507
  60. instance OAI.WitnessedSeparation.Grid.(instance at line 530) line 530
  61. instance OAI.WitnessedSeparation.Grid.(instance at line 532) line 532
  62. abbrev OAI.WitnessedSeparation.Input.Edge line 543
  63. abbrev OAI.WitnessedSeparation.Input.Config line 545
  64. instance OAI.WitnessedSeparation.Input.(instance at line 547) line 547
  65. instance OAI.WitnessedSeparation.Input.(instance at line 549) line 549
  66. instance OAI.WitnessedSeparation.Input.(instance at line 551) line 551
  67. instance OAI.WitnessedSeparation.Input.(instance at line 553) line 553
  68. def OAI.WitnessedSeparation.Input.coefficient line 555
  69. def OAI.WitnessedSeparation.Input.incident line 560
  70. def OAI.WitnessedSeparation.Input.normalized line 564
  71. def OAI.WitnessedSeparation.Input.consistent line 567
  72. def OAI.WitnessedSeparation.Input.query line 571
  73. structure OAI.WitnessedSeparation.Input.Iso line 574
  74. def OAI.WitnessedSeparation.Input.Iso.edgeEquiv line 581
  75. def OAI.WitnessedSeparation.Input.Iso.configEquiv line 584
  76. theorem OAI.WitnessedSeparation.Input.Iso.edgeEquiv_val line 588
  77. theorem OAI.WitnessedSeparation.Input.Iso.configEquiv_val line 591
  78. theorem OAI.WitnessedSeparation.Input.Iso.coefficient_eq line 593
  79. theorem OAI.WitnessedSeparation.Input.Iso.incident_eq line 602
  80. def OAI.WitnessedSeparation.Input.Iso.symm line 623
  81. theorem OAI.WitnessedSeparation.Input.Iso.query_map line 630
  82. theorem OAI.WitnessedSeparation.Input.query_invariant line 660
  83. def OAI.WitnessedSeparation.Grid.actionIso line 675
  84. def OAI.WitnessedSeparation.Grid.zeroEdgeAtom line 685
  85. theorem OAI.WitnessedSeparation.Grid.central_fix_zeroEdgeAtom_iff line 687
  86. abbrev OAI.WitnessedSeparation.Grid.CentralGroup line 700
  87. def OAI.WitnessedSeparation.Grid.centralHom line 702
  88. instance OAI.WitnessedSeparation.Grid.(instance at line 707) line 707
  89. theorem OAI.WitnessedSeparation.Grid.central_smul_atom line 710
  90. theorem OAI.WitnessedSeparation.Grid.edge_support_tuple line 713
  91. theorem OAI.WitnessedSeparation.Grid.atomInput_rel_true line 745
  92. def OAI.WitnessedSeparation.Grid.queryEdge line 749
  93. def OAI.WitnessedSeparation.Grid.queryConfig line 752
  94. theorem OAI.WitnessedSeparation.Grid.exists_queryEdge line 755
  95. theorem OAI.WitnessedSeparation.Grid.exists_queryConfig line 762
  96. theorem OAI.WitnessedSeparation.Grid.queryEdge_eq line 769
  97. theorem OAI.WitnessedSeparation.Grid.queryConfig_eq line 773
  98. def OAI.WitnessedSeparation.Grid.queryEdgeEquiv line 778
  99. def OAI.WitnessedSeparation.Grid.queryConfigEquiv line 784
  100. theorem OAI.WitnessedSeparation.Grid.rel_vb line 790
  101. theorem OAI.WitnessedSeparation.Grid.rel_eb line 800
  102. theorem OAI.WitnessedSeparation.Grid.rel_inc line 810
  103. theorem OAI.WitnessedSeparation.Grid.rel_z_same line 822
  104. theorem OAI.WitnessedSeparation.Grid.rel_z_edge line 832
  105. theorem OAI.WitnessedSeparation.Grid.epsilon_head line 838
  106. theorem OAI.WitnessedSeparation.Grid.epsilon_tail line 841
  107. theorem OAI.WitnessedSeparation.Grid.epsilon_sq line 844
  108. def OAI.WitnessedSeparation.Grid.someConfiguration line 850
  109. def OAI.WitnessedSeparation.Grid.zeroConfiguration line 863
  110. theorem OAI.WitnessedSeparation.Grid.sum_queryEdges line 868
  111. theorem OAI.WitnessedSeparation.Grid.sum_queryConfigs line 873
  112. theorem OAI.WitnessedSeparation.Grid.zsum_same line 878
  113. theorem OAI.WitnessedSeparation.Grid.zsum_ne line 884
  114. theorem OAI.WitnessedSeparation.Grid.coefficient_incident line 894
  115. theorem OAI.WitnessedSeparation.Grid.query_incident_iff line 914
  116. theorem OAI.WitnessedSeparation.Grid.sum_block line 931
  117. theorem OAI.WitnessedSeparation.Grid.block_normalized line 943
  118. theorem OAI.WitnessedSeparation.Grid.flow_query_eq line 950
  119. theorem OAI.WitnessedSeparation.Grid.query_implies_total_charge_zero line 959
  120. def OAI.WitnessedSeparation.Grid.zeroWeight line 986
  121. def OAI.WitnessedSeparation.Grid.zeroMu line 992
  122. theorem OAI.WitnessedSeparation.Grid.query_zero_charge line 997
  123. theorem OAI.WitnessedSeparation.Grid.opposite_answers line 1017