Erdős Problem 82

Reference: erdosproblems.com/82

def Erdos82.IsRegularInduced {V : Type u_1} [Fintype V] {G : SimpleGraph V} (S : G.Subgraph) : Prop

A predicate that holds if $S$ is a regular induced subgraph of $G$

Equations

• Erdos82.IsRegularInduced S = (S.IsInduced ∧ ∃ (k : ℕ), S.coe.IsRegularOfDegree k)

noncomputable def Erdos82.F (n : ℕ) : ℕ

$F(n)$ is the maximal integer such that every graph on $n$ vertices contains a regular induced subgraph on at least $F(n)$ vertices.

Equations

• Erdos82.F n = sSup {k : ℕ | ∀ (G : SimpleGraph (Fin n)), ∃ (S : G.Subgraph), Erdos82.IsRegularInduced S ∧ k ≤ S.verts.ncard}

theorem Erdos82.erdos_82 : Filter.Tendsto (fun (n : ℕ) => ↑(F n) / Real.log ↑n) Filter.atTop Filter.atTop

$F(n) / \log n \to \infty as n \to \infty$

theorem Erdos82.erdos_82.variants.F_upper_bound : (fun (n : ℕ) => ↑(F n)) =O[Filter.atTop] fun (n : ℕ) => √↑n * Real.log ↑n ^ (3 / 4)

$F(n) \le O(n^{1/2} \ln ^ {3/4} n)$

Theorem 1.4 from [AKS07]

[AKS07] Alon, N. and Krivelevich, M. and Sudakov, B., Large nearly regular induced subgraphs. arXiv:0710.2106 (2007).