Formal target: Corpus.Erdos563.erdos_563

Let $F(n,\alpha)$ denote the smallest $m$ such that there exists a $2$-colouring of the edges of $K_n$ so that every $X\subseteq [n]$ with $\lvert X\rvert\geq m$ contains more than $\alpha \binom{\lvert X\rvert}{2}$ many edges of each colour.

Exact formal statement

∀ (α : Real),
  LE.le.{0} 0 α →
    LT.lt.{0} α (1 / 2) →
      Exists.{1} fun c =>
        And (LT.lt.{0} 0 c)
          (Filter.Tendsto.{0, 0}
            (fun n => HDiv.hDiv.{0, 0, 0} (Nat.cast.{0} (Corpus.Erdos563.F n α)) (Real.log (Nat.cast.{0} n)))
            Filter.atTop.{0} (nhds.{0} c))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record