OAI/Probability/FKMaps/ConditionedWalk.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_bridge_pos line 13
  2. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridgeLaw line 19
  3. instance OAI.FKCRT.TreeCoding.(instance at line 24) line 24
  4. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridgeLaw_real line 31
  5. def OAI.FKCRT.TreeCoding.degreeFrequency line 45
  6. lemma OAI.FKCRT.TreeCoding.degreeFrequency_nonneg line 49
  7. lemma OAI.FKCRT.TreeCoding.degreeFrequency_le_one line 53
  8. lemma OAI.FKCRT.TreeCoding.degreeFrequency_integrable line 61
  9. lemma OAI.FKCRT.TreeCoding.degreeFrequency_square_integrable line 70
  10. lemma OAI.FKCRT.TreeCoding.coordinate_indicator_integrable line 83
  11. lemma OAI.FKCRT.TreeCoding.coordinate_pair_indicator_integrable line 90
  12. lemma OAI.FKCRT.TreeCoding.integral_coordinate_indicator line 98
  13. lemma OAI.FKCRT.TreeCoding.integral_coordinate_pair_indicator line 105
  14. lemma OAI.FKCRT.TreeCoding.integral_degreeFrequency line 117
  15. lemma OAI.FKCRT.TreeCoding.integral_degreeFrequency_sq line 127
  16. lemma OAI.FKCRT.TreeCoding.integral_degreeFrequency_square_error line 156
  17. lemma OAI.FKCRT.TreeCoding.degreeFrequency_deviation_bound line 175
  18. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_cond_real line 191
  19. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iidSiteProbability line 204
  20. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.singleBridgeProbability line 208
  21. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridgeFrequencyDeviation line 213
  22. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_frequency_limit line 219
  23. lemma OAI.FKCRT.TreeCoding.degreeFrequency_rotation line 287
  24. lemma OAI.FKCRT.TreeCoding.code_frequency_probability_eq_bridge line 297
  25. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.conditioned_degree_frequencies line 312
  26. lemma OAI.FKCRT.TreeCoding.degreeFrequency_abs_integrable line 320
  27. lemma OAI.FKCRT.TreeCoding.integral_degreeFrequency_abs_bound line 326
  28. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_frequency_l1_limit line 354
  29. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.BridgeDominated line 371
  30. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_coordinate_domination line 376
  31. lemma OAI.FKCRT.TreeCoding.integral_degreeFrequency_le line 426
  32. lemma OAI.FKCRT.TreeCoding.integral_degreeFrequency_abs_le line 438
  33. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_weighted_frequency_l1_limit line 449
  34. lemma OAI.FKCRT.TreeCoding.degreeFrequency_finite_support line 467
  35. lemma OAI.FKCRT.TreeCoding.summable_weighted_frequency_error line 479
  36. lemma OAI.FKCRT.TreeCoding.moment_eq_tsum_frequency line 488
  37. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_integrable line 505
  38. lemma OAI.FKCRT.TreeCoding.moment_deviation_le line 516
  39. def OAI.FKCRT.TreeCoding.empiricalSecondMoment line 528
  40. lemma OAI.FKCRT.TreeCoding.empiricalSecondMoment_rotation line 532
  41. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.secondMean line 540
  42. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.integral_moment_error_le line 544
  43. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_second_moment_l1_limit line 565
  44. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_moment_deviation_bound line 574
  45. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_second_moment_limit line 586
  46. lemma OAI.FKCRT.TreeCoding.code_second_moment_probability_eq_bridge line 594
  47. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.conditioned_second_moment line 609
  48. lemma OAI.FKCRT.TreeCoding.iid_prefix_endpoint_bound line 621
  49. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.PrefixDominated line 659
  50. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_prefix_domination line 666
  51. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.PrefixDominatedFraction line 726
  52. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_prefix_domination_fraction line 733