Formal target: Corpus.Erdos571.erdos_571

Show that for any rational $\alpha \in [1,2)$ there exists a bipartite graph $G$ such that $$\mathrm{ex}(n;G)\asymp n^{\alpha}.$$

Exact formal statement

∀ (α : Rat),
  LE.le.{0} 1 α →
    LT.lt.{0} α 2 →
      Exists.{1} fun q =>
        Exists.{1} fun G =>
          And (SimpleGraph.IsBipartite.{0} G)
            (Asymptotics.IsTheta.{0, 0, 0} Filter.atTop.{0} (fun n => Nat.cast.{0} (SimpleGraph.extremalNumber.{0} n G))
              fun n => HPow.hPow.{0, 0, 0} (Nat.cast.{0} n) (Rat.cast.{0} α))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record