OAI/NumberTheory/Jacobsthal/Probability/PhysicalMarkedRecord.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.recordFirst line 16
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.recordFirst_measurable line 17
3. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.physicalMarkedRecord line 20
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.physicalMarkedRecord_measurable line 24
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.source_record_physical line 30
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.physicalMarkedRecord_witness line 34
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceRecord_ae_physical line 46
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceLastRecord_ae_physical line 55
9. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.hitWordEvent_last_cost line 61