Formal target: Corpus.Erdos865.erdos_865.variants.sos

Erdős and Sós conjectured that $f_k(N)\sim \frac{1}{2}\left(1+\sum_{1\leq r\leq k-2}\frac{1}{4^r}\right) N$, where $f_k(N)$ is the minimal size of a subset of $\{1, \dots, N\}$ guaranteeing $k$ elements have all pairwise sums in the set.

Exact formal statement

∀ (k : Nat),
  LE.le.{0} 2 k →
    Asymptotics.IsEquivalent.{0, 0} Filter.atTop.{0} (fun N => Nat.cast.{0} (Corpus.Erdos865.f N k)) fun N =>
      HMul.hMul.{0, 0, 0}
        (HMul.hMul.{0, 0, 0} (1 / 2)
          (HAdd.hAdd.{0, 0, 0} 1
            (Finset.sum.{0, 0} (Finset.Icc.{0} 1 (HSub.hSub.{0, 0, 0} k 2)) fun r => HPow.hPow.{0, 0, 0} (1 / 4) r)))
        (Nat.cast.{0} N)

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record