OAI/NumberTheory/Jacobsthal/Paths/FlaggedSourceStart.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.FlagState line 17
  2. def OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.badBit line 19
  3. theorem OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.badBit_measurable line 23
  4. def OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.update line 27
  5. theorem OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.update_measurable line 30
  6. def OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.marked line 35
  7. instance OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.marked_isMarkov line 39
  8. theorem OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.marked_apply line 44
  9. theorem OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.row_update_measurable line 53
  10. theorem OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.marked_eq_map line 58
  11. theorem OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.marked_map line 66
  12. def OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.failed line 72
  13. theorem OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.failed_measurable line 74
  14. theorem OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.marked_failed_true line 77
  15. theorem OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.marked_failed_false line 82
  16. instance OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.marked_pow_markov line 90
  17. theorem OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.marked_power_map line 100
  18. def OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.law line 105
  19. instance OAI.Erdos970.NumberTheoryLean.PersistentFailureFlag.law_probability line 108
  20. def OAI.Erdos970.NumberTheoryLean.FailureFlagBounds.surviving line 125
  21. theorem OAI.Erdos970.NumberTheoryLean.FailureFlagBounds.surviving_measurable line 127
  22. theorem OAI.Erdos970.NumberTheoryLean.FailureFlagBounds.surviving_step line 131
  23. theorem OAI.Erdos970.NumberTheoryLean.FailureFlagBounds.law_survives line 151
  24. theorem OAI.Erdos970.NumberTheoryLean.FailureFlagBounds.marked_failure_row_bound line 169
  25. theorem OAI.Erdos970.NumberTheoryLean.FailureFlagBounds.law_failure_step line 183
  26. theorem OAI.Erdos970.NumberTheoryLean.FailureFlagBounds.failure_probability_le line 202
  27. def OAI.Erdos970.NumberTheoryLean.FullHistoryFailureFlag.noResetPath line 236
  28. theorem OAI.Erdos970.NumberTheoryLean.FullHistoryFailureFlag.noResetPath_measurable line 239
  29. theorem OAI.Erdos970.NumberTheoryLean.FullHistoryFailureFlag.noResetPath_extend line 246
  30. theorem OAI.Erdos970.NumberTheoryLean.FullHistoryFailureFlag.marked_no_reset line 261
  31. theorem OAI.Erdos970.NumberTheoryLean.FullHistoryFailureFlag.marked_history_no_reset line 272
  32. def OAI.Erdos970.NumberTheoryLean.ActualFlagInvariant.mismatch line 299
  33. theorem OAI.Erdos970.NumberTheoryLean.ActualFlagInvariant.mismatch_measurable line 302
  34. def OAI.Erdos970.NumberTheoryLean.ActualFlagInvariant.liveGood line 308
  35. def OAI.Erdos970.NumberTheoryLean.ActualFlagInvariant.GoodAt line 312
  36. theorem OAI.Erdos970.NumberTheoryLean.ActualFlagInvariant.liveGood_measurable line 317
  37. theorem OAI.Erdos970.NumberTheoryLean.ActualFlagInvariant.GoodAt_measurable line 330
  38. theorem OAI.Erdos970.NumberTheoryLean.ActualFlagInvariant.joint_dead_ae line 342
  39. theorem OAI.Erdos970.NumberTheoryLean.ActualFlagInvariant.actual_good_step line 368
  40. def OAI.Erdos970.NumberTheoryLean.ActualFlagInvariant.flaggedKernel line 409
  41. instance OAI.Erdos970.NumberTheoryLean.ActualFlagInvariant.flaggedKernel_markov line 413
  42. theorem OAI.Erdos970.NumberTheoryLean.ActualFlagInvariant.actual_flagged_invariant line 418
  43. def OAI.Erdos970.NumberTheoryLean.FlaggedSourceStart.typedState line 437
  44. theorem OAI.Erdos970.NumberTheoryLean.FlaggedSourceStart.typedState_side line 441
  45. theorem OAI.Erdos970.NumberTheoryLean.FlaggedSourceStart.typedState_ratio line 444
  46. def OAI.Erdos970.NumberTheoryLean.FlaggedSourceStart.sourceCostState line 449
  47. def OAI.Erdos970.NumberTheoryLean.FlaggedSourceStart.sourceJoint line 452
  48. theorem OAI.Erdos970.NumberTheoryLean.FlaggedSourceStart.source_gap line 455
  49. theorem OAI.Erdos970.NumberTheoryLean.FlaggedSourceStart.source_good line 459
  50. def OAI.Erdos970.NumberTheoryLean.FlaggedSourceStart.sourceLaw line 476
  51. instance OAI.Erdos970.NumberTheoryLean.FlaggedSourceStart.sourceLaw_probability line 480
  52. theorem OAI.Erdos970.NumberTheoryLean.FlaggedSourceStart.sourceLaw_joint line 485
  53. theorem OAI.Erdos970.NumberTheoryLean.FlaggedSourceStart.sourceLaw_prime line 490
  54. theorem OAI.Erdos970.NumberTheoryLean.FlaggedSourceStart.sourceLaw_continuous line 497
  55. theorem OAI.Erdos970.NumberTheoryLean.FlaggedSourceStart.sourceLaw_good line 505