OAI/Combinatorics/Progressions/Estimates/CorrelatingVerticalPair.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_weighted_common_factor line 12
2. structure OAI.Erdos3.NativePairPartition line 112
3. def OAI.Erdos3.NativePairPartition.mono line 134
4. theorem OAI.Erdos3.exists_antisymmetric_pair_precise_partition line 147
5. theorem OAI.Erdos3.NativePairPartition.exists_correlating_anchor line 244
6. def OAI.Erdos3.NativePolynomialOrbitFactors.HasCorrelatingAnchor line 302
7. theorem OAI.Erdos3.NativePolynomialOrbitFactors.hasCorrelatingAnchor_mono line 317
8. theorem OAI.Erdos3.exists_antisymmetric_pair_correlating_anchor line 329
9. theorem OAI.Erdos3.exists_common_anchor_approximation line 422
10. def OAI.Erdos3.NativePolynomialOrbitFactors.HasVerticalCorrelatingAnchor line 555
11. theorem OAI.Erdos3.exists_correlating_vertical_pair line 581