OAI/NumberTheory/Jacobsthal/Probability/GenuineMarkedVisit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.genuineMarkedVisitEvent line 15
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.genuineMarkedVisitEvent_measurable line 19
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenHit_ae_genuine line 23
4. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.genuineMarkedVisit_mass line 29
5. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.genuineMarkedVisit_exponential line 34
6. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.moving_genuine_marked_visit line 45