OAI/NumberTheory/Jacobsthal/Paths/CanonicalUniformMissingVisit.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.oddConsecutiveContinue_power_embed line 16
2. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.consecutiveMarkedHit_odd_mass line 23
3. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.consecutiveMarkedHit_after_regeneration line 38
4. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.canonicalEvenPairVisitKernel line 56
5. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.canonicalEvenPairVisitKernel_isFiniteKernel line 59
6. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.canonicalEvenPairVisit_completion line 63
7. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.canonicalEvenPairVisit_mass line 71
8. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.canonicalEvenPairVisit_exponential line 84
9. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.moving_canonical_even_visit line 95
10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.extendFinitePrefix_total line 121
11. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.canonicalEvenPairVisit_bounded_mass line 132
12. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.finite_history_length_exhausts line 138
13. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.canonical_even_hit_probability_limit line 150
14. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.finitePathMeasure_marked_hit_limit line 158
15. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.pair_no_future_hit_of_bad_inputs line 175
16. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.regeneration_ratio_le_three line 192
17. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.eligible_input_large_exponent line 198
18. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.low_gap_no_future_pair_hit line 209
19. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.cutoff_no_future_pair_hit line 225
20. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.closedNoHitEvent line 259
21. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.closedNoHitEvent_measurable line 263
22. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.closedNoHitEvent_future line 271
23. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.closedNoHitEvent_mass_future line 280
24. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.canonical_closed_nohit_le_failure line 309
25. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.canonical_closed_nohit_exponential line 342
26. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.moving_cutoff_one line 356
27. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.moving_canonical_missing_visit line 371