OAI/NumberTheory/Jacobsthal/Renewal/RegenerativeOddOccupation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.Erdos970Dependency.RegenerationMass.oddMeasure_below_one line 18
  2. theorem OAI.Erdos970.Erdos970Dependency.RegenerationMass.oddMeasure_regeneration_interval line 26
  3. theorem OAI.Erdos970.Erdos970Dependency.RegenerationMass.oddMeasure_Iic_three line 34
  4. theorem OAI.Erdos970.Erdos970Dependency.RegenerationMass.oddStateMeasure_regeneration line 42
  5. theorem OAI.Erdos970.Erdos970Dependency.RegenerationMass.oddStateMeasure_mass_pos line 51
  6. theorem OAI.Erdos970.Erdos970Dependency.RegenerationMass.stateMeasure_mass_pos line 57
  7. theorem OAI.Erdos970.Erdos970Dependency.RegenerationMass.stateMeasure_ne_zero line 64
  8. theorem OAI.Erdos970.Erdos970Dependency.RegenerativeOddOccupation.paired_invariance line 85
  9. theorem OAI.Erdos970.Erdos970Dependency.RegenerativeOddOccupation.odd_draw_common line 88
  10. theorem OAI.Erdos970.Erdos970Dependency.RegenerativeOddOccupation.paired_common line 93
  11. theorem OAI.Erdos970.Erdos970Dependency.RegenerativeOddOccupation.killed_common line 97
  12. theorem OAI.Erdos970.Erdos970Dependency.RegenerativeOddOccupation.odd_source_equation line 101
  13. def OAI.Erdos970.Erdos970Dependency.RegenerativeOddOccupation.ratioVisits line 106
  14. instance OAI.Erdos970.Erdos970Dependency.RegenerativeOddOccupation.ratioVisits_isFiniteKernel line 109
  15. theorem OAI.Erdos970.Erdos970Dependency.RegenerativeOddOccupation.ratioVisits_common line 111
  16. theorem OAI.Erdos970.Erdos970Dependency.RegenerativeOddOccupation.ratioVisits_invariant_mass line 116
  17. def OAI.Erdos970.Erdos970Dependency.RegenerativeOddOccupation.ratioOccupation line 121
  18. theorem OAI.Erdos970.Erdos970Dependency.RegenerativeOddOccupation.stateMeasure_eq_occupation line 124
  19. theorem OAI.Erdos970.Erdos970Dependency.RegenerativeOddOccupation.ratioOccupation_eq line 132