Erdős problem 1077 · problems.science

We call a graph $D$ -balanced (or $D$ -almost-regular) if the maximum degree is at most $D$ times the minimum degree.

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1077.lean

Retained formal statement1 of 1

We call a graph $D$ -balanced (or $D$ -almost-regular) if the maximum degree is at most $D$ times the minimum degree.

Let $ε, α > 0$ and $D$ and $n$ be sufficiently large. If $G$ is a graph on $n$ vertices with at least $n^{1+α}$ edges, then must $G$ contain a $D$ -balanced subgraph on $m > n^{1-α}$ vertices with at least $εm^{1+α}$ edges?

FormalConjectures/ErdosProblems/1077.leanErdos1077.erdos_107711 linesExact file

1False ↔2  ∀ ε > 0,3    ε < 1 →4      ∀ α > 0,5        α < 1 →6          ∀ᶠ (D : ℝ) in Filter.atTop,7            ∀ᶠ (n : ℕ) in Filter.atTop,8              ∀ (G : SimpleGraph (Fin n)),9                ↑G.edgeSet.ncard > ↑n ^ (1 + α) →10                  ∃ H,11                    H.coe.IsBalanced D ∧ ↑H.verts.ncard > ↑n ^ (1 - α) ∧ ↑H.edgeSet.ncard > ε * ↑H.verts.ncard ^ (1 + α)

SolvedStatement only, no proof

Sources

Search problems.science