OAI/Combinatorics/Progressions/Linear/ShiftFailurePositiveBasis.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.positive_basis_error_bound line 11
2. theorem OAI.Erdos3.exists_positive_basis_precision line 31
3. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.exists_quantitative_positive_basis line 70
4. theorem OAI.Erdos3.positive_violation_of_norm_sub_le line 114
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_common_positive_basis line 126
6. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_common_model_positive_basis line 227
7. structure OAI.Erdos3.PositiveShiftBasis line 342
8. theorem OAI.Erdos3.PositiveShiftBasis.exists_adapted line 399
9. def OAI.Erdos3.PositiveShiftBasis.mono line 460
10. def OAI.Erdos3.PositiveShiftBasis.testingFamily line 509
11. theorem OAI.Erdos3.PositiveShiftBasis.testingFamily_of_mem line 514
12. theorem OAI.Erdos3.PositiveShiftBasis.testingFamily_norm_le line 519
13. theorem OAI.Erdos3.PositiveShiftBasis.exists_fixed_partners line 527
14. theorem OAI.Erdos3.exists_positive_basis_of_shift_failure line 577