OAI/Combinatorics/Progressions/Estimates/ComparableUnconditionedScalarTransfer.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.comparableScalarProductivityCutoff_le_exp line 11
2. theorem OAI.Erdos3.comparableScalarProductivitySize line 109
3. theorem OAI.Erdos3.exists_comparableScalarGeometryTransfer line 140
4. def OAI.Erdos3.ComparableUnconditionedScalarProductiveTransferStatement line 216
5. theorem OAI.Erdos3.exists_comparable_unconditioned_scalar_productive_transfer line 258
6. def OAI.Erdos3.ComparableUnconditionedScalarTransferStatement line 333
7. theorem OAI.Erdos3.exists_comparable_unconditioned_scalar_transfer line 373