OAI/MathematicalPhysics/Heisenberg/SpatialClocks.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Heisenberg.Clocks.mixedCoins line 17
  2. def OAI.Heisenberg.Clocks.mixedSource line 20
  3. lemma OAI.Heisenberg.Clocks.mixedCoins_index line 24
  4. theorem OAI.Heisenberg.Clocks.joint_trajectory_localization line 29
  5. def OAI.Heisenberg.Serial.sampledPrefix line 120
  6. theorem OAI.Heisenberg.Serial.sampledPrefix_event line 127
  7. theorem OAI.Heisenberg.Serial.sampledPrefix_localization line 177
  8. def OAI.Heisenberg.SparseWitness.Tree line 224
  9. def OAI.Heisenberg.SparseWitness.root line 229
  10. def OAI.Heisenberg.SparseWitness.leaves line 233
  11. lemma OAI.Heisenberg.SparseWitness.root_mem line 237
  12. def OAI.Heisenberg.SparseWitness.Admissible line 244
  13. lemma OAI.Heisenberg.SparseWitness.leaves_disjoint line 250
  14. lemma OAI.Heisenberg.SparseWitness.card_leaves line 259
  15. lemma OAI.Heisenberg.SparseWitness.small_diameter_count line 270
  16. lemma OAI.Heisenberg.SparseWitness.ball_count line 324
  17. lemma OAI.Heisenberg.SparseWitness.ball_meets_one_child line 334
  18. def OAI.Heisenberg.SparseWitness.Sparse line 358
  19. theorem OAI.Heisenberg.SparseWitness.admissible_sparse line 361
  20. lemma OAI.Heisenberg.SparseWitness.geometric_scale_growth line 386