OAI/Probability/Ballisticity/Estimates/CommonWordWidth.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.recordCount_eq_height_at_record line 12
  2. lemma OAI.DirectionalTransience.independent_conditioned_true_at_index_lower line 26
  3. def OAI.DirectionalTransience.commonWordWidth line 62
  4. lemma OAI.DirectionalTransience.commonWordWidth_positive line 65
  5. lemma OAI.DirectionalTransience.independent_commonWordWidth_integrable line 73
  6. lemma OAI.DirectionalTransience.singleCommonIndex_exists_bound line 119
  7. def OAI.DirectionalTransience.singleCommonIndex line 125
  8. lemma OAI.DirectionalTransience.measurable_singleCommonIndex line 128
  9. lemma OAI.DirectionalTransience.singleCommonIndex_time line 138
  10. lemma OAI.DirectionalTransience.singleCommonIndex_le_width line 151
  11. lemma OAI.DirectionalTransience.commonWordRadius_le_single_sum line 166
  12. lemma OAI.DirectionalTransience.finite_prefix_sum_eq line 177
  13. def OAI.DirectionalTransience.NoCommonInPrefix line 192
  14. lemma OAI.DirectionalTransience.measurableSet_noCommonInPrefix line 197
  15. lemma OAI.DirectionalTransience.singleCommonIndex_gt_iff line 216
  16. lemma OAI.DirectionalTransience.indepFun_past_product line 266
  17. lemma OAI.DirectionalTransience.tsum_nat_lt_ennreal line 287
  18. lemma OAI.DirectionalTransience.lintegral_stopped_iid_sum line 297
  19. lemma OAI.DirectionalTransience.independent_conditioned_singleCommonIndex_indep line 328
  20. lemma OAI.DirectionalTransience.independent_singleCommonIndex_integrable line 364
  21. lemma OAI.DirectionalTransience.identDistrib_fst line 385
  22. lemma OAI.DirectionalTransience.independent_commonWordRadius_fst_integrable line 396