OAI/NumberTheory/Jacobsthal/Paths/ActualThresholdArrival.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.LiveKilledPrefixes.live_coordinate_original line 20
  2. theorem OAI.Erdos970.NumberTheoryLean.LiveKilledPrefixes.live_prefix_preserved line 30
  3. def OAI.Erdos970.NumberTheoryLean.CompletedArrivalOccurrence.liveMember line 54
  4. theorem OAI.Erdos970.NumberTheoryLean.CompletedArrivalOccurrence.liveMember_measurable line 58
  5. def OAI.Erdos970.NumberTheoryLean.CompletedArrivalOccurrence.completedOccurrence line 61
  6. theorem OAI.Erdos970.NumberTheoryLean.CompletedArrivalOccurrence.completedOccurrence_measurable line 64
  7. theorem OAI.Erdos970.NumberTheoryLean.CompletedArrivalOccurrence.kill_completed_subset line 72
  8. theorem OAI.Erdos970.NumberTheoryLean.CompletedArrivalOccurrence.source_completed_occurrence_le line 91
  9. def OAI.Erdos970.NumberTheoryLean.CanonicalGapExposure.coordinate line 109
  10. def OAI.Erdos970.NumberTheoryLean.CanonicalGapExposure.pathExposure line 112
  11. theorem OAI.Erdos970.NumberTheoryLean.CanonicalGapExposure.pathExposure_measurable line 116
  12. theorem OAI.Erdos970.NumberTheoryLean.CanonicalGapExposure.pathExposure_nonneg line 126
  13. theorem OAI.Erdos970.NumberTheoryLean.CanonicalGapExposure.canonical_gap_steps line 133
  14. theorem OAI.Erdos970.NumberTheoryLean.CanonicalGapExposure.canonical_exposure_bound line 151
  15. theorem OAI.Erdos970.NumberTheoryLean.CanonicalGapExposure.canonical_exposure_integral line 159
  16. def OAI.Erdos970.NumberTheoryLean.CanonicalEvenArrivalSupport.evenArrivalSupport line 182
  17. theorem OAI.Erdos970.NumberTheoryLean.CanonicalEvenArrivalSupport.evenArrivalSupport_measurable line 184
  18. theorem OAI.Erdos970.NumberTheoryLean.CanonicalEvenArrivalSupport.costKernel_even_output line 194
  19. theorem OAI.Erdos970.NumberTheoryLean.CanonicalEvenArrivalSupport.path_arrival_support line 206
  20. theorem OAI.Erdos970.NumberTheoryLean.CanonicalEvenArrivalSupport.canonical_even_arrivals line 221
  21. theorem OAI.Erdos970.NumberTheoryLean.ThresholdExposureBridge.odd_threshold_zero_high_parent line 237
  22. theorem OAI.Erdos970.NumberTheoryLean.ThresholdExposureBridge.odd_threshold_zero_small_gap line 252
  23. def OAI.Erdos970.NumberTheoryLean.ThresholdExposureBridge.thresholdHazard line 257
  24. theorem OAI.Erdos970.NumberTheoryLean.ThresholdExposureBridge.thresholdHazard_exposure line 261
  25. theorem OAI.Erdos970.NumberTheoryLean.ThresholdExposureBridge.canonical_total_threshold_hazard line 281
  26. theorem OAI.Erdos970.NumberTheoryLean.CoupledEvenArrivalSupport.killed_even_coordinate line 311
  27. theorem OAI.Erdos970.NumberTheoryLean.CoupledEvenArrivalSupport.sourceHistory_even_arrivals line 333
  28. def OAI.Erdos970.NumberTheoryLean.ActualThresholdArrival.thresholdArrival line 367
  29. theorem OAI.Erdos970.NumberTheoryLean.ActualThresholdArrival.thresholdArrival_measurable line 372
  30. theorem OAI.Erdos970.NumberTheoryLean.ActualThresholdArrival.thresholdArrival_update line 381
  31. theorem OAI.Erdos970.NumberTheoryLean.ActualThresholdArrival.thresholdHazard_eq_actual line 388
  32. theorem OAI.Erdos970.NumberTheoryLean.ActualThresholdArrival.actualHazard_measurable line 418
  33. theorem OAI.Erdos970.NumberTheoryLean.ActualThresholdArrival.actualHazard_bounds line 423