OAI/Combinatorics/Progressions/Estimates/CanonicalUnconditionedScalarTransfer.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_unconditioned_joint_scalar_transfer line 18
2. theorem OAI.Erdos3.exists_unconditioned_trimmed_scalar_transfer line 121
3. theorem OAI.Erdos3.exists_unconditioned_trimmed_threshold_transfer line 230
4. theorem OAI.Erdos3.exists_canonicalScalarTailApplication line 320
5. theorem OAI.Erdos3.exists_comparableScalarSliceGeometryTransfer line 436
6. theorem OAI.Erdos3.exists_comparableScalarTailApplication line 548
7. theorem OAI.Erdos3.exists_canonicalScalarGeometryTransfer line 665
8. def OAI.Erdos3.CanonicalUnconditionedScalarTransferStatement line 741
9. theorem OAI.Erdos3.exists_canonical_unconditioned_scalar_transfer line 781