CoreGapPruneLocal

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

Few edges have an endpoint at which many edges were deleted — localised version. The number of vertices at which more than t edges were deleted is at most 2|Bad|/t, and each of them lies in at most D edges.

theorem Nibble.AX1.prune_near_regular_local {V : Type} [Fintype V] [DecidableEq V] (T : SimpleGraph V) [DecidableRel T.Adj] (Bad : Finset (Finset V)) {μ d t : ℝ} (ht : 0 < t) {D : ℕ} (hdeg : ∀ (v : V), {z : V | T.Adj v z}.card ≤ D) (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 * ↑D ∧ ∀ e ∈ (prune T Bad).cliqueFinset 2, e ∉ Exc → (1 - μ) * d - 2 * t ≤ ↑(edgeTriangleDegree (prune T Bad) e)

The pruned graph — localised. As Nibble.AX1.prune_near_regular, but the exceptional set is bounded using a degree bound D for T instead of the number of vertices of the ambient graph.

theorem Nibble.AX1.tripleGraph_degree_le {V : Type} [Fintype V] (G : SimpleGraph V) (U W X : Finset V) (v : V) : {z : V | (tripleGraph G U W X).Adj v z}.card ≤ U.card + W.card + X.card

A tripartite graph has degrees at most |U| + |W| + |X|: all its edges stay inside the three parts.

theorem Nibble.AX1.uniform_triple_member_local {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 * (↑U.card + ↑W.card + ↑X.card) ∧ ∀ 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 — localised. As Nibble.AX1.uniform_triple_member, but the exceptional edges are bounded by (2|Bad|/t)·(|U| + |W| + |X|), which involves only the triple and not the ambient graph.

CoreGapDesignLocal

noncomputable def Nibble.AX1.designSupport {V : Type} (A B C : Finset V) : ℝ

The support size |A| + |B| + |C| of a sub-triple: the localised replacement for |V| in the exceptional-edge clause of a design.

Equations

• Nibble.AX1.designSupport A B C = ↑A.card + ↑B.card + ↑C.card

def Nibble.AX1.IsSubTripleDesignLocal {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (ε μ η d₀ ε₂ μ₂ t : ℝ) (k : ℕ) (A B C : ℕ → Finset V) (d Elo : ℕ → ℝ) : Prop

A local sub-triple design. The shape of Nibble.AX1.IsSubTripleShape together with the global clauses, the exceptional-edge clause now being charged against the support of the sub-triple rather than against the whole vertex set.

Equations

• One or more equations did not get rendered due to their size.

theorem Nibble.AX1.hasNearRegularFamily_of_subTripleDesignLocal {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {ε μ η d₀ ε₂ μ₂ t : ℝ} {k : ℕ} {A B C : ℕ → Finset V} {d Elo : ℕ → ℝ} (h : IsSubTripleDesignLocal G ε μ η d₀ ε₂ μ₂ t k A B C d Elo) : HasNearRegularFamily G ε μ η d₀

The bridge from a local sub-triple design to a near-regular family. Identical to Nibble.AX1.hasNearRegularFamily_of_subTripleDesign except that the exceptional edges of each member are charged against the support of that member, via Nibble.AX1.uniform_triple_member_local.

CoreGapGridResidual

def Nibble.AX1.SubTripleDesignAt (ε μ η d₀ ε₁ : ℝ) : Prop

The design form of the reduced residual at parameters (ε, μ, η, d₀) and regularity scale ε₁: every triangle-rich regularity-reduced graph carries a sub-triple design in the sense of Nibble.AX1.IsSubTripleDesign.

Equations

• One or more equations did not get rendered due to their size.

def Nibble.AX1.SubTripleDesignResidual : Prop

The design residual: a sub-triple design at every window of parameters, for some regularity scale ε₁ as small as one likes.

Equations

• One or more equations did not get rendered due to their size.

theorem Nibble.AX1.reducedFamilyAt_of_subTripleDesignAt {ε μ η d₀ ε₁ : ℝ} (h : SubTripleDesignAt ε μ η d₀ ε₁) : ReducedFamilyAt ε μ η d₀ ε₁

A design gives the reduced family.

theorem Nibble.AX1.reducedFamilyResidual_of_subTripleDesign (h : SubTripleDesignResidual) : ReducedFamilyResidual

The design residual implies the structural residual Nibble.AX1.ReducedFamilyResidual.

theorem Nibble.AX1.ax1_of_subTripleDesign (h : SubTripleDesignResidual) : AX1Statement

AX1 from the design residual.

CoreGapGridLocalResidual

def Nibble.AX1.SubTripleDesignLocalAt (ε μ η d₀ ε₁ : ℝ) : Prop

The local design form of the reduced residual at parameters (ε, μ, η, d₀) and regularity scale ε₁: every triangle-rich regularity-reduced graph carries a sub-triple design in the sense of Nibble.AX1.IsSubTripleDesignLocal.

Equations

• One or more equations did not get rendered due to their size.

def Nibble.AX1.SubTripleDesignLocalResidual : Prop

The local design residual: a local sub-triple design at every window of parameters, for some regularity scale ε₁ as small as one likes.

Equations

• One or more equations did not get rendered due to their size.

theorem Nibble.AX1.reducedFamilyAt_of_subTripleDesignLocalAt {ε μ η d₀ ε₁ : ℝ} (h : SubTripleDesignLocalAt ε μ η d₀ ε₁) : ReducedFamilyAt ε μ η d₀ ε₁

A local design gives the reduced family.

theorem Nibble.AX1.reducedFamilyResidual_of_subTripleDesignLocal (h : SubTripleDesignLocalResidual) : ReducedFamilyResidual

The local design residual implies the structural residual Nibble.AX1.ReducedFamilyResidual.

theorem Nibble.AX1.ax1_of_subTripleDesignLocal (h : SubTripleDesignLocalResidual) : AX1Statement

AX1 from the local design residual.