OAI/Probability/Ballisticity/Estimates/RecordIndexTime.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.common_record_gap_le_max line 12
  2. lemma OAI.DirectionalTransience.conditioned_record_prefix_true line 25
  3. def OAI.DirectionalTransience.recordIndexTime line 47
  4. lemma OAI.DirectionalTransience.recordIndexTime_eq line 51
  5. lemma OAI.DirectionalTransience.measurable_recordIndexTime line 59
  6. def OAI.DirectionalTransience.recordIndexPosition line 99
  7. lemma OAI.DirectionalTransience.measurable_recordIndexPosition line 102
  8. lemma OAI.DirectionalTransience.conditioned_recordIndexPrefix_exists line 108
  9. lemma OAI.DirectionalTransience.conditioned_recordIndexTime_spec line 116
  10. lemma OAI.DirectionalTransience.independentConditionedPairLaw_eq_restrict line 123
  11. lemma OAI.DirectionalTransience.independentConditionedPairLaw_normalization line 132
  12. lemma OAI.DirectionalTransience.independentConditionedPairLaw_le_raw line 141
  13. lemma OAI.DirectionalTransience.independent_conditioned_record_prefix_lower line 149
  14. def OAI.DirectionalTransience.PairRecordDeviation line 171
  15. def OAI.DirectionalTransience.FirstPairRecordDeviation line 178
  16. lemma OAI.DirectionalTransience.measurableSet_pairRecordDeviation line 183
  17. lemma OAI.DirectionalTransience.measurableSet_firstPairRecordDeviation line 200
  18. lemma OAI.DirectionalTransience.pairRecordDeviation_prefix line 208
  19. lemma OAI.DirectionalTransience.firstPairRecordDeviation_prefix line 216
  20. lemma OAI.DirectionalTransience.recordIndexPrefix_time_lt_iff line 227
  21. lemma OAI.DirectionalTransience.pairRecordDeviation_time_order line 240
  22. lemma OAI.DirectionalTransience.firstPairRecordDeviation_disjoint line 254
  23. lemma OAI.DirectionalTransience.iUnion_firstPairRecordDeviation line 267
  24. lemma OAI.DirectionalTransience.firstPairRecordDeviation_force_lower line 284
  25. lemma OAI.DirectionalTransience.independent_pair_deviation_transfer line 309
  26. lemma OAI.DirectionalTransience.measurableSet_pairIndexDeviation line 351
  27. lemma OAI.DirectionalTransience.independent_firstHit_pair_maximum line 365
  28. lemma OAI.DirectionalTransience.exists_integer_median line 407