Formal target: Corpus.Erdos572.erdos_572
Show that for $k\geq 3$ $$\mathrm{ex}(n;C_{2k})\gg n^{1+\frac{1}{k}}.$$ This problem is #46 in Extremal Graph Theory in the graphs problem collection.
Exact formal statement
∀ (k : Nat),
LE.le.{0} 3 k →
Exists.{1} fun c =>
And (GT.gt.{0} c 0)
(Filter.Eventually.{0}
(fun n =>
LE.le.{0}
(HMul.hMul.{0, 0, 0} c
(HPow.hPow.{0, 0, 0} (Nat.cast.{0} n) (HAdd.hAdd.{0, 0, 0} 1 (HDiv.hDiv.{0, 0, 0} 1 (Nat.cast.{0} k)))))
(Nat.cast.{0} (SimpleGraph.extremalNumber.{0} n (SimpleGraph.cycleGraph (HMul.hMul.{0, 0, 0} 2 k)))))
Filter.atTop.{0})This target is a formal statement, not a proof of the problem.
Environment availability: available.