FormalConjectures/ErdosProblems/713.lean
Explanation legend Lean4 Domain Explanation Language (L4DEL)
L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.
- L4DEL
- Lean4 Domain Explanation Language
Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.
Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1
2 declarations, 2 contain sorry, 0 declared as axioms
Erdős Problem 713
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.
Imports (1)
- theorem
Erdos713.erdos_713.parts.iIs it true that, for every bipartite graph sorry line 49 sourceSource documentation
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 cn^\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.
depends on sorry what this means
Statement uses:
Iff,True,Nat,SimpleGraph,Fin,SimpleGraph.IsBipartite,LE.le,OfNat.ofNat,Finset.card,Sym2,SimpleGraph.edgeFinset,Classical.propDecidable,SimpleGraph.Adj,Exists,Real,And,Membership.mem,Set,Set.Ico,LT.ltand 5 moreProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous54 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
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 : ℝ) ^ α) := by …Mentions: c
- theorem
Erdos713.erdos_713.parts.iiMust $\alpha$ be rational? sorry line 65 sourceSource documentation
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}$.
depends on sorry what this means
Statement uses:
Iff,True,Nat,SimpleGraph,Fin,SimpleGraph.IsBipartite,LE.le,OfNat.ofNat,Finset.card,Sym2,SimpleGraph.edgeFinset,Classical.propDecidable,SimpleGraph.Adj,Real,Membership.mem,Set,Set.Ico,LT.lt,Asymptotics.IsEquivalent,Filter.atTopand 5 moreProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous58 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
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 ((↑) : ℚ → ℝ) := by …Mentions: c