OAI/Combinatorics/Progressions/Estimates/BoundedNativeDependentApproximations.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.fourSparseAnchorChange line 16
2. theorem OAI.Erdos3.exists_simultaneous_four_point_anchors line 32
3. structure OAI.Erdos3.NativeRankRelation.CommonData.SparseAnchors line 107
4. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_sparse_anchors line 117
5. theorem OAI.Erdos3.NativeRankRelation.CommonData.SparseAnchors.shifts_subset line 133
6. theorem OAI.Erdos3.NativeRankRelation.CommonData.SparseAnchors.anchors_mem line 139
7. theorem OAI.Erdos3.NativeRankRelation.CommonData.SparseAnchors.partners_mem line 150
8. theorem OAI.Erdos3.NativeRankRelation.CommonData.SparseAnchors.exists_anchor_representative_corrections line 179
9. def OAI.Erdos3.NativeDegreeRankFamily.nativeCoefficientCoordinates line 262
10. theorem OAI.Erdos3.NativeRankRelation.CommonData.native_scaled_correction line 282
11. theorem OAI.Erdos3.NativeRankRelation.CommonData.SparseAnchors.exists_native_sparse_approximations line 347
12. theorem OAI.Erdos3.NativeRankRelation.CommonData.SparseAnchors.exists_native_dependent_approximations line 416
13. theorem OAI.Erdos3.NativeRankRelation.CommonData.SparseAnchors.exists_bounded_native_dependent_approximations line 511