OAI/MathematicalPhysics/Heisenberg/ClockWitnesses.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Heisenberg.Bernoulli.marked_union_bound line 18
  2. def OAI.Heisenberg.Clocks.weakTimes line 65
  3. lemma OAI.Heisenberg.Clocks.weakTimes_card line 67
  4. def OAI.Heisenberg.Clocks.functionWords line 71
  5. lemma OAI.Heisenberg.Clocks.card_functionWords line 74
  6. def OAI.Heisenberg.Clocks.witnesses line 83
  7. def OAI.Heisenberg.Clocks.witnessMarks line 89
  8. lemma OAI.Heisenberg.Clocks.witnessMarks_card line 93
  9. lemma OAI.Heisenberg.Clocks.witnesses_card line 99
  10. theorem OAI.Heisenberg.Clocks.witness_probability line 111
  11. def OAI.Heisenberg.Clocks.moveList line 149
  12. lemma OAI.Heisenberg.Clocks.moveList_bounds line 154
  13. lemma OAI.Heisenberg.Clocks.moveList_moved line 168
  14. lemma OAI.Heisenberg.Clocks.moveList_pairwise line 180
  15. lemma OAI.Heisenberg.Clocks.moveList_follows line 192
  16. lemma OAI.Heisenberg.Clocks.follows_take line 210
  17. lemma OAI.Heisenberg.Clocks.dist_le_moves line 220
  18. theorem OAI.Heisenberg.Clocks.trajectory_witness line 235