Balanced subgraphs

DefinitionBalanced graph#✓fully proved

Let \(G\) be a finite simple graph and \(D\) a real number. The graph \(G\) is \(D\)-balanced if its maximum degree \(\Delta(G)\) is at most \(D\) times its minimum degree \(\delta(G)\), that is, \(\Delta(G) \le D \cdot \delta(G)\).

def IsBalanced (G : SimpleGraph V) (D : ℝ) [DecidableRel G.Adj] : Prop :=
  G.maxDegree ≤ D * G.minDegree

Used by 1

Used byErdős–Simonovits balanced subgraph claim

DefinitionErdős–Simonovits balanced subgraph claim#✓fully proved

For all reals \(\varepsilon\) and \(\alpha\) with \(0 < \varepsilon < 1\) and \(0 < \alpha < 1\), for all sufficiently large real \(D\) and then all sufficiently large \(n\), every simple graph \(G\) on the vertex set \(\{0, \dots, n-1\}\) with more than \(n^{1+\alpha}\) edges has a (not necessarily induced) subgraph \(H\) with some number \(m\) of vertices such that \(H\) is \(D\)-balanced (its maximum degree is at most \(D\) times its minimum degree), \(m > n^{1-\alpha}\), and \(H\) has more than \(\varepsilon m^{1+\alpha}\) edges.

This claim (Erdős Problem 1077) is false.

def mainPositive : Prop :=
  ∀ ε > (0 : ℝ), ε < 1 → ∀ α > (0 : ℝ), α < 1 → ∀ᶠ D in atTop, ∀ᶠ n in atTop,
    ∀ G : SimpleGraph (Fin n), G.edgeSet.ncard > (n : ℝ) ^ (1 + α) →
      ∃ (H : SimpleGraph.Subgraph G),
        letI m := H.verts.ncard
        SimpleGraph.IsBalanced H.coe D ∧
        m > (n : ℝ) ^ (1 - α) ∧
        H.edgeSet.ncard > ε * m ^ (1 + α)

Uses 1 · Used by 2

Statement usesBalanced graph

Used byNegation of the Erdős–Simonovits balanced subgraph claim · The Erdős–Simonovits balanced subgraph claim is false

DefinitionNegation of the Erdős–Simonovits balanced subgraph claim#✓fully proved

The proposition that the Erdős–Simonovits balanced subgraph claim fails, that is, that it is not the case that for all reals \(\varepsilon\) and \(\alpha\) with \(0 < \varepsilon < 1\) and \(0 < \alpha < 1\), for all sufficiently large real \(D\) and then all sufficiently large \(n\), every simple graph \(G\) on the vertex set \(\{0, \dots, n-1\}\) with more than \(n^{1+\alpha}\) edges has a (not necessarily induced) subgraph \(H\) with some number \(m\) of vertices such that \(H\) is \(D\)-balanced (its maximum degree is at most \(D\) times its minimum degree), \(m > n^{1-\alpha}\), and \(H\) has more than \(\varepsilon m^{1+\alpha}\) edges.

def disprovedMain : Prop := ¬ mainPositive

Uses 1

Statement usesErdős–Simonovits balanced subgraph claim

TheoremThe Erdős–Simonovits balanced subgraph claim is false#●ready to prove

It is not the case that for all reals \(\varepsilon\) and \(\alpha\) with \(0 < \varepsilon < 1\) and \(0 < \alpha < 1\), for all sufficiently large real \(D\) and then all sufficiently large \(n\), every simple graph \(G\) on the vertex set \(\{0, \dots, n-1\}\) with more than \(n^{1+\alpha}\) edges has a (not necessarily induced) subgraph \(H\) with some number \(m\) of vertices such that \(H\) is \(D\)-balanced (its maximum degree is at most \(D\) times its minimum degree), \(m > n^{1-\alpha}\), and \(H\) has more than \(\varepsilon m^{1+\alpha}\) edges.

The disproof uses a bipartite witness: the requirement \(m > n^{1-\alpha}\) is too strong, and the correct order is \(n^{\alpha}\) per Jun Gao and Jiang–Longbrake [JiLo25], per erdosproblems.com/1077.

public theorem_wanted mainPositive_refuted : ¬ mainPositive

Sources

• External Lean disproof of Erdos Problem 1077, plby/lean-proofs, https://github.com/plby/lean-proofs/blob/dfe2d78128b493c572cf525b1b8edf4897fb7664/src/latest/ErdosProblems/Erdos1077.lean#L265.

Uses 1

Statement usesErdős–Simonovits balanced subgraph claim

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.