OAI/Probability/Ballisticity/Coupling/SeedStateOrder.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.exists_atom_probability line 12
  2. lemma OAI.DirectionalTransience.seedOrdered_trans line 20
  3. lemma OAI.DirectionalTransience.seedStateStep_ordered line 29
  4. lemma OAI.DirectionalTransience.seedProfileRaw_joint_rows line 90
  5. lemma OAI.DirectionalTransience.seedSplitTest_joint_rows line 101
  6. lemma OAI.DirectionalTransience.seedStateStep_joint_rows line 114
  7. lemma OAI.DirectionalTransience.seedPreserved_joint_rows line 133
  8. def OAI.DirectionalTransience.seedBelow line 154
  9. def OAI.DirectionalTransience.seedAbove line 155
  10. lemma OAI.DirectionalTransience.seedBelow_disjoint_above line 157
  11. lemma OAI.DirectionalTransience.strip_subset_seedAbove line 164
  12. lemma OAI.DirectionalTransience.strip_subset_seedBelow line 171
  13. lemma OAI.DirectionalTransience.seed_fresh_test_bound line 179