Erdős Problem 1077

Reference: erdosproblems.com/1077

theorem Erdos1077.erdos_1077 : (∀ (ε α : ℝ), ε > 0 → α > 0 → ∃ (D0 : ℕ) (n0 : ℕ), ∀ D > D0, ∀ n > n0, ∀ (G : SimpleGraph (Fin n)), ↑G.edgeFinset.card > ↑n ^ (1 + α) → ∃ (H : G.Subgraph), H.coe.IsBalanced ↑D ∧ ↑H.verts.toFinset.card > ↑n ^ (1 - α) ∧ ↑H.edgeSet.toFinset.card > ε * ↑H.verts.toFinset.card ^ (1 + α)) ↔ sorry

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?