OAI/NumberTheory/Jacobsthal/Paths/SampleWitnessAverage.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosInverseSampling.many_large_weights line 14
2. def OAI.Erdos970.ErdosInverseSampling.witnessPairs line 33
3. theorem OAI.Erdos970.ErdosInverseSampling.witnessPairs_card line 37
4. def OAI.Erdos970.ErdosInverseSampling.selectedPairs line 52
5. def OAI.Erdos970.ErdosInverseSampling.selectedFraction line 56
6. theorem OAI.Erdos970.ErdosInverseSampling.goodSamples_filter line 60
7. theorem OAI.Erdos970.ErdosInverseSampling.sample_incidence_average_eq line 66
8. theorem OAI.Erdos970.ErdosInverseSampling.sample_incidence_average_lower line 83