GridDesignRect

The general principle

theorem Nibble.AX1.tripleFamily_pairwise_edgeDisjoint {V : Type} (G : SimpleGraph V) {nA nB nC k : ℕ} (Ub Wb Xb : ℕ → Finset V) (IA IB IC : ℕ → ℕ) (hIA : ∀ i < k, IA i < nA) (hIB : ∀ i < k, IB i < nB) (hIC : ∀ i < k, IC i < nC) (hUU : ∀ a < nA, ∀ b < nA, a ≠ b → Disjoint (Ub a) (Ub b)) (hWW : ∀ a < nB, ∀ b < nB, a ≠ b → Disjoint (Wb a) (Wb b)) (hXX : ∀ a < nC, ∀ b < nC, a ≠ b → Disjoint (Xb a) (Xb b)) (hUW : ∀ a < nA, ∀ b < nB, Disjoint (Ub a) (Wb b)) (hUX : ∀ a < nA, ∀ b < nC, Disjoint (Ub a) (Xb b)) (hWX : ∀ a < nB, ∀ b < nC, Disjoint (Wb a) (Xb b)) (hABinj : ∀ i < k, ∀ i' < k, IA i = IA i' → IB i = IB i' → i = i') (hACinj : ∀ i < k, ∀ i' < k, IA i = IA i' → IC i = IC i' → i = i') (hBCinj : ∀ i < k, ∀ i' < k, IB i = IB i' → IC i = IC i' → i = i') {i : ℕ} (hi : i < k) {i' : ℕ} (hi' : i' < k) (hne : i ≠ i') (x y : V) (h : (tripleGraph G (Ub (IA i)) (Wb (IB i)) (Xb (IC i))).Adj x y) : ¬(tripleGraph G (Ub (IA i')) (Wb (IB i')) (Xb (IC i'))).Adj x y

A family of sub-triples with pairwise jointly injective index functions is edge-disjoint.

IA i, IB i, IC i are the indices of the three blocks of the i-th sub-triple. A common edge of two members determines which pair of clusters carries it, and — the blocks of a cluster being pairwise disjoint and blocks of different clusters being disjoint — the two indices of that pair; joint injectivity of that pair of index functions then forces the two members to coincide.

The rectangular diagonal indices

def Nibble.AX1.rectIdxA (nA nC i : ℕ) : ℕ

The U-block index of the i-th member of the rectangular diagonal design.

Equations

• Nibble.AX1.rectIdxA nA nC i = (i / nC + i % nC) % nA

def Nibble.AX1.rectIdxB (nC i : ℕ) : ℕ

The W-block index of the i-th member of the rectangular diagonal design.

Equations

• Nibble.AX1.rectIdxB nC i = i / nC

def Nibble.AX1.rectIdxC (nC i : ℕ) : ℕ

The X-block index of the i-th member of the rectangular diagonal design.

Equations

• Nibble.AX1.rectIdxC nC i = i % nC

theorem Nibble.AX1.rectIdxA_lt {nA nC : ℕ} (hnA : 0 < nA) (i : ℕ) : rectIdxA nA nC i < nA

theorem Nibble.AX1.rectIdxB_lt {nB nC i : ℕ} (hi : i < nB * nC) : rectIdxB nC i < nB

theorem Nibble.AX1.rectIdxC_lt {nC : ℕ} (hnC : 0 < nC) (i : ℕ) : rectIdxC nC i < nC

theorem Nibble.AX1.rectIdx_AB_inj {nA nB nC i i' : ℕ} (hCA : nC ≤ nA) (hi : i < nB * nC) (hi' : i' < nB * nC) (hA : rectIdxA nA nC i = rectIdxA nA nC i') (hB : rectIdxB nC i = rectIdxB nC i') : i = i'

The U–W block pair is used at most once — provided there are at least as many U-blocks as X-blocks.

theorem Nibble.AX1.rectIdx_AC_inj {nA nB nC i i' : ℕ} (hBA : nB ≤ nA) (hi : i < nB * nC) (hi' : i' < nB * nC) (hA : rectIdxA nA nC i = rectIdxA nA nC i') (hC : rectIdxC nC i = rectIdxC nC i') : i = i'

The U–X block pair is used at most once — provided there are at least as many U-blocks as W-blocks.

theorem Nibble.AX1.rectIdx_BC_inj {nC i i' : ℕ} (hB : rectIdxB nC i = rectIdxB nC i') (hC : rectIdxC nC i = rectIdxC nC i') : i = i'

The W–X block pair is used at most once.

The rectangular design

theorem Nibble.AX1.rectDesign_pairwise_edgeDisjoint {V : Type} (G : SimpleGraph V) {nA nB nC : ℕ} (Ub Wb Xb : ℕ → Finset V) (hBA : nB ≤ nA) (hCA : nC ≤ nA) (hUU : ∀ a < nA, ∀ b < nA, a ≠ b → Disjoint (Ub a) (Ub b)) (hWW : ∀ a < nB, ∀ b < nB, a ≠ b → Disjoint (Wb a) (Wb b)) (hXX : ∀ a < nC, ∀ b < nC, a ≠ b → Disjoint (Xb a) (Xb b)) (hUW : ∀ a < nA, ∀ b < nB, Disjoint (Ub a) (Wb b)) (hUX : ∀ a < nA, ∀ b < nC, Disjoint (Ub a) (Xb b)) (hWX : ∀ a < nB, ∀ b < nC, Disjoint (Wb a) (Xb b)) {i : ℕ} (hi : i < nB * nC) {i' : ℕ} (hi' : i' < nB * nC) (hne : i ≠ i') (x y : V) (h : (tripleGraph G (Ub (rectIdxA nA nC i)) (Wb (rectIdxB nC i)) (Xb (rectIdxC nC i))).Adj x y) : ¬(tripleGraph G (Ub (rectIdxA nA nC i')) (Wb (rectIdxB nC i')) (Xb (rectIdxC nC i'))).Adj x y

The rectangular diagonal design is edge-disjoint. The clusters U, W, X are split into nA, nB, nC pairwise disjoint blocks with nB, nC ≤ nA, and the nB · nC sub-triples (U_{(j+k) mod nA}, W_j, X_k) have pairwise no common edge.

GridScale

theorem Nibble.AX1.scale_window {x y z x' y' s τ d δ μ ε e : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) (hx : δ ≤ x) (hx1 : x ≤ 1) (hy : δ ≤ y) (hy1 : y ≤ 1) (hz : δ ≤ z) (hz1 : z ≤ 1) (hx' : |x' - x| ≤ e) (hy' : |y' - y| ≤ e) (hs : |s - τ * z| ≤ 1) (he : 0 ≤ e) (hε : 0 < ε) (hμ0 : 0 < μ) (hμ1 : μ ≤ 1) (hE : e + 2 * ε ≤ μ * δ ^ 3 / 12) (hτ : 2 / (μ * δ ^ 3) ≤ τ) (hd : d = τ * (x * y * z)) : (1 - μ) * d ≤ (x' - ε) * (y' - 2 * ε) * s ∧ (x' + ε) * (y' + 2 * ε) * s ≤ (1 + μ) * d

Scale equalisation. If the three cluster densities x, y, z lie in [δ, 1], the measured sub-block densities x', y' are within e of x, y, the block size s is within 1 of τ·z, the total error satisfies e + 2ε ≤ μδ³/12 and the scale satisfies τ ≥ 2/(μδ³), then the two-sided codegree count (x' ∓ ε)(y' ∓ 2ε)·s lies in the window (1 ± μ)·d around the common scale d = τ·x·y·z.

CoreGapSubblock

theorem Nibble.AX1.edgeDensity_sub_lt_of_isUniform {V : Type} (G : SimpleGraph V) [DecidableRel G.Adj] {A B A' B' : Finset V} {ε α : ℝ} (hU : G.IsUniform ε A B) (hA' : A' ⊆ A) (hB' : B' ⊆ B) (hεα : ε ≤ α) (hcardA : α * ↑A.card ≤ ↑A'.card) (hcardB : α * ↑B.card ≤ ↑B'.card) : |↑(G.edgeDensity A' B') - ↑(G.edgeDensity A B)| < ε

A pair of subsets of relative size at least α ≥ ε of an ε-uniform pair has density within ε of the density of the pair.

theorem Nibble.AX1.isUniform_subblock {V : Type} (G : SimpleGraph V) [DecidableRel G.Adj] {A B A' B' : Finset V} {ε α : ℝ} (hU : G.IsUniform ε A B) (hε : 0 < ε) (hA' : A' ⊆ A) (hB' : B' ⊆ B) (hεα : ε ≤ α) (hα : 2 * α ≤ 1) (hcardA : α * ↑A.card ≤ ↑A'.card) (hcardB : α * ↑B.card ≤ ↑B'.card) : G.IsUniform (ε / α) A' B'

Uniformity passes to large sub-blocks. If (A, B) is ε-uniform and A' ⊆ A, B' ⊆ B have relative size at least α, with ε ≤ α ≤ 1/2, then (A', B') is (ε/α)-uniform.

The proof is the obvious one: a subset of A' of relative size ε/α has absolute size at least ε|A|, so uniformity of (A, B) applies to it and to (A', B') itself, and the two densities are each within ε of d(A, B), hence within 2ε ≤ ε/α of each other.

CoreGapTripleShape

def Nibble.AX1.IsSubTripleShape {V : Type} (G : SimpleGraph V) [DecidableRel G.Adj] (ε₂ μ₂ : ℝ) (k : ℕ) (A B C : ℕ → Finset V) (d : ℕ → ℝ) : Prop

The local clauses of a sub-triple design. Everything in Nibble.AX1.IsSubTripleDesign that refers only to the sub-triples themselves: the three parts of each sub-triple are disjoint, pairwise ε₂-uniform and of density at least 2ε₂, the three triangle-degree scales of each sub-triple agree with a common d i to within μ₂, and the tripartite graphs of the family are pairwise edge-disjoint.

Equations

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

theorem Nibble.AX1.isSubTripleDesign_of_shape {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {ε μ η d₀ ε₂ μ₂ t : ℝ} {k : ℕ} {A B C : ℕ → Finset V} {d Elo : ℕ → ℝ} (hshape : IsSubTripleShape G ε₂ μ₂ k A B C d) (hε₂ : 0 < ε₂) (hε₂1 : ε₂ ≤ 1) (ht : 0 < t) (hη : 0 ≤ η) (hμ₂ : μ₂ ≤ μ) (hd₀ : ∀ i < k, d₀ ≤ d i) (hdnn : ∀ i < k, 0 ≤ d i) (hslack : ∀ i < k, 2 * t ≤ (μ - μ₂) * d i) (hElo : ∀ i < k, Elo i ≤ ↑((tripleGraph G (A i) (B i) (C i)).cliqueFinset 2).card) (hexc : ∀ i < k, 2 * designBad ε₂ (A i) (B i) (C i) / t * ↑(Fintype.card V) ≤ η * (Elo i - designBad ε₂ (A i) (B i) (C i))) (hcover : YusterE.nu3star G ≤ ∑ i ∈ Finset.range k, (Elo i - designBad ε₂ (A i) (B i) (C i)) / 3 + ε * ↑(Fintype.card V) ^ 2) : IsSubTripleDesign G ε μ η d₀ ε₂ μ₂ t k A B C d Elo

A shape together with the global clauses is a design.

The construction inside one cluster triple

theorem Nibble.AX1.subTripleShape_grid {V : Type} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {U W X : Finset V} {δ μ₂ ε₁ α τ : ℝ} {sA sB sC nA nB nC : ℕ} (hUW : Disjoint U W) (hUX : Disjoint U X) (hWX : Disjoint W X) (huUW : G.IsUniform ε₁ U W) (huUX : G.IsUniform ε₁ U X) (huWX : G.IsUniform ε₁ W X) (hε₁ : 0 < ε₁) (hαε : ε₁ ≤ α) (hα2 : 2 * α ≤ 1) (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) (hμ0 : 0 < μ₂) (hμ1 : μ₂ ≤ 1) (hx : δ ≤ ↑(G.edgeDensity U W)) (hy : δ ≤ ↑(G.edgeDensity U X)) (hz : δ ≤ ↑(G.edgeDensity W X)) (hErr : ε₁ + 2 * (ε₁ / α) ≤ μ₂ * δ ^ 3 / 12) (hdense : 2 * (ε₁ / α) + ε₁ ≤ δ) (hτ : 2 / (μ₂ * δ ^ 3) ≤ τ) (hsA : |↑sA - τ * ↑(G.edgeDensity W X)| ≤ 1) (hsB : |↑sB - τ * ↑(G.edgeDensity U X)| ≤ 1) (hsC : |↑sC - τ * ↑(G.edgeDensity U W)| ≤ 1) (hsA0 : 0 < sA) (hsB0 : 0 < sB) (hsC0 : 0 < sC) (hfitA : nA * sA ≤ U.card) (hfitB : nB * sB ≤ W.card) (hfitC : nC * sC ≤ X.card) (hrelA : α * ↑U.card ≤ ↑sA) (hrelB : α * ↑W.card ≤ ↑sB) (hrelC : α * ↑X.card ≤ ↑sC) (hBA : nB ≤ nA) (hCA : nC ≤ nA) : IsSubTripleShape G (ε₁ / α) μ₂ (nB * nC) (fun (i : ℕ) => blockOf U sA (rectIdxA nA nC i)) (fun (i : ℕ) => blockOf W sB (rectIdxB nC i)) (fun (i : ℕ) => blockOf X sC (rectIdxC nC i)) fun (x : ℕ) => τ * (↑(G.edgeDensity U W) * ↑(G.edgeDensity U X) * ↑(G.edgeDensity W X))

The sub-block grid of one cluster triple is a shape.

The clusters U, W, X are pairwise ε₁-uniform of densities x = d(U,W), y = d(U,X), z = d(W,X) in [δ, 1]. Split U into nA blocks of size sA ≈ τ·z, W into nB blocks of size sB ≈ τ·y and X into nC blocks of size sC ≈ τ·x — each block size proportional to the density of the opposite pair, and each block of relative size at least α in its cluster — and take the nB·nC diagonal sub-triples of Nibble.AX1.rectDesign_pairwise_edgeDisjoint. Then, at uniformity scale ε₂ = ε₁/α, this family is a shape with the single triangle-degree scale d = τ·x·y·z.