OAI/Probability/DirectionalWalk/RenewalFactorization.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalZeroOne.measurable_dependent_subtype_tsum line 12
  2. lemma OAI.DirectionalZeroOne.measurable_contactBinMass line 24
  3. lemma OAI.DirectionalZeroOne.measurable_quenched_apply line 46
  4. lemma OAI.DirectionalZeroOne.measurable_kernel_weighted_sum line 50
  5. lemma OAI.DirectionalZeroOne.measurable_weighted_contact_tsum line 59
  6. lemma OAI.DirectionalZeroOne.totalPosterior_le_bins line 68
  7. lemma OAI.DirectionalZeroOne.posterior_contact_raw_bound line 118
  8. def OAI.DirectionalZeroOne.commonCount line 166
  9. def OAI.DirectionalZeroOne.listCommonCount line 170
  10. lemma OAI.DirectionalZeroOne.commonCount_cutList line 175
  11. lemma OAI.DirectionalZeroOne.commonCount_zero line 186
  12. lemma OAI.DirectionalZeroOne.commonCount_succ line 189
  13. lemma OAI.DirectionalZeroOne.commonCount_mono line 194
  14. lemma OAI.DirectionalZeroOne.commonCount_lt_at_cut line 200
  15. lemma OAI.DirectionalZeroOne.commonCut_count_injective line 210
  16. lemma OAI.DirectionalZeroOne.commonCount_add line 218
  17. lemma OAI.DirectionalZeroOne.commonCount_first line 229
  18. lemma OAI.DirectionalZeroOne.twoShift_comp line 243
  19. lemma OAI.DirectionalZeroOne.cutListIndex_spec line 248
  20. lemma OAI.DirectionalZeroOne.afterCommonCut_add line 254
  21. def OAI.DirectionalZeroOne.commonDepth line 273
  22. lemma OAI.DirectionalZeroOne.commonDepth_zero line 276
  23. lemma OAI.DirectionalZeroOne.commonDepth_succ line 279
  24. lemma OAI.DirectionalZeroOne.commonDepth_spec line 283
  25. lemma OAI.DirectionalZeroOne.ae_common_iterates line 308
  26. lemma OAI.DirectionalZeroOne.measurable_commonDepth line 317
  27. def OAI.DirectionalZeroOne.nthCommonList line 322
  28. lemma OAI.DirectionalZeroOne.measurable_nthCommonList line 325
  29. def OAI.DirectionalZeroOne.BalancedList line 331
  30. lemma OAI.DirectionalZeroOne.nthCommonList_atom_iff line 334
  31. def OAI.DirectionalZeroOne.nthCommonLaw line 354
  32. instance OAI.DirectionalZeroOne.nthCommonLaw_probability line 359
  33. lemma OAI.DirectionalZeroOne.nthCommonLaw_atom line 364
  34. lemma OAI.DirectionalZeroOne.nthCommon_suffix_factorization line 389
  35. def OAI.DirectionalZeroOne.windowCommonLaw line 423
  36. instance OAI.DirectionalZeroOne.windowCommonLaw_probability line 428
  37. def OAI.DirectionalZeroOne.twoListWeight line 436