OAI/NumberTheory/Jacobsthal/Probability/CemeteryHistoryLaw.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos970.NumberTheoryLean.CemeteryKernel.Space line 19
  2. def OAI.Erdos970.NumberTheoryLean.CemeteryKernel.dead line 21
  3. def OAI.Erdos970.NumberTheoryLean.CemeteryKernel.cemeteryPart line 23
  4. theorem OAI.Erdos970.NumberTheoryLean.CemeteryKernel.cemeteryPart_measurable line 26
  5. theorem OAI.Erdos970.NumberTheoryLean.CemeteryKernel.cemeteryPart_apply line 30
  6. def OAI.Erdos970.NumberTheoryLean.CemeteryKernel.liveRow line 34
  7. theorem OAI.Erdos970.NumberTheoryLean.CemeteryKernel.liveRow_apply line 36
  8. def OAI.Erdos970.NumberTheoryLean.CemeteryKernel.complete line 40
  9. theorem OAI.Erdos970.NumberTheoryLean.CemeteryKernel.complete_live line 44
  10. theorem OAI.Erdos970.NumberTheoryLean.CemeteryKernel.complete_dead line 45
  11. theorem OAI.Erdos970.NumberTheoryLean.CemeteryKernel.complete_isMarkov line 47
  12. theorem OAI.Erdos970.NumberTheoryLean.CemeteryKernel.complete_live_mass line 62
  13. def OAI.Erdos970.NumberTheoryLean.CemeteryPowers.liftReward line 86
  14. theorem OAI.Erdos970.NumberTheoryLean.CemeteryPowers.liftReward_measurable line 88
  15. theorem OAI.Erdos970.NumberTheoryLean.CemeteryPowers.row_lift line 91
  16. theorem OAI.Erdos970.NumberTheoryLean.CemeteryPowers.power_lift line 105
  17. def OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.live line 145
  18. theorem OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.live_measurable line 147
  19. def OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.killStep line 150
  20. theorem OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.killStep_measurable line 154
  21. theorem OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.killStep_eq_or_dead line 161
  22. theorem OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.extend_restrict line 167
  23. def OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.killHist line 173
  24. theorem OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.killHist_measurable line 179
  25. theorem OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.killHist_extend line 188
  26. theorem OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.killHist_last line 193
  27. def OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.aliveThrough line 216
  28. theorem OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.aliveThrough_succ line 220
  29. theorem OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.killHist_restrict line 236
  30. theorem OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.killHist_last_exact line 257
  31. theorem OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.killHist_coordinate line 274
  32. theorem OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.killStep_live_map line 298
  33. theorem OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.killStep_dead_map line 322
  34. theorem OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.killHist_step_map line 330
  35. instance OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.restricted_complete_markov line 339
  36. theorem OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.lintegral_killHist line 360
  37. theorem OAI.Erdos970.NumberTheoryLean.CemeteryHistoryMap.pathMeasure_killHist line 389