OAI/Probability/Ballisticity/Coupling/SeedOrder.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.ae_at_atom line 12
  2. lemma OAI.DirectionalTransience.atom_of_ae_domination line 17
  3. lemma OAI.DirectionalTransience.seedEndpointRaw_atom_origin line 24
  4. lemma OAI.DirectionalTransience.seedAdvance_atom_origin line 39
  5. lemma OAI.DirectionalTransience.seedHalfProfile_atom_origin line 48
  6. def OAI.DirectionalTransience.SeedOrdered line 57
  7. lemma OAI.DirectionalTransience.seedOrdered_mono line 62
  8. lemma OAI.DirectionalTransience.seedOrdered_central line 66
  9. lemma OAI.DirectionalTransience.signedHeight_cast_coordinate line 80
  10. lemma OAI.DirectionalTransience.seedOrdered_split line 84
  11. lemma OAI.DirectionalTransience.seedOrdered_half_left line 104
  12. lemma OAI.DirectionalTransience.seedOrdered_half_right line 109
  13. abbrev OAI.DirectionalTransience.SeedState line 124
  14. lemma OAI.DirectionalTransience.measurable_seedEval line 126
  15. def OAI.DirectionalTransience.seedCentralInput line 130
  16. def OAI.DirectionalTransience.seedJumpInput line 134
  17. lemma OAI.DirectionalTransience.measurable_seedCentralInput line 137
  18. lemma OAI.DirectionalTransience.measurable_seedJumpInput line 145
  19. def OAI.DirectionalTransience.seedSplitTest line 150
  20. def OAI.DirectionalTransience.seedStateStep line 154
  21. def OAI.DirectionalTransience.SeedStateOrdered line 161
  22. def OAI.DirectionalTransience.SeedStateRetained line 164
  23. def OAI.DirectionalTransience.SeedPreserved line 168
  24. lemma OAI.DirectionalTransience.seedStateStep_count line 173
  25. lemma OAI.DirectionalTransience.seedStateStep_strict line 181
  26. lemma OAI.DirectionalTransience.seedCentralInput_domination line 187
  27. lemma OAI.DirectionalTransience.seedCentralInput_atom line 197
  28. lemma OAI.DirectionalTransience.seedStateStep_retained line 202