Erdős Problem #571: rational exponents for bipartite Turán numbers

For every rational $\alpha$ satisfying $$1\le\alpha<2,$$ the Lean theorem constructs some finite $q$ and a bipartite graph $$G:\operatorname{SimpleGraph}(\operatorname{Fin} q)$$ such that $$\operatorname{ex}(n;G)=\Theta(n^\alpha)$$ as $n\to\infty$. This resolves the single-graph rational-exponents conjecture. Earlier work of Bukh and Conlon proved the corresponding statement only for a finite family of forbidden bipartite graphs, and subsequent work realized many large classes of individual rational exponents. Astra's theorem covers every rational $\alpha\in[1,2)$ with one forbidden graph for each exponent.

For every rational $\alpha$ satisfying $$1\le\alpha<2,$$ the Lean theorem constructs some finite $q$ and a bipartite graph $$G:\operatorname{SimpleGraph}(\operatorname{Fin} q)$$ such that $$\operatorname{ex}(n;G)=\Theta(n^\alpha)$$ as $n\to\infty$. This resolves the single-graph rational-exponents conjecture. Earlier work of Bukh and Conlon proved the corresponding statement only for a finite family of forbidden bipartite graphs, and subsequent work realized many large classes of individual rational exponents. Astra's theorem covers every rational $\alpha\in[1,2)$ with one forbidden graph for each exponent.