Erdős Problem 1077

Reference: erdosproblems.com/1077

theorem Erdos1077.erdos_1077 : False ↔ ∀ ε > 0, ε < 1 → ∀ α > 0, α < 1 → ∀ᶠ (D : ℝ) in Filter.atTop, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), ↑G.edgeSet.ncard > ↑n ^ (1 + α) → ∃ (H : G.Subgraph), H.coe.IsBalanced D ∧ ↑H.verts.ncard > ↑n ^ (1 - α) ∧ ↑H.edgeSet.ncard > ε * ↑H.verts.ncard ^ (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?