CoreGapReducedPair #
theorem
Nibble.AX1.regularityReduced_adj_iff_of_goodPair
{V : Type}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(P : Finpartition Finset.univ)
{ep de : ℝ}
{U W : Finset V}
(hU : U ∈ P.parts)
(hW : W ∈ P.parts)
(hUW : U ≠ W)
(hu : G.IsUniform ep U W)
(hd : de ≤ ↑(G.edgeDensity U W))
{x y : V}
(hx : x ∈ U)
(hy : y ∈ W)
:
On a good cluster pair the reduced graph agrees with G.
theorem
Nibble.AX1.interedges_regularityReduced
{V : Type}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(P : Finpartition Finset.univ)
{ep de : ℝ}
{U W A B : Finset V}
(hU : U ∈ P.parts)
(hW : W ∈ P.parts)
(hUW : U ≠ W)
(hu : G.IsUniform ep U W)
(hd : de ≤ ↑(G.edgeDensity U W))
(hA : A ⊆ U)
(hB : B ⊆ W)
:
The interedges of two sub-blocks of a good cluster pair are the same in G and in the reduced
graph.
theorem
Nibble.AX1.edgeDensity_regularityReduced
{V : Type}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(P : Finpartition Finset.univ)
{ep de : ℝ}
{U W A B : Finset V}
(hU : U ∈ P.parts)
(hW : W ∈ P.parts)
(hUW : U ≠ W)
(hu : G.IsUniform ep U W)
(hd : de ≤ ↑(G.edgeDensity U W))
(hA : A ⊆ U)
(hB : B ⊆ W)
:
The densities of two sub-blocks of a good cluster pair are the same in G and in the reduced
graph.
theorem
Nibble.AX1.isUniform_regularityReduced
{V : Type}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(P : Finpartition Finset.univ)
{ep de ε : ℝ}
{U W A B : Finset V}
(hU : U ∈ P.parts)
(hW : W ∈ P.parts)
(hUW : U ≠ W)
(hu : G.IsUniform ep U W)
(hd : de ≤ ↑(G.edgeDensity U W))
(hA : A ⊆ U)
(hB : B ⊆ W)
(h : G.IsUniform ε A B)
:
(SimpleGraph.regularityReduced P G ep de).IsUniform ε A B
Uniformity of a pair of sub-blocks transfers to the reduced graph.
CoreGapBlockShape #
def
Nibble.AX1.IsGridSubTriple
{V : Type}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(P : Finpartition Finset.univ)
(ep de α τ : ℝ)
(U W X A B C : Finset V)
:
One sub-triple of the grid construction: blocks A ⊆ U, B ⊆ W, C ⊆ X of a good cluster
triple, each of relative size at least α in its cluster, with sizes proportional to the density of
the opposite pair at the common scale τ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Nibble.AX1.gridSubTriple_data
{V : Type}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(P : Finpartition Finset.univ)
{δ α τ ε₁ : ℝ}
{U W X A B C : Finset V}
(hε₁ : 0 < ε₁)
(hαε : ε₁ / 8 ≤ α)
(hα2 : 2 * α ≤ 1)
(hde : ε₁ / 4 ≤ δ)
(h : IsGridSubTriple G P (ε₁ / 8) δ α τ U W X A B C)
:
(Disjoint A B ∧ Disjoint A C ∧ Disjoint B C) ∧ ((SimpleGraph.regularityReduced P G (ε₁ / 8) (ε₁ / 4)).IsUniform (ε₁ / 8 / α) A B ∧ (SimpleGraph.regularityReduced P G (ε₁ / 8) (ε₁ / 4)).IsUniform (ε₁ / 8 / α) A C ∧ (SimpleGraph.regularityReduced P G (ε₁ / 8) (ε₁ / 4)).IsUniform (ε₁ / 8 / α) B C) ∧ |↑((SimpleGraph.regularityReduced P G (ε₁ / 8) (ε₁ / 4)).edgeDensity A B) - ↑(G.edgeDensity U W)| ≤ ε₁ / 8 ∧ |↑((SimpleGraph.regularityReduced P G (ε₁ / 8) (ε₁ / 4)).edgeDensity A C) - ↑(G.edgeDensity U X)| ≤ ε₁ / 8 ∧ |↑((SimpleGraph.regularityReduced P G (ε₁ / 8) (ε₁ / 4)).edgeDensity B C) - ↑(G.edgeDensity W X)| ≤ ε₁ / 8
The three pairs of one block sub-triple: they are disjoint, uniform at scale ε₁/(8α) in
the reduced graph, and their densities are within ε₁/8 of the densities of the cluster pairs.
theorem
Nibble.AX1.gridSubTriple_density_mem
{V : Type}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(P : Finpartition Finset.univ)
{δ α τ ep : ℝ}
{U W X A B C : Finset V}
(h : IsGridSubTriple G P ep δ α τ U W X A B C)
:
(δ ≤ ↑(G.edgeDensity U W) ∧ ↑(G.edgeDensity U W) ≤ 1) ∧ (δ ≤ ↑(G.edgeDensity U X) ∧ ↑(G.edgeDensity U X) ≤ 1) ∧ δ ≤ ↑(G.edgeDensity W X) ∧ ↑(G.edgeDensity W X) ≤ 1
The cluster densities of a good triple lie in [δ, 1].
theorem
Nibble.AX1.subTripleShape_of_gridSubTriples
{V : Type}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(P : Finpartition Finset.univ)
{δ α τ μ₂ ε₁ : ℝ}
{k : ℕ}
(U W X A B C : ℕ → Finset V)
(hε₁ : 0 < ε₁)
(hαε : ε₁ / 8 ≤ α)
(hα2 : 2 * α ≤ 1)
(hδ0 : 0 < δ)
(hδ1 : δ ≤ 1)
(hμ0 : 0 < μ₂)
(hμ1 : μ₂ ≤ 1)
(hde : ε₁ / 4 ≤ δ)
(hErr : ε₁ / 8 + 2 * (ε₁ / 8 / α) ≤ μ₂ * δ ^ 3 / 12)
(hdense : 2 * (ε₁ / 8 / α) + ε₁ / 8 ≤ δ)
(hτ : 2 / (μ₂ * δ ^ 3) ≤ τ)
(hgrid : ∀ i < k, IsGridSubTriple G P (ε₁ / 8) δ α τ (U i) (W i) (X i) (A i) (B i) (C i))
(hdisj : ∀ i < k, ∀ j < k, i ≠ j → Disjoint (tripleRect (A i) (B i) (C i)) (tripleRect (A j) (B j) (C j)))
:
IsSubTripleShape (SimpleGraph.regularityReduced P G (ε₁ / 8) (ε₁ / 4)) (ε₁ / 8 / α) μ₂ k A B C fun (i : ℕ) =>
τ * (↑(G.edgeDensity (U i) (W i)) * ↑(G.edgeDensity (U i) (X i)) * ↑(G.edgeDensity (W i) (X i)))
The local clauses of a design, for a family of block sub-triples.