OAI/NumberTheory/Jacobsthal/Estimates/FiniteSampleSpace.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Erdos970.ErdosInverseSampling.Sample line 12
2. def OAI.Erdos970.ErdosInverseSampling.goodSamples line 14
3. def OAI.Erdos970.ErdosInverseSampling.goodSampleEquiv line 18
4. theorem OAI.Erdos970.ErdosInverseSampling.sample_card line 47
5. theorem OAI.Erdos970.ErdosInverseSampling.goodSamples_card line 52
6. def OAI.Erdos970.ErdosInverseSampling.sampleFrequency line 58
7. theorem OAI.Erdos970.ErdosInverseSampling.sampleFrequency_eq line 61