OAI/NumberTheory/Jacobsthal/Estimates/SourceEdgeClasses.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosInverseCRT.product_density line 12
2. theorem OAI.Erdos970.ErdosInverseCRT.slopeCell_normalized_upper line 17
3. theorem OAI.Erdos970.ErdosInverseCRT.sampledSlopes_card_upper line 35
4. def OAI.Erdos970.ErdosInverseCRT.sourceEdgeResidue line 63
5. def OAI.Erdos970.ErdosInverseCRT.sourceCoefficient line 68
6. def OAI.Erdos970.ErdosInverseCRT.sourceShift line 71
7. theorem OAI.Erdos970.ErdosInverseCRT.sourceEdgeResidue_eq_affine line 75
8. theorem OAI.Erdos970.ErdosInverseCRT.sourceEdgeResidue_of_same_cell line 82
9. theorem OAI.Erdos970.ErdosInverseCRT.source_progression_edge_hit line 92
10. def OAI.Erdos970.ErdosInverseCRT.sourceTestedSlopes line 101
11. theorem OAI.Erdos970.ErdosInverseCRT.sourceTestedSlopes_eq_sampledSlopes line 107