OAI/NumberTheory/Jacobsthal/Estimates/SourceInitialDiscard.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosInverseCells.discard_coefficient_bound line 13
2. theorem OAI.Erdos970.ErdosInverseCells.subset_weight_spread line 42
3. theorem OAI.Erdos970.ErdosInverseCells.discarded_weight_bound line 60
4. def OAI.Erdos970.ErdosInverseCells.initialDiscarded line 86
5. theorem OAI.Erdos970.ErdosInverseCells.source_initial_discard_power line 90
6. theorem OAI.Erdos970.ErdosInverseCells.source_initial_discard_small line 122