OAI/NumberTheory/Jacobsthal/Paths/FiniteVisitMass.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Erdos970.Erdos970Dependency.MarkedVisits.FiniteRawHistory line 15
  2. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.selectedVisitPrefix line 17
  3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.selectedVisitPrefix_measurable line 20
  4. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawVisitPrefix line 27
  5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawVisitPrefix_measurable line 30
  6. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.finiteRawLast line 33
  7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.finiteRawLast_measurable line 35
  8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawVisitPrefix_length line 40
  9. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawVisitPrefix_last line 45
  10. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawVisitPrefixKernel line 53
  11. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawVisitPrefixKernel_isFiniteKernel line 56
  12. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawVisitPrefix_mass line 60
  13. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawVisitPrefix_mass_eq_ordinaryHit line 64
  14. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawVisitPrefix_last_law line 69
  15. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.finiteRawPrevious line 90
  16. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.finiteRawPrevious_measurable line 93
  17. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.finiteRawLength_measurable line 99
  18. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawVisitPrefix_previous line 104
  19. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenHitAnchor_cost line 112
  20. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.finiteSuppliedPast line 117
  21. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.finiteSuppliedPast_measurable line 120
  22. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.selectedVisitPrefix_past line 125
  23. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawVisitPrefix_ae_past line 131
  24. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.finitePrefixSourceEvent line 139
  25. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.finitePrefixSourceEvent_measurable line 145
  26. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawVisitPrefix_ae_source line 154
  27. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawVisitPrefix_witness_mass line 169
  28. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.finitePrefixSourceEvent_even_witness line 189
  29. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.visitHorizonEvent line 197
  30. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.visitHorizonEvent_measurable line 200
  31. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.finite_visit_horizon_mass line 205
  32. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.finite_visit_exponential line 224
  33. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.moving_finite_visit line 235