CoreGapPrune

Pruning a set of edges

noncomputable def Nibble.AX1.prune {V : Type} [DecidableEq V] (T : SimpleGraph V) (Bad : Finset (Finset V)) : SimpleGraph V

The subgraph of T obtained by deleting the edges lying in Bad.

Equations

• Nibble.AX1.prune T Bad = Nibble.AX1.edgeSelect T fun (e : Finset V) => e ∉ Bad

@[instance_reducible]

noncomputable instance Nibble.AX1.instDecidableRelPrune {V : Type} [DecidableEq V] (T : SimpleGraph V) (Bad : Finset (Finset V)) : DecidableRel (prune T Bad).Adj

Equations

• Nibble.AX1.instDecidableRelPrune T Bad x✝¹ x✝ = Classical.dec ((Nibble.AX1.prune T Bad).Adj x✝¹ x✝)

theorem Nibble.AX1.prune_le {V : Type} [DecidableEq V] (T : SimpleGraph V) (Bad : Finset (Finset V)) : prune T Bad ≤ T

theorem Nibble.AX1.prune_adj {V : Type} [DecidableEq V] (T : SimpleGraph V) (Bad : Finset (Finset V)) (x y : V) : (prune T Bad).Adj x y ↔ T.Adj x y ∧ {x, y} ∉ Bad

def Nibble.AX1.deletedDegree {V : Type} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj] (Bad : Finset (Finset V)) (v : V) : ℕ

The number of deleted edges at a vertex.

Equations

• Nibble.AX1.deletedDegree T Bad v = {z : V | T.Adj v z ∧ {v, z} ∈ Bad}.card

The triangle degree lost by pruning

theorem Nibble.AX1.edgeTriangleDegree_prune_ge {V : Type} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj] (Bad : Finset (Finset V)) {x y : V} (hadj : (prune T Bad).Adj x y) : edgeTriangleDegree T {x, y} ≤ edgeTriangleDegree (prune T Bad) {x, y} + deletedDegree T Bad x + deletedDegree T Bad y

Pruning costs a surviving edge at most the deleted degrees of its endpoints.

The handshake bound

theorem Nibble.AX1.sum_deletedDegree_le {V : Type} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj] (Bad : Finset (Finset V)) : ∑ v : V, deletedDegree T Bad v ≤ 2 * Bad.card

The total deleted degree is at most twice the number of deleted edges.

theorem Nibble.AX1.card_vertices_deletedDegree_gt {V : Type} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj] (Bad : Finset (Finset V)) {t : ℝ} : ↑{v : V | t < ↑(deletedDegree T Bad v)}.card * t ≤ 2 * ↑Bad.card

Markov's inequality for the deleted degrees.

theorem Nibble.AX1.card_edges_heavy_deleted_le {V : Type} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj] (Bad : Finset (Finset V)) {t : ℝ} (ht : 0 < t) : ↑{e ∈ T.cliqueFinset 2 | ¬∀ v ∈ e, ↑(deletedDegree T Bad v) ≤ t}.card ≤ 2 * ↑Bad.card / t * ↑(Fintype.card V)

Few edges have an endpoint at which many edges were deleted.

The pruned graph is near-regular with no exceptions above

theorem Nibble.AX1.mem_cliqueFinset_two_prune {V : Type} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj] (Bad : Finset (Finset V)) {e : Finset V} (he : e ∈ (prune T Bad).cliqueFinset 2) : e ∈ T.cliqueFinset 2 ∧ e ∉ Bad

Every edge of the pruned graph is an edge of T outside Bad.

theorem Nibble.AX1.prune_near_regular {V : Type} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj] (Bad : Finset (Finset V)) {μ d t : ℝ} (ht : 0 < t) (hhi : ∀ e ∈ T.cliqueFinset 2, e ∉ Bad → ↑(edgeTriangleDegree T e) ≤ (1 + μ) * d) (hlo : ∀ e ∈ T.cliqueFinset 2, e ∉ Bad → (1 - μ) * d ≤ ↑(edgeTriangleDegree T e)) : (∀ e ∈ (prune T Bad).cliqueFinset 2, ↑(edgeTriangleDegree (prune T Bad) e) ≤ (1 + μ) * d) ∧ ∃ (Exc : Finset (Finset V)), ↑Exc.card ≤ 2 * ↑Bad.card / t * ↑(Fintype.card V) ∧ ∀ e ∈ (prune T Bad).cliqueFinset 2, e ∉ Exc → (1 - μ) * d - 2 * t ≤ ↑(edgeTriangleDegree (prune T Bad) e)

The pruned graph. If the triangle degrees of T are between (1−μ)d and (1+μ)d outside Bad, then after deleting Bad every surviving edge has triangle degree at most (1+μ)d, and all but at most (2|Bad|/t)|V| of them have triangle degree at least (1−μ)d − 2t.

theorem Nibble.AX1.card_cliqueFinset_two_prune_ge {V : Type} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj] (Bad : Finset (Finset V)) : ↑(T.cliqueFinset 2).card - ↑Bad.card ≤ ↑((prune T Bad).cliqueFinset 2).card

Pruning destroys at most |Bad| edges.

A near-regular member from a single cluster triple

theorem Nibble.AX1.uniform_triple_member {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {U W X : Finset V} (hUW : Disjoint U W) (hUX : Disjoint U X) (hWX : Disjoint W X) {ε μ d t : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (ht : 0 < t) (hUWu : G.IsUniform ε U W) (hUXu : G.IsUniform ε U X) (hWXu : G.IsUniform ε W X) (hdUW : 2 * ε ≤ ↑(G.edgeDensity U W)) (hdUX : 2 * ε ≤ ↑(G.edgeDensity U X)) (hdWX : 2 * ε ≤ ↑(G.edgeDensity W X)) (hXlo : (1 - μ) * d ≤ (↑(G.edgeDensity U X) - ε) * (↑(G.edgeDensity W X) - 2 * ε) * ↑X.card) (hXhi : (↑(G.edgeDensity U X) + ε) * (↑(G.edgeDensity W X) + 2 * ε) * ↑X.card ≤ (1 + μ) * d) (hWlo : (1 - μ) * d ≤ (↑(G.edgeDensity U W) - ε) * (↑(G.edgeDensity W X) - 2 * ε) * ↑W.card) (hWhi : (↑(G.edgeDensity U W) + ε) * (↑(G.edgeDensity W X) + 2 * ε) * ↑W.card ≤ (1 + μ) * d) (hUlo : (1 - μ) * d ≤ (↑(G.edgeDensity U W) - ε) * (↑(G.edgeDensity U X) - 2 * ε) * ↑U.card) (hUhi : (↑(G.edgeDensity U W) + ε) * (↑(G.edgeDensity U X) + 2 * ε) * ↑U.card ≤ (1 + μ) * d) : ∃ (Bad : Finset (Finset V)), ↑Bad.card ≤ 4 * ε * (↑U.card * ↑W.card + ↑U.card * ↑X.card + ↑W.card * ↑X.card) ∧ prune (tripleGraph G U W X) Bad ≤ G ∧ (∀ e ∈ (prune (tripleGraph G U W X) Bad).cliqueFinset 2, ↑(edgeTriangleDegree (prune (tripleGraph G U W X) Bad) e) ≤ (1 + μ) * d) ∧ (∃ (Exc : Finset (Finset V)), ↑Exc.card ≤ 2 * ↑Bad.card / t * ↑(Fintype.card V) ∧ ∀ e ∈ (prune (tripleGraph G U W X) Bad).cliqueFinset 2, e ∉ Exc → (1 - μ) * d - 2 * t ≤ ↑(edgeTriangleDegree (prune (tripleGraph G U W X) Bad) e)) ∧ ↑((tripleGraph G U W X).cliqueFinset 2).card - ↑Bad.card ≤ ↑((prune (tripleGraph G U W X) Bad).cliqueFinset 2).card

A near-regular member of the family from one cluster triple. Under the hypotheses of Nibble.AX1.tripleGraph_near_regular (three pairwise ε-uniform pairs of density at least 2ε whose three triangle-degree scales are equalised to d within μ), deleting the ≤ 4ε(|U||W| + |U||X| + |W||X|) exceptional edges produces a subgraph H ≤ G in which

• every edge has triangle degree at most (1+μ)d;
• all but (2|Bad|/t)|V| edges have triangle degree at least (1−μ)d − 2t;
• at most |Bad| edges of the tripartite graph of the triple were lost.

This is exactly one member of the family Nibble.AX1.HasNearRegularFamily asks for; what the residual still needs is the global assembly of these members — see RESIDUAL.md.