Erdős Problem #713

The question

erdos_713.parts.i. Is it true that, for every bipartite graph $G$, there exists some $\alpha \in [1,2)$ and $c>0$ such that $$\mathrm{ex}(n;G)\sim c{n}^{\alpha }?$$

The condition that $G$ have at least two edges excludes degenerate forbidden graphs whose extremal number is eventually zero, for which the displayed asymptotic with $c>0$ is impossible.

erdos_713.parts.ii. Must $\alpha$ be rational?

The same nondegeneracy condition on $G$ is used as in part (i). Rationality means that the real number $\alpha$ lies in the image of the canonical embedding $\mathbb{Q}\to \mathbb{R}$.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.ErdosProblems.«713» (2 statements). answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

theorem erdos_713.parts.i : answer(sorry) ↔
    ∀ (q : ℕ) (G : SimpleGraph (Fin q)), G.IsBipartite → 2 ≤ G.edgeFinset.card →
      ∃ α c : ℝ, α ∈ Set.Ico 1 2 ∧ 0 < c ∧
        Asymptotics.IsEquivalent atTop
          (fun n : ℕ => (extremalNumber n G : ℝ))
          (fun n : ℕ => c * (n : ℝ) ^ α)

theorem erdos_713.parts.ii : answer(sorry) ↔
    ∀ (q : ℕ) (G : SimpleGraph (Fin q)), G.IsBipartite → 2 ≤ G.edgeFinset.card →
      ∀ α c : ℝ, α ∈ Set.Ico 1 2 → 0 < c →
        Asymptotics.IsEquivalent atTop
          (fun n : ℕ => (extremalNumber n G : ℝ))
          (fun n : ℕ => c * (n : ℝ) ^ α) →
        α ∈ Set.range ((↑) : ℚ → ℝ)

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already — check erdosproblems.com/713. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• erdosproblems.com/713
• [Er67d] Erdős, P., Some recent results on extremal problems in graph theory. {R}esults. (1967), 117--123 (English); pp. 124--130 (French).
• [ErSi70] Erdős, P. and Simonovits, M., Some extremal problems in graph theory. Combinatorial theory and its applications, I-III (Proc. Colloq., Balatonfüred, 1969) (1970), 377-390.
• [FrFu87] Frankl, P. and Füredi, Z., Exact solution of some Turán-type problems. J. Combin. Theory Ser. A (1987), 226--262.
• [FuGe21] Füredi, Zoltán and Gerbner, Dániel, Hypergraphs without exponents. J. Combin. Theory Ser. A (2021), Paper No. 105517, 9.

Source and licence

Imported from Formal Conjectures (Erdős problems), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.