OAI/Probability/Ballisticity/Estimates/CommonTrueRecord.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.noDropFinite_real_integral_translation line 12
  2. lemma OAI.DirectionalTransience.noDropFinite_toReal_le_one line 24
  3. lemma OAI.DirectionalTransience.noDrop_real_integrable line 29
  4. lemma OAI.DirectionalTransience.noDropFinite_real_integrable line 35
  5. lemma OAI.DirectionalTransience.noDropFinite_real_integral_tendsto line 41
  6. lemma OAI.DirectionalTransience.sharedNoDropMass_toReal line 56
  7. lemma OAI.DirectionalTransience.sharedNoDropMass_mixing line 67
  8. def OAI.DirectionalTransience.CommonTrueRecord line 147
  9. def OAI.DirectionalTransience.FirstCommonTrueRecord line 151
  10. lemma OAI.DirectionalTransience.measurableSet_commonTrueRecord line 155
  11. lemma OAI.DirectionalTransience.measurableSet_firstCommonTrueRecord line 165
  12. lemma OAI.DirectionalTransience.not_trueRecord_before_true_iff line 175
  13. def OAI.DirectionalTransience.AdmissibleCommonWords line 202
  14. lemma OAI.DirectionalTransience.noDrop_iff_prefix_and_future line 219
  15. lemma OAI.DirectionalTransience.commonTrueRecord_congr_prefix line 233
  16. lemma OAI.DirectionalTransience.firstCommonWords_characterization line 244
  17. def OAI.DirectionalTransience.commonPairSuffix line 300
  18. lemma OAI.DirectionalTransience.measurable_commonPairSuffix line 303
  19. def OAI.DirectionalTransience.commonWordEvent line 308
  20. lemma OAI.DirectionalTransience.measurableSet_commonWordEvent line 313
  21. lemma OAI.DirectionalTransience.common_word_suffix_event line 318
  22. lemma OAI.DirectionalTransience.shared_conditioned_common_word_rectangle line 351
  23. lemma OAI.DirectionalTransience.ae_of_frestrict_probability_lower line 398