OAI/NumberTheory/Jacobsthal/Paths/FiniteHistorySupport.lean

GitHub source file

115 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.Side line 16
  2. def OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.Side.flip line 18
  3. def OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.weight line 20
  4. def OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.Valid line 22
  5. def OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.minRatio line 26
  6. def OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.transitionDensity line 30
  7. def OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.Admissible line 33
  8. def OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.nextExponent line 37
  9. def OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.nextGap line 38
  10. def OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.cost line 39
  11. def OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.finalGap line 41
  12. def OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.finalRatio line 45
  13. def OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.finalSide line 49
  14. def OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.pathCost line 53
  15. def OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.harmonicDensity line 57
  16. def OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.tiltedDensity line 61
  17. def OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.AllExponentsAbove line 65
  18. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.valid_pos line 69
  19. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.weight_pos line 72
  20. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.valid_next line 77
  21. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.minRatio_ge_sub_one line 86
  22. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.transitionDensity_even line 91
  23. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.transitionDensity_odd line 92
  24. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.nextGap_pos line 94
  25. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.nextExponent_pos line 98
  26. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.gap_exponent_conservation line 102
  27. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.nextGap_div_ratio line 107
  28. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.nextRatio_identity line 111
  29. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.exponent_le_cutoff line 116
  30. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.upper_standard_admission line 123
  31. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.step_weight_identity line 133
  32. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.valid_final line 146
  33. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.finalGap_pos line 152
  34. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.telescoping_path_weight line 160
  35. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.cost_pos line 180
  36. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.nextGap_eq_cost line 184
  37. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.finalGap_eq_cost line 190
  38. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.final_gap_ratio_le_cutoff line 201
  39. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.all_exponents_iff_final line 213
  40. theorem OAI.Erdos970.NumberTheoryLean.FinitePathGeometry.arrival_cutoff line 234
  41. abbrev OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.State line 252
  42. abbrev OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.CostState line 253
  43. def OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.evenToOdd line 255
  44. def OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.oddToEven line 258
  45. instance OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.evenToOdd_isMarkovKernel line 261
  46. instance OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.oddToEven_isMarkovKernel line 273
  47. def OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.evenBranch line 285
  48. def OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.oddBranch line 286
  49. instance OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.evenBranch_isMarkovKernel line 288
  50. instance OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.oddBranch_isMarkovKernel line 291
  51. def OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.stateKernel line 294
  52. instance OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.stateKernel_isMarkovKernel line 298
  53. def OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.stateRatio line 305
  54. def OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.stateSide line 306
  55. theorem OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.stateRatio_valid line 308
  56. theorem OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.stateRatio_measurable line 313
  57. theorem OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.cost_measurable line 316
  58. def OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.addCost line 320
  59. theorem OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.addCost_measurable line 323
  60. def OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.costKernel line 327
  61. instance OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.costKernel_isMarkovKernel line 330
  62. theorem OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.costKernel_apply line 333
  63. def OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.historyKernel line 341
  64. instance OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.historyKernel_isMarkovKernel line 345
  65. def OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.finitePathKernel line 349
  66. instance OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.finitePathKernel_isMarkovKernel line 353
  67. def OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.finitePathMeasure line 357
  68. instance OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.finitePathMeasure_isProbabilityMeasure line 360
  69. theorem OAI.Erdos970.NumberTheoryLean.FinitePathMeasures.finite_history_factorization line 365
  70. def OAI.Erdos970.NumberTheoryLean.ReciprocalGapExposure.potential line 378
  71. theorem OAI.Erdos970.NumberTheoryLean.ReciprocalGapExposure.potential_step_mono line 380
  72. theorem OAI.Erdos970.NumberTheoryLean.ReciprocalGapExposure.selected_step_exposure line 386
  73. def OAI.Erdos970.NumberTheoryLean.ReciprocalGapExposure.exposure line 406
  74. theorem OAI.Erdos970.NumberTheoryLean.ReciprocalGapExposure.exposure_potential line 410
  75. theorem OAI.Erdos970.NumberTheoryLean.ReciprocalGapExposure.exposure_bound line 423
  76. theorem OAI.Erdos970.NumberTheoryLean.ReciprocalGapExposure.admissible_exposure_bound line 432
  77. abbrev OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.Hist line 454
  78. def OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.last line 456
  79. def OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.mapHist line 458
  80. def OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.extend line 461
  81. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.mapHist_measurable line 465
  82. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.extend_measurable line 469
  83. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.mapHist_extend line 474
  84. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.last_measurable_for_comap line 482
  85. def OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.pastKernel line 485
  86. instance OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.pastKernel_sfinite line 489
  87. def OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.pathKernel line 494
  88. instance OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.pathKernel_sfinite line 498
  89. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.lintegral_pathKernel_succ line 503
  90. theorem OAI.Erdos970.NumberTheoryLean.FiniteGapExposure.finite_potential_telescope line 527
  91. theorem OAI.Erdos970.NumberTheoryLean.FiniteGapExposure.finite_arrival_exposure line 534
  92. theorem OAI.Erdos970.NumberTheoryLean.FiniteGapExposure.finite_all_exposure line 552
  93. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.lintegral_mapHist line 582
  94. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.pathKernel_mapHist line 612
  95. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.pathMeasure_mapHist line 620
  96. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.extend_last line 637
  97. instance OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.pastKernel_markov line 640
  98. instance OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.pathKernel_markov line 645
  99. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.last_measurable line 650
  100. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.lintegral_endpoint line 655
  101. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.pathKernel_endpoint line 670
  102. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.pathMeasure_endpoint line 677
  103. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.pathMeasure_coordinate line 681
  104. def OAI.Erdos970.NumberTheoryLean.FiniteHistoryOccurrence.atIndex line 700
  105. def OAI.Erdos970.NumberTheoryLean.FiniteHistoryOccurrence.arrivalOccurrence line 703
  106. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryOccurrence.arrivalOccurrence_measurable line 706
  107. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryOccurrence.atIndex_law line 712
  108. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryOccurrence.probability_integrable line 716
  109. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryOccurrence.next_probability_identity line 727
  110. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryOccurrence.occurrence_le_integrated_hazards line 752
  111. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.ae_pathKernel_succ line 773
  112. def OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.pathSum line 789
  113. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.pathSum_measurable line 792
  114. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.extend_previous line 797
  115. theorem OAI.Erdos970.NumberTheoryLean.FiniteHistoryTransport.pathSum_extend line 801