OAI/NumberTheory/Jacobsthal/Estimates/SourceRichPoints.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosInverseTail.commonParentLength_le_ratio line 12
2. theorem OAI.Erdos970.ErdosInverseTail.strict_deviation_transfer line 22
3. theorem OAI.Erdos970.ErdosInverseTail.source_bad_edge_implies_frozen line 44
4. theorem OAI.Erdos970.ErdosInverseRefinement.selectedRow_subset_nonstructured line 116
5. theorem OAI.Erdos970.ErdosInverseRefinement.rich_points_incidence line 133
6. theorem OAI.Erdos970.ErdosInverseRefinement.source_parentSlope_mem line 166
7. theorem OAI.Erdos970.ErdosInverseRefinement.source_rich_points line 243