OAI/NumberTheory/Jacobsthal/Estimates/RawInitialPacking.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Erdos970.Erdos970Dependency.MarkedVisits.RawInitialPackedTrace line 16
2. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.packRawInitialEven line 18
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.packRawInitialEven_measurable line 22
4. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.packedInitialKernel line 29
5. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.packedInitialKernel_isFiniteKernel line 32
6. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.packedInitialEndpoint line 36
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.packedInitialEndpoint_measurable line 39
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.packedInitialEndpoint_pack line 44
9. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.packedInitial_endpoint_law line 50
10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.packedInitial_ae_regeneration line 59
11. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.packedInitial_mass_one line 67