OAI/NumberTheory/Jacobsthal/Estimates/RawReturnBound.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Erdos970.Erdos970Dependency.MarkedVisits.RawReturnTrace line 15
2. abbrev OAI.Erdos970.Erdos970Dependency.MarkedVisits.ReturnSignature line 16
3. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.packRawReturnTrace line 18
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnTrace_mk_measurable line 21
5. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnTraceKernel line 26
6. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnTraceKernel_isSFiniteKernel line 29
7. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnSignature line 33
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnSignature_measurable line 36
9. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceReturnSignature line 44
10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceReturnSignature_measurable line 47
11. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceReturnSignature_injective line 53
12. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnTerm_signature line 63
13. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnTrace_signature line 80
14. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnTrace_mass_one line 92
15. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.twoReturnHistory line 111
16. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.twoReturnHistory_isFiniteKernel line 115
17. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.twoReturnEvent line 119
18. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.twoReturnEvent_measurable line 125
19. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.twoReturnHistory_eq_cylinder line 131
20. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.twoReturnHistory_retains_past line 142
21. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.twoReturnHistoryWithFirsts line 148
22. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.twoReturnHistoryWithFirsts_apply line 157
23. abbrev OAI.Erdos970.Erdos970Dependency.MarkedVisits.RawTwoReturnTrace line 180
24. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.packRawTwoReturnTrace line 183
25. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.measurableSigmaMk line 187
26. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.packRawTwoReturnTrace_measurable line 190
27. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawTwoReturnTraceKernel line 194
28. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawTwoReturnTraceKernel_isSFiniteKernel line 198
29. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnTrace_mass_series line 202
30. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnTrace_mass_at_regeneration line 209
31. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawTwoReturnTrace_mass_series line 218
32. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawTwoReturnTrace_mass_conditioning line 228
33. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawTwoReturnTrace_mass_one line 242
34. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.fullPairCaptured_add_killed line 266
35. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.fullPairReturn_mass_step line 271
36. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.fullPairReturn_finite_mass line 282
37. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.fullPairReturn_total_mass_le line 293
38. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstReturnHistory_mass_full line 302
39. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnTrace_mass_le_one line 309
40. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturnTraceKernel_isFiniteKernel line 314