OAI/Probability/Ballisticity/Coupling/SeedProfile.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.SeedProfile line 12
  2. instance OAI.DirectionalTransience.seedProfile_measurableSpace line 15
  3. def OAI.DirectionalTransience.SeedProfile.measure line 18
  4. instance OAI.DirectionalTransience.SeedProfile.probability line 19
  5. lemma OAI.DirectionalTransience.SeedProfile.measurable_measure line 21
  6. def OAI.DirectionalTransience.seedHalfProfile line 24
  7. lemma OAI.DirectionalTransience.measurable_seedHalfProfile line 28
  8. def OAI.DirectionalTransience.seedShift line 32
  9. lemma OAI.DirectionalTransience.measurable_seedShift line 36
  10. lemma OAI.DirectionalTransience.seedShift_height line 39
  11. def OAI.DirectionalTransience.seedAdvance line 46
  12. lemma OAI.DirectionalTransience.seedAdvance_mass line 53
  13. lemma OAI.DirectionalTransience.seedAdvance_domination line 58
  14. lemma OAI.DirectionalTransience.seedAdvance_ae line 67
  15. lemma OAI.DirectionalTransience.SeedProfile.measurable_supported line 76
  16. lemma OAI.DirectionalTransience.seedAdvance_joint_rows line 81
  17. lemma OAI.DirectionalTransience.seedAdvance_retained line 94
  18. def OAI.DirectionalTransience.SeedCentral line 118
  19. def OAI.DirectionalTransience.SeedJump line 121
  20. lemma OAI.DirectionalTransience.seedCentral_total_ge line 124
  21. lemma OAI.DirectionalTransience.seedJump_probability line 138
  22. theorem OAI.DirectionalTransience.seed_block_tests line 160