571.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/571
Formal Lean proof
[BuCo18] Bukh, Boris and Conlon, David, Rational exponents in extremal graph theory. J. Eur. Math. Soc. (JEMS) (2018), 1747-1757.
[CJL21] Conlon, David and Janzer, Oliver and Lee, Joonkyung, More on the extremal number of subdivisions. Combinatorica (2021), 465-494.
[CoJa22] Conlon, David and Janzer, Oliver, Rational exponents near two. Adv. Comb. (2022), Paper No. 9, 10.
[Er78] Erdős, Paul, Problems and results in combinatorial analysis and combinatorial number theory. Proceedings of the Ninth Southeastern Conference on Combinatorics, Graph Theory, and Computing (Florida Atlantic Univ., Boca Raton, Fla., 1978) (1978), 29-40.
[JJM20] Jiang, Tao and Jiang, Zilin and Ma, Jie, Negligible obstructions and Turán exponents. arXiv:2007.02975 (2020).
[JMY22] Jiang, Tao and Ma, Jie and Yepremyan, Liana, On Turán exponents of bipartite graphs. Combin. Probab. Comput. (2022), 333-344.
[JiQi20] Jiang, Tao and Qiu, Yu, Turán numbers of bipartite subdivisions. SIAM J. Discrete Math. (2020), 556-570.
[JiQi23] Jiang, Tao and Qiu, Yu, Many Turán exponents via subdivisions. Combin. Probab. Comput. (2023), 134-150.
[KKL21] Kang, Dong Yeap and Kim, Jaehoon and Liu, Hong, On the rational Turán exponents conjecture. J. Combin. Theory Ser. B (2021), 149-172.

Imports (1)

theorem Erdos571.erdos_571 sorry line 61 source
depends on sorry what this means
Statement uses: Rat, LE.le, OfNat.ofNat, LT.lt, Exists, Nat, SimpleGraph, Fin, And, SimpleGraph.IsBipartite, Asymptotics.IsTheta, Real, Filter.atTop, SimpleGraph.extremalNumber, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
23 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.