OAI/Combinatorics/Progressions/Estimates/ComparableUnconditionedScalarFamily.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.canonicalScalarFamily_apply line 12
2. theorem OAI.Erdos3.canonicalScalarFamily_apply_with line 70
3. def OAI.Erdos3.CanonicalUnconditionedScalarFamilyStatement line 136
4. theorem OAI.Erdos3.exists_canonical_unconditioned_scalar_family line 182
5. def OAI.Erdos3.ComparableUnconditionedScalarProductiveFamilyStatement line 210
6. theorem OAI.Erdos3.exists_comparable_unconditioned_scalar_productive_family line 258
7. theorem OAI.Erdos3.exists_dyadic_unconditioned_scalar_productive_family line 279
8. def OAI.Erdos3.ComparableUnconditionedScalarFamilyStatement line 299
9. theorem OAI.Erdos3.exists_comparable_unconditioned_scalar_family line 345
10. theorem OAI.Erdos3.exists_dyadic_unconditioned_scalar_family line 360