OAI/Combinatorics/Progressions/Estimates/MarkedEvaluationJointBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.markedShiftBasis_structure_height line 20
2. def OAI.Erdos3.markedQuotientHeight line 60
3. theorem OAI.Erdos3.exists_markedShiftQuotient_bounded_data line 80
4. def OAI.Erdos3.markedQuotientFrequencyHeight line 141
5. theorem OAI.Erdos3.exists_markedShiftQuotient_bounded_frequency_data line 159
6. theorem OAI.Erdos3.exists_markedShiftQuotient_bounded_direction_data line 258
7. def OAI.Erdos3.markedEvaluationHeight line 356
8. theorem OAI.Erdos3.exists_markedShiftQuotient_bounded_evaluation_data line 373