OAI/ModelTheory/Choiceless/Grid.lean

GitHub source file

135 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CPTSeparation.Grid.pairing line 13
  2. theorem OAI.CPTSeparation.Grid.pairing_single line 18
  3. theorem OAI.CPTSeparation.Grid.pairing_boundary line 27
  4. abbrev OAI.CPTSeparation.Grid.FlowSpace line 39
  5. def OAI.CPTSeparation.Grid.flowCycle line 41
  6. theorem OAI.CPTSeparation.Grid.pairing_gradient_flow line 43
  7. theorem OAI.CPTSeparation.Grid.pairing_sub line 47
  8. theorem OAI.CPTSeparation.Grid.exists_representative line 52
  9. theorem OAI.CPTSeparation.Grid.curl_representative line 73
  10. abbrev OAI.CPTSeparation.Grid.BoxGroup line 79
  11. def OAI.CPTSeparation.Grid.faceCodim line 81
  12. def OAI.CPTSeparation.Grid.flowCodim line 85
  13. theorem OAI.CPTSeparation.Grid.curl_count_le_codim line 89
  14. theorem OAI.CPTSeparation.Grid.sparse_annihilator line 105
  15. theorem OAI.CPTSeparation.Grid.subgroup_support_edges line 117
  16. theorem OAI.CPTSeparation.Grid.box_subgroup_index line 168
  17. theorem OAI.CPTSeparation.Grid.orbit_card_eq_power line 172
  18. theorem OAI.CPTSeparation.Grid.small_orbit_support_edges line 179
  19. theorem OAI.CPTSeparation.Grid.sum_subtype_zero line 218
  20. abbrev OAI.CPTSeparation.Grid.EdgeFaces line 225
  21. def OAI.CPTSeparation.Grid.localCycle line 227
  22. abbrev OAI.CPTSeparation.Grid.LocalGroup line 229
  23. def OAI.CPTSeparation.Grid.restrictGroup line 231
  24. theorem OAI.CPTSeparation.Grid.restrictGroup_face line 245
  25. theorem OAI.CPTSeparation.Grid.restrictGroup_flow line 248
  26. def OAI.CPTSeparation.Grid.incident line 251
  27. instance OAI.CPTSeparation.Grid.(instance at line 253) line 253
  28. abbrev OAI.CPTSeparation.Grid.IncidentEdges line 256
  29. def OAI.CPTSeparation.Grid.epsilon line 258
  30. theorem OAI.CPTSeparation.Grid.boundary_eval line 261
  31. theorem OAI.CPTSeparation.Grid.epsilon_eq_zero line 270
  32. theorem OAI.CPTSeparation.Grid.sum_incident line 276
  33. abbrev OAI.CPTSeparation.Grid.LocalStates line 283
  34. def OAI.CPTSeparation.Grid.Compatible line 285
  35. theorem OAI.CPTSeparation.Grid.compatible_iff_extend line 290
  36. def OAI.CPTSeparation.Grid.divergence line 306
  37. structure OAI.CPTSeparation.Grid.Configuration line 309
  38. theorem OAI.CPTSeparation.Grid.Configuration.ext line 314
  39. def OAI.CPTSeparation.Grid.actState line 320
  40. theorem OAI.CPTSeparation.Grid.actState_compatible line 323
  41. theorem OAI.CPTSeparation.Grid.actState_divergence line 329
  42. def OAI.CPTSeparation.Grid.actConfiguration line 354
  43. instance OAI.CPTSeparation.Grid.(instance at line 360) line 360
  44. abbrev OAI.CPTSeparation.Grid.Atom line 375
  45. def OAI.CPTSeparation.Grid.actAtom line 378
  46. instance OAI.CPTSeparation.Grid.(instance at line 382) line 382
  47. example OAI.CPTSeparation.(example at line 399) line 399
  48. instance OAI.CPTSeparation.Input.(instance at line 405) line 405
  49. instance OAI.CPTSeparation.Input.(instance at line 407) line 407
  50. def OAI.CPTSeparation.Input.Iso.edgeEquiv line 413
  51. def OAI.CPTSeparation.Input.Iso.configEquiv line 416
  52. theorem OAI.CPTSeparation.Input.Iso.edgeEquiv_val line 420
  53. theorem OAI.CPTSeparation.Input.Iso.configEquiv_val line 430
  54. theorem OAI.CPTSeparation.Input.Iso.coefficient_eq line 439
  55. theorem OAI.CPTSeparation.Input.Iso.incident_eq line 448
  56. def OAI.CPTSeparation.Input.Iso.symm line 476
  57. theorem OAI.CPTSeparation.Input.Iso.query_map line 483
  58. theorem OAI.CPTSeparation.Input.query_invariant line 513
  59. instance OAI.CPTSeparation.Grid.(instance at line 528) line 528
  60. instance OAI.CPTSeparation.Grid.(instance at line 532) line 532
  61. inductive OAI.CPTSeparation.Grid.AtomRelation line 534
  62. theorem OAI.CPTSeparation.Grid.AtomRelation.map line 548
  63. theorem OAI.CPTSeparation.Grid.AtomRelation.map_iff line 560
  64. def OAI.CPTSeparation.Grid.atomInput line 567
  65. def OAI.CPTSeparation.Grid.actionIso line 570
  66. def OAI.CPTSeparation.Grid.zeroEdgeAtom line 580
  67. theorem OAI.CPTSeparation.Grid.central_fix_zeroEdgeAtom_iff line 582
  68. abbrev OAI.CPTSeparation.Grid.CentralGroup line 595
  69. def OAI.CPTSeparation.Grid.centralHom line 597
  70. instance OAI.CPTSeparation.Grid.(instance at line 602) line 602
  71. theorem OAI.CPTSeparation.Grid.central_smul_atom line 605
  72. theorem OAI.CPTSeparation.Grid.edge_support_tuple line 608
  73. theorem OAI.CPTSeparation.Grid.head_ne_tail line 634
  74. theorem OAI.CPTSeparation.Grid.sum_boundary line 650
  75. def OAI.CPTSeparation.Grid.edgeAxis line 659
  76. theorem OAI.CPTSeparation.Grid.head_injective_on_axis line 664
  77. theorem OAI.CPTSeparation.Grid.tail_injective_on_axis line 670
  78. theorem OAI.CPTSeparation.Grid.exists_head_or_tail line 676
  79. theorem OAI.CPTSeparation.Grid.degree_le_six line 690
  80. instance OAI.CPTSeparation.Grid.(instance at line 717) line 717
  81. instance OAI.CPTSeparation.Grid.(instance at line 719) line 719
  82. theorem OAI.CPTSeparation.Grid.atomInput_rel_true line 721
  83. def OAI.CPTSeparation.Grid.queryEdge line 725
  84. def OAI.CPTSeparation.Grid.queryConfig line 728
  85. theorem OAI.CPTSeparation.Grid.exists_queryEdge line 731
  86. theorem OAI.CPTSeparation.Grid.exists_queryConfig line 738
  87. theorem OAI.CPTSeparation.Grid.queryEdge_eq line 745
  88. theorem OAI.CPTSeparation.Grid.queryConfig_eq line 749
  89. def OAI.CPTSeparation.Grid.queryEdgeEquiv line 754
  90. def OAI.CPTSeparation.Grid.queryConfigEquiv line 760
  91. theorem OAI.CPTSeparation.Grid.rel_vb line 766
  92. theorem OAI.CPTSeparation.Grid.rel_eb line 776
  93. theorem OAI.CPTSeparation.Grid.rel_inc line 786
  94. theorem OAI.CPTSeparation.Grid.rel_z_same line 798
  95. theorem OAI.CPTSeparation.Grid.rel_z_edge line 808
  96. theorem OAI.CPTSeparation.Grid.epsilon_head line 814
  97. theorem OAI.CPTSeparation.Grid.epsilon_tail line 817
  98. theorem OAI.CPTSeparation.Grid.epsilon_sq line 820
  99. def OAI.CPTSeparation.Grid.someConfiguration line 826
  100. def OAI.CPTSeparation.Grid.zeroConfiguration line 839
  101. theorem OAI.CPTSeparation.Grid.sum_queryEdges line 844
  102. theorem OAI.CPTSeparation.Grid.sum_queryConfigs line 849
  103. theorem OAI.CPTSeparation.Grid.zsum_same line 854
  104. theorem OAI.CPTSeparation.Grid.zsum_ne line 860
  105. theorem OAI.CPTSeparation.Grid.coefficient_incident line 870
  106. theorem OAI.CPTSeparation.Grid.query_incident_iff line 890
  107. theorem OAI.CPTSeparation.Grid.sum_block line 907
  108. theorem OAI.CPTSeparation.Grid.block_normalized line 919
  109. theorem OAI.CPTSeparation.Grid.flow_query_eq line 926
  110. theorem OAI.CPTSeparation.Grid.query_implies_total_charge_zero line 935
  111. def OAI.CPTSeparation.Grid.zeroWeight line 962
  112. def OAI.CPTSeparation.Grid.zeroMu line 968
  113. theorem OAI.CPTSeparation.Grid.query_zero_charge line 973
  114. theorem OAI.CPTSeparation.Grid.opposite_answers line 993
  115. def OAI.CPTSeparation.Grid.shiftLocal line 1007
  116. theorem OAI.CPTSeparation.Grid.shiftLocal_face line 1010
  117. theorem OAI.CPTSeparation.Grid.shiftLocal_flow line 1014
  118. theorem OAI.CPTSeparation.Grid.shiftLocal_zero line 1018
  119. theorem OAI.CPTSeparation.Grid.shiftLocal_add line 1021
  120. def OAI.CPTSeparation.Grid.localShiftEquiv line 1025
  121. def OAI.CPTSeparation.Grid.shiftStates line 1031
  122. theorem OAI.CPTSeparation.Grid.shiftStates_compatible line 1034
  123. theorem OAI.CPTSeparation.Grid.shiftStates_divergence line 1039
  124. def OAI.CPTSeparation.Grid.Configuration.shift line 1043
  125. theorem OAI.CPTSeparation.Grid.Configuration.shift_state line 1049
  126. def OAI.CPTSeparation.Grid.configShiftEquiv line 1053
  127. inductive OAI.CPTSeparation.Grid.AtomShift line 1060
  128. theorem OAI.CPTSeparation.Grid.AtomShift.symm line 1066
  129. theorem OAI.CPTSeparation.Grid.AtomShift.functional line 1075
  130. theorem OAI.CPTSeparation.Grid.AtomShift.equal_iff line 1079
  131. theorem OAI.CPTSeparation.Grid.AtomShift.relation line 1085
  132. theorem OAI.CPTSeparation.Grid.AtomShift.relation_iff line 1099
  133. def OAI.CPTSeparation.Grid.blockShiftEquiv line 1104
  134. theorem OAI.CPTSeparation.Grid.blockShiftEquiv_edge line 1109
  135. theorem OAI.CPTSeparation.Grid.blockShiftEquiv_config line 1113