OAI/NumberTheory/Jacobsthal/Probability/FirstHitKernels.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.evenToOdd_map_ratio line 17
  2. theorem OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.oddToEven_map_ratio line 25
  3. theorem OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.stateKernel_even_ratio line 33
  4. theorem OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.stateKernel_odd_ratio line 40
  5. theorem OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.evenToOdd_lintegral_ratio line 47
  6. theorem OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.oddToEven_lintegral_ratio line 51
  7. theorem OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.evenKernel_lintegral_density line 55
  8. theorem OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.oddKernel_lintegral_density line 62
  9. theorem OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.transitionDensity_joint_measurable line 69
  10. def OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.evenTwoStep line 88
  11. def OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.oddTwoStep line 91
  12. instance OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.evenTwoStep_isMarkovKernel line 94
  13. instance OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.oddTwoStep_isMarkovKernel line 98
  14. theorem OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.evenTwoStep_lintegral line 102
  15. theorem OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.oddTwoStep_lintegral line 129
  16. def OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.jointDensity line 156
  17. theorem OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.jointDensity_measurable line 159
  18. theorem OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.evenTwoStep_eq_withDensity line 164
  19. theorem OAI.Erdos970.NumberTheoryLean.KernelDensityBridge.oddTwoStep_eq_withDensity line 174
  20. def OAI.Erdos970.NumberTheoryLean.JointMinorization.rectangle line 197
  21. theorem OAI.Erdos970.NumberTheoryLean.JointMinorization.rectangle_measurable line 199
  22. def OAI.Erdos970.NumberTheoryLean.JointMinorization.rectangleLaw line 202
  23. instance OAI.Erdos970.NumberTheoryLean.JointMinorization.rectangleLaw_isProbabilityMeasure line 205
  24. theorem OAI.Erdos970.NumberTheoryLean.JointMinorization.transitionDensity_nonneg line 212
  25. theorem OAI.Erdos970.NumberTheoryLean.JointMinorization.rectangle_minorization line 218
  26. theorem OAI.Erdos970.NumberTheoryLean.JointMinorization.evenTwoStep_rectangle_minorization line 237
  27. theorem OAI.Erdos970.NumberTheoryLean.JointMinorization.oddTwoStep_rectangle_minorization line 243
  28. def OAI.Erdos970.NumberTheoryLean.JointMinorization.pairCost line 249
  29. theorem OAI.Erdos970.NumberTheoryLean.JointMinorization.pairCost_measurable line 252
  30. def OAI.Erdos970.NumberTheoryLean.JointMinorization.minorizingLaw line 256
  31. instance OAI.Erdos970.NumberTheoryLean.JointMinorization.minorizingLaw_isProbabilityMeasure line 258
  32. def OAI.Erdos970.NumberTheoryLean.JointMinorization.evenJointKernel line 262
  33. def OAI.Erdos970.NumberTheoryLean.JointMinorization.oddJointKernel line 263
  34. instance OAI.Erdos970.NumberTheoryLean.JointMinorization.evenJointKernel_isMarkovKernel line 265
  35. instance OAI.Erdos970.NumberTheoryLean.JointMinorization.oddJointKernel_isMarkovKernel line 268
  36. theorem OAI.Erdos970.NumberTheoryLean.JointMinorization.even_joint_minorization line 271
  37. theorem OAI.Erdos970.NumberTheoryLean.JointMinorization.odd_joint_minorization line 278
  38. theorem OAI.Erdos970.NumberTheoryLean.JointMinorization.compact_joint_minorization line 285
  39. def OAI.Erdos970.NumberTheoryLean.GoodPairTransitions.goodPair line 311
  40. theorem OAI.Erdos970.NumberTheoryLean.GoodPairTransitions.goodPair_measurable line 315
  41. theorem OAI.Erdos970.NumberTheoryLean.GoodPairTransitions.goodPair_volume line 321
  42. theorem OAI.Erdos970.NumberTheoryLean.GoodPairTransitions.goodPair_bounds line 344
  43. theorem OAI.Erdos970.NumberTheoryLean.GoodPairTransitions.goodPair_terminal line 350
  44. theorem OAI.Erdos970.NumberTheoryLean.GoodPairTransitions.phiOdd_le_A line 362
  45. def OAI.Erdos970.NumberTheoryLean.GoodPairTransitions.goodPairDensityLower line 368
  46. theorem OAI.Erdos970.NumberTheoryLean.GoodPairTransitions.goodPairDensityLower_pos line 370
  47. theorem OAI.Erdos970.NumberTheoryLean.GoodPairTransitions.goodPair_density_lower line 374
  48. theorem OAI.Erdos970.NumberTheoryLean.GoodPairTransitions.goodPair_measure_lower line 393
  49. def OAI.Erdos970.NumberTheoryLean.GoodPairTransitions.goodPairProbability line 417
  50. theorem OAI.Erdos970.NumberTheoryLean.GoodPairTransitions.goodPairProbability_pos line 419
  51. theorem OAI.Erdos970.NumberTheoryLean.GoodPairTransitions.goodPairProbability_le_one line 422
  52. theorem OAI.Erdos970.NumberTheoryLean.GoodPairTransitions.odd_terminal_progress line 425
  53. def OAI.Erdos970.NumberTheoryLean.FirstHitKernels.regenerationStateSet line 445
  54. theorem OAI.Erdos970.NumberTheoryLean.FirstHitKernels.regenerationStateSet_measurable line 449
  55. def OAI.Erdos970.NumberTheoryLean.FirstHitKernels.regenerationSet line 455
  56. theorem OAI.Erdos970.NumberTheoryLean.FirstHitKernels.regenerationSet_measurable line 457
  57. theorem OAI.Erdos970.NumberTheoryLean.FirstHitKernels.regeneration_even line 460
  58. theorem OAI.Erdos970.NumberTheoryLean.FirstHitKernels.regeneration_odd line 463
  59. def OAI.Erdos970.NumberTheoryLean.FirstHitKernels.killed line 466
  60. def OAI.Erdos970.NumberTheoryLean.FirstHitKernels.captured line 467
  61. instance OAI.Erdos970.NumberTheoryLean.FirstHitKernels.killed_isFiniteKernel line 469
  62. instance OAI.Erdos970.NumberTheoryLean.FirstHitKernels.captured_isFiniteKernel line 470
  63. instance OAI.Erdos970.NumberTheoryLean.FirstHitKernels.killed_pow_isFiniteKernel line 472
  64. theorem OAI.Erdos970.NumberTheoryLean.FirstHitKernels.captured_add_killed line 480
  65. def OAI.Erdos970.NumberTheoryLean.FirstHitKernels.firstHit line 485
  66. instance OAI.Erdos970.NumberTheoryLean.FirstHitKernels.firstHit_isFiniteKernel line 487
  67. def OAI.Erdos970.NumberTheoryLean.FirstHitKernels.firstHitLaw line 491
  68. instance OAI.Erdos970.NumberTheoryLean.FirstHitKernels.firstHitLaw_isSFiniteKernel line 493
  69. theorem OAI.Erdos970.NumberTheoryLean.FirstHitKernels.firstHit_mass_step line 497
  70. theorem OAI.Erdos970.NumberTheoryLean.FirstHitKernels.firstHit_finite_mass line 507
  71. theorem OAI.Erdos970.NumberTheoryLean.FirstHitKernels.survival_mass_le_one line 522
  72. theorem OAI.Erdos970.NumberTheoryLean.FirstHitKernels.firstHit_partial_mass_le_one line 527
  73. theorem OAI.Erdos970.NumberTheoryLean.FirstHitKernels.survival_mass_antitone line 533
  74. theorem OAI.Erdos970.NumberTheoryLean.FirstHitKernels.firstHitLaw_mass_le_one line 540
  75. instance OAI.Erdos970.NumberTheoryLean.FirstHitKernels.firstHitLaw_isFiniteKernel line 544
  76. theorem OAI.Erdos970.NumberTheoryLean.FirstHitKernels.firstHitLaw_probability_of_survival_vanishes line 547
  77. theorem OAI.Erdos970.NumberTheoryLean.FirstHitKernels.captured_off_regeneration line 556
  78. theorem OAI.Erdos970.NumberTheoryLean.FirstHitKernels.firstHit_off_regeneration line 560
  79. theorem OAI.Erdos970.NumberTheoryLean.FirstHitKernels.firstHitLaw_off_regeneration line 564
  80. theorem OAI.Erdos970.NumberTheoryLean.FirstHitKernels.costKernel_increases_cost line 568