OAI/Probability/DirectionalWalk/CommonBlocks.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.firstCommonWidth line 12
  2. lemma OAI.DirectionalZeroOne.firstCommonWidth_spec line 16
  3. lemma OAI.DirectionalZeroOne.firstCommonWidth_zero_iff line 24
  4. lemma OAI.DirectionalZeroOne.firstCommonWidth_eq_pos_iff line 32
  5. lemma OAI.DirectionalZeroOne.measurable_firstCommonWidth line 51
  6. lemma OAI.DirectionalZeroOne.firstCommonWidth_tail_subset line 68
  7. lemma OAI.DirectionalZeroOne.ae_exists_commonCut line 74
  8. lemma OAI.DirectionalZeroOne.lintegral_firstCommonWidth_le line 89
  9. lemma OAI.DirectionalZeroOne.integrable_firstCommonWidth line 99
  10. def OAI.DirectionalZeroOne.listHasCut line 111
  11. lemma OAI.DirectionalZeroOne.listHasCut_prefix line 114
  12. lemma OAI.DirectionalZeroOne.renewalCut_iff_listHasCut line 119
  13. lemma OAI.DirectionalZeroOne.commonCut_iff_listHasCut line 130
  14. def OAI.DirectionalZeroOne.firstCommonBlock line 135
  15. def OAI.DirectionalZeroOne.commonRestart line 138
  16. lemma OAI.DirectionalZeroOne.measurable_firstCommonBlock line 141
  17. lemma OAI.DirectionalZeroOne.measurable_commonRestart line 147
  18. def OAI.DirectionalZeroOne.IsFirstCommonList line 153
  19. lemma OAI.DirectionalZeroOne.firstCommonBlock_spec line 158
  20. lemma OAI.DirectionalZeroOne.firstCommonBlock_atom_iff line 170
  21. lemma OAI.DirectionalZeroOne.commonRestart_eq_shift line 189
  22. def OAI.DirectionalZeroOne.commonBlockLaw line 195
  23. lemma OAI.DirectionalZeroOne.firstCommonBlock_suffix_factorization line 200
  24. lemma OAI.DirectionalZeroOne.commonRestart_measurePreserving line 236
  25. def OAI.DirectionalZeroOne.commonNeeds line 254
  26. lemma OAI.DirectionalZeroOne.commonNeeds_iff line 258
  27. lemma OAI.DirectionalZeroOne.coordSigma_le line 292
  28. lemma OAI.DirectionalZeroOne.measurableSet_commonNeeds_rest line 296
  29. lemma OAI.DirectionalZeroOne.measurableSet_commonNeeds line 331
  30. lemma OAI.DirectionalZeroOne.commonNeeds_next_independent line 336
  31. lemma OAI.DirectionalZeroOne.commonNeeds_radius_factorization line 358
  32. def OAI.DirectionalZeroOne.listCost line 381
  33. lemma OAI.DirectionalZeroOne.firstCommonBlock_length_le line 384
  34. lemma OAI.DirectionalZeroOne.firstCommonBlock_cost_eq line 393
  35. lemma OAI.DirectionalZeroOne.commonBlock_Wald line 413
  36. lemma OAI.DirectionalZeroOne.commonBlock_cost_bound line 444