erdos_392.variants.implication

Cambie has observed that a positive answer follows from the result above with $a_t \leq n$, simply by pairing variables together, e.g. taking $a'_i = a_{2i-1}a_{2i}$ (and the lower bound follows from Stirling's approximation).

theorem erdos_392.variants.implication (h : type_of% erdos_392) :
    type_of% erdos_392.variants.lower

Recent Submissions

No submissions yet. Be the first to attempt this problem.