OAI/MathematicalPhysics/Heisenberg/ClockInsertions.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Heisenberg.Clocks.mixed_trajectory_probability line 19
  2. theorem OAI.Heisenberg.Bernoulli.marked_union_bound_on line 79
  3. theorem OAI.Heisenberg.Clocks.witness_probability_spatial line 123
  4. theorem OAI.Heisenberg.Clocks.adaptive_trajectory_witness line 160
  5. theorem OAI.Heisenberg.Clocks.adaptive_trajectory_probability line 210
  6. def OAI.Heisenberg.Bernoulli.doubleRates line 244
  7. def OAI.Heisenberg.Bernoulli.original line 246
  8. def OAI.Heisenberg.Bernoulli.fresh line 248
  9. lemma OAI.Heisenberg.Bernoulli.weight_total line 250
  10. lemma OAI.Heisenberg.Bernoulli.double_weight line 256
  11. lemma OAI.Heisenberg.Bernoulli.double_sum line 262
  12. lemma OAI.Heisenberg.Bernoulli.double_partition line 269
  13. lemma OAI.Heisenberg.Bernoulli.original_update_left line 276
  14. lemma OAI.Heisenberg.Bernoulli.original_update_right line 285
  15. theorem OAI.Heisenberg.Bernoulli.double_insertion line 293