OAI/Probability/FKMaps/HeightCoding.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FKCRT.TreeCoding.reversedPath line 14
  2. lemma OAI.FKCRT.TreeCoding.reverse_record_iff line 17
  3. lemma OAI.FKCRT.TreeCoding.reverse_record_filter_card line 40
  4. lemma OAI.FKCRT.TreeCoding.recordHeight_dual line 66
  5. lemma OAI.FKCRT.TreeCoding.reverseRecords_surviving_at_minimum line 71
  6. lemma OAI.FKCRT.TreeCoding.recordHeight_fall_dual line 93
  7. lemma OAI.FKCRT.TreeCoding.recordHeight_at_first_minimum_split line 117
  8. lemma OAI.FKCRT.TreeCoding.height_oscillation_of_reverse_ladders line 140
  9. lemma OAI.FKCRT.TreeCoding.weakRecords_congr_prefix line 164
  10. lemma OAI.FKCRT.TreeCoding.height_oscillation_of_reverse_extensions line 177
  11. lemma OAI.FKCRT.TreeCoding.height_oscillation_of_reverse_extensions_real line 211
  12. def OAI.FKCRT.TreeCoding.heightModulusFailure line 247
  13. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.ae_reverse_ladders line 255
  14. lemma OAI.FKCRT.TreeCoding.height_modulus_failure_subset line 262
  15. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.height_modulus_probability line 282
  16. lemma OAI.FKCRT.TreeCoding.conditional_event_bound line 309
  17. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.conditional_height_modulus_probability line 316
  18. def OAI.FKCRT.TreeCoding.standardExcursion line 325
  19. def OAI.FKCRT.TreeCoding.diagonalExcursion line 331
  20. def OAI.FKCRT.TreeCoding.jointBrownianExpectation line 339
  21. def OAI.FKCRT.TreeCoding.JointCodingStatement line 344
  22. def OAI.FKCRT.TreeCoding.circularReversePath line 356
  23. lemma OAI.FKCRT.TreeCoding.circularReversePath_prefix line 360
  24. lemma OAI.FKCRT.TreeCoding.circular_records_of_good line 365
  25. lemma OAI.FKCRT.TreeCoding.circular_record_height_of_good line 390
  26. lemma OAI.FKCRT.TreeCoding.circular_maximum_of_good line 396
  27. lemma OAI.FKCRT.TreeCoding.height_eq_recordHeight line 412
  28. lemma OAI.FKCRT.TreeCoding.walk_rotate_left line 431
  29. lemma OAI.FKCRT.TreeCoding.walk_rotate_right line 439
  30. lemma OAI.FKCRT.TreeCoding.circular_reverse_rotate line 447
  31. lemma OAI.FKCRT.TreeCoding.rotated_code_reverse_records line 465
  32. def OAI.FKCRT.TreeCoding.prefixMaximum line 475
  33. lemma OAI.FKCRT.TreeCoding.prefixMaximum_congr line 479
  34. lemma OAI.FKCRT.TreeCoding.prefixMaximum_eq line 487
  35. lemma OAI.FKCRT.TreeCoding.rotated_code_reverse_maximum line 494
  36. lemma OAI.FKCRT.TreeCoding.rotation_sum_invariant line 505
  37. lemma OAI.FKCRT.TreeCoding.canonical_rotation_sum line 512
  38. theorem OAI.FKCRT.TreeCoding.uniform_vertex_cyclic_identity line 518
  39. theorem OAI.FKCRT.TreeCoding.uniform_vertex_height_error line 547
  40. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridgeFourier line 567
  41. lemma OAI.FKCRT.TreeCoding.integral_standard_gaussian_complex line 571
  42. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridgeFourier_limit line 585
  43. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridgeFourier_integral line 613
  44. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridgeFourier_partition line 651
  45. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridgePartition_limit line 667
  46. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.codePartition_asymptotic line 685
  47. def OAI.FKCRT.TreeCoding.CriticalEvenOffspring.squareTail line 702
  48. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.squareTail_tendsto line 706
  49. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.squareTail_bound line 725
  50. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.sqrt_tail_small line 746
  51. def OAI.FKCRT.TreeCoding.codeEventMass line 763
  52. def OAI.FKCRT.TreeCoding.bridgeEventMass line 769
  53. theorem OAI.FKCRT.TreeCoding.codeEventMass_cyclic line 775
  54. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridgeEventMass_eq_iid line 802
  55. def OAI.FKCRT.TreeCoding.codeEventProbability line 843
  56. lemma OAI.FKCRT.TreeCoding.codeEventProbability_eq_bridge line 848
  57. lemma OAI.FKCRT.TreeCoding.maxDegree_rotation line 859
  58. lemma OAI.FKCRT.TreeCoding.code_max_probability_eq_iid line 870
  59. theorem OAI.FKCRT.TreeCoding.CriticalEvenOffspring.conditioned_max_degree line 885
  60. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_fixed_site_limit line 937
  61. lemma OAI.FKCRT.TreeCoding.sqrt_affine_ratio_limit line 968
  62. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_coordinate_limit line 987
  63. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.iid_pair_site line 1031
  64. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_coordinate_limit_any line 1059
  65. lemma OAI.FKCRT.TreeCoding.CriticalEvenOffspring.bridge_pair_limit line 1069