OAI/NumberTheory/Jacobsthal/Probability/RawEvenMarkedHit.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Erdos970.Erdos970Dependency.MarkedVisits.RawEvenMarkedHitTrace line 15
2. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenHitContinuation line 18
3. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenHitContinuation_isFiniteKernel line 23
4. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenMarkedHitKernel line 29
5. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenMarkedHitKernel_isFiniteKernel line 32
6. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenMarkedHit_mass line 36
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenMarkedHit_mass_le_one line 57
8. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenMarkedHit_exponential line 62
9. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.moving_raw_even_marked_hit line 73