OAI/MathematicalPhysics/Heisenberg/ScheduledResiduals.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Heisenberg.Serial.product_snoc line 17
  2. lemma OAI.Heisenberg.Serial.prefix_product line 26
  3. lemma OAI.Heisenberg.Serial.residualBetween_coin line 35
  4. lemma OAI.Heisenberg.Serial.mul_projection_column line 46
  5. lemma OAI.Heisenberg.Serial.sampledPrefix_exposed line 56
  6. theorem OAI.Heisenberg.Serial.exposedPrefix_localization line 72
  7. theorem OAI.Heisenberg.Schedule.cyclic_localization line 119
  8. def OAI.Heisenberg.SpatialFrame.neighbors line 203
  9. lemma OAI.Heisenberg.SpatialFrame.step_mem_neighbors line 206
  10. lemma OAI.Heisenberg.SpatialFrame.neighbors_card line 220
  11. def OAI.Heisenberg.SpatialFrame.choices line 223
  12. lemma OAI.Heisenberg.SpatialFrame.choices_card line 226
  13. def OAI.Heisenberg.SpatialFrame.next line 263
  14. lemma OAI.Heisenberg.SpatialFrame.edge_site_ne line 267
  15. lemma OAI.Heisenberg.SpatialFrame.swap_step line 275
  16. lemma OAI.Heisenberg.SpatialFrame.swap_move line 288
  17. lemma OAI.Heisenberg.SpatialFrame.same_site_swap line 299