Corollary 1: Alon–Chung Contrapositive

Main Results

• incidentVertices: The set of vertices incident to a set of edges.
• alonChungContrapositive_direct: If E ⊆ X₁ is incident to at most γ|X₀| vertices, then |E| ≤ α|X₁|.
• alonChungContrapositive: If |E| > α|X₁|, then E is incident to more than γ|X₀| vertices.

Incident vertices of an edge set

def AlonChungContrapositive.incidentVertices {V : Type u_1} [Fintype V] [DecidableEq V] (E : Finset (Sym2 V)) : Finset V

The set of vertices incident to a set of edges E ⊆ X₁: Γ(E) = {v ∈ X₀ | ∃ e ∈ E, v ∈ e}.

Equations

• AlonChungContrapositive.incidentVertices E = {v : V | ∃ e ∈ E, v ∈ e}

theorem AlonChungContrapositive.mem_incidentVertices {V : Type u_1} [Fintype V] [DecidableEq V] (E : Finset (Sym2 V)) (v : V) : v ∈ incidentVertices E ↔ ∃ e ∈ E, v ∈ e

theorem AlonChungContrapositive.incidentVertices_nonempty {V : Type u_1} [Fintype V] [DecidableEq V] (E : Finset (Sym2 V)) (h : ∃ e ∈ E, ∃ (v : V), v ∈ e) : (incidentVertices E).Nonempty

theorem AlonChungContrapositive.subset_inducedEdges_incidentVertices {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (E : Finset (Sym2 V)) (hE : E ⊆ G.edgeFinset) : E ⊆ AlonChung.inducedEdges G (incidentVertices E)

Edges whose both endpoints lie in incidentVertices E include E.

Monotonicity of f(t) = t² + (λ₂/s) t(1-t)

theorem AlonChungContrapositive.alpha_mono {c : ℝ} (hc0 : 0 ≤ c) (hc1 : c ≤ 1) {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) : a ^ 2 + c * a * (1 - a) ≤ b ^ 2 + c * b * (1 - b)

The function f(t) = t² + c·t·(1-t) = (1-c)t² + c·t is non-decreasing on [0,∞) when 0 ≤ c ≤ 1.

Direct form: incident to at most γ|V| vertices implies |E| ≤ α|X₁|

theorem AlonChungContrapositive.alonChungContrapositive_direct {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hs : 1 ≤ s) (hreg : G.IsRegularOfDegree s) (hcard : 2 ≤ Fintype.card V) (E : Finset (Sym2 V)) (hE : E ⊆ G.edgeFinset) (γ : ℝ) (hγ0 : 0 < γ) (hγ1 : γ < 1) (lam₂ : ℝ) (hlam₂ : lam₂ = GraphExpansion.secondLargestEigenvalue G hcard) (hlam₂_nn : 0 ≤ lam₂) (hincident : ↑(incidentVertices E).card ≤ γ * ↑(Fintype.card V)) : ↑E.card ≤ (γ ^ 2 + lam₂ / ↑s * γ * (1 - γ)) * ↑G.edgeFinset.card

Alon–Chung Contrapositive (direct form). If E ⊆ X₁ is incident to at most γ|X₀| vertices, then |E| ≤ α|X₁| where α = γ² + (λ₂/s)γ(1-γ).

theorem AlonChungContrapositive.alonChungContrapositive {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hs : 1 ≤ s) (hreg : G.IsRegularOfDegree s) (hcard : 2 ≤ Fintype.card V) (E : Finset (Sym2 V)) (hE : E ⊆ G.edgeFinset) (γ : ℝ) (hγ0 : 0 < γ) (hγ1 : γ < 1) (lam₂ : ℝ) (hlam₂ : lam₂ = GraphExpansion.secondLargestEigenvalue G hcard) (hlam₂_nn : 0 ≤ lam₂) (hE_large : ↑E.card > (γ ^ 2 + lam₂ / ↑s * γ * (1 - γ)) * ↑G.edgeFinset.card) : ↑(incidentVertices E).card > γ * ↑(Fintype.card V)

Alon–Chung Contrapositive. If |E| > α|X₁|, then E is incident to more than γ|X₀| vertices.