CoreGapDesign

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

The exceptional-edge budget of a sub-triple at uniformity scale ε₂: the bound 4ε₂(|A||B| + |A||C| + |B||C|) of Nibble.AX1.tripleGraph_near_regular.

Equations

• Nibble.AX1.designBad ε₂ A B C = 4 * ε₂ * (↑A.card * ↑B.card + ↑A.card * ↑C.card + ↑B.card * ↑C.card)

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

A sub-triple design for G at parameters (ε, μ, η, d₀), with internal scales (ε₂, μ₂, t). This is the exact package of hypotheses that Nibble.AX1.hasNearRegularFamily_of_subTripleDesign turns into a near-regular family; it contains no probability and no regularity argument, only explicit inequalities about the k sub-triples (A i, B i, C i), their common triangle-degree scales d i and the lower bounds Elo i for their edge counts.

Equations

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

theorem Nibble.AX1.hasNearRegularFamily_of_subTripleDesign {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {ε μ η d₀ ε₂ μ₂ t : ℝ} (k : ℕ) (A B C : ℕ → Finset V) (d Elo : ℕ → ℝ) (hε₂ : 0 < ε₂) (hε₂1 : ε₂ ≤ 1) (ht : 0 < t) (hη : 0 ≤ η) (hdAB : ∀ i < k, Disjoint (A i) (B i)) (hdAC : ∀ i < k, Disjoint (A i) (C i)) (hdBC : ∀ i < k, Disjoint (B i) (C i)) (huAB : ∀ i < k, G.IsUniform ε₂ (A i) (B i)) (huAC : ∀ i < k, G.IsUniform ε₂ (A i) (C i)) (huBC : ∀ i < k, G.IsUniform ε₂ (B i) (C i)) (hρAB : ∀ i < k, 2 * ε₂ ≤ ↑(G.edgeDensity (A i) (B i))) (hρAC : ∀ i < k, 2 * ε₂ ≤ ↑(G.edgeDensity (A i) (C i))) (hρBC : ∀ i < k, 2 * ε₂ ≤ ↑(G.edgeDensity (B i) (C i))) (hClo : ∀ i < k, (1 - μ₂) * d i ≤ (↑(G.edgeDensity (A i) (C i)) - ε₂) * (↑(G.edgeDensity (B i) (C i)) - 2 * ε₂) * ↑(C i).card) (hChi : ∀ i < k, (↑(G.edgeDensity (A i) (C i)) + ε₂) * (↑(G.edgeDensity (B i) (C i)) + 2 * ε₂) * ↑(C i).card ≤ (1 + μ₂) * d i) (hBlo : ∀ i < k, (1 - μ₂) * d i ≤ (↑(G.edgeDensity (A i) (B i)) - ε₂) * (↑(G.edgeDensity (B i) (C i)) - 2 * ε₂) * ↑(B i).card) (hBhi : ∀ i < k, (↑(G.edgeDensity (A i) (B i)) + ε₂) * (↑(G.edgeDensity (B i) (C i)) + 2 * ε₂) * ↑(B i).card ≤ (1 + μ₂) * d i) (hAlo : ∀ i < k, (1 - μ₂) * d i ≤ (↑(G.edgeDensity (A i) (B i)) - ε₂) * (↑(G.edgeDensity (A i) (C i)) - 2 * ε₂) * ↑(A i).card) (hAhi : ∀ i < k, (↑(G.edgeDensity (A i) (B i)) + ε₂) * (↑(G.edgeDensity (A i) (C i)) + 2 * ε₂) * ↑(A i).card ≤ (1 + μ₂) * d i) (hd₀ : ∀ i < k, d₀ ≤ d i) (hdnn : ∀ i < k, 0 ≤ d i) (hμ₂ : μ₂ ≤ μ) (hslack : ∀ i < k, 2 * t ≤ (μ - μ₂) * d i) (hpair : ∀ i < k, ∀ j < k, i ≠ j → ∀ (x y : V), (tripleGraph G (A i) (B i) (C i)).Adj x y → ¬(tripleGraph G (A j) (B j) (C j)).Adj x y) (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) : HasNearRegularFamily G ε μ η d₀

The bridge from a sub-triple design to a near-regular family.

A design consists of k triples (A i, B i, C i) of pairwise disjoint vertex sets which are

• pairwise ε₂-uniform of density at least 2ε₂;
• scale equalised: the three triangle-degree scales of the triple agree with a common d i ≥ d₀ to within μ₂, even after the ε₂-slack of the counting lemma;
• pairwise edge-disjoint as tripartite graphs;
• large: Elo i is a lower bound for the number of edges of the i-th tripartite graph, the exceptional edges produced by pruning are at most an η-fraction of what survives, and the surviving edges recover 3ν₃*(G) − 3ε|V|².

Then G has a near-regular family at (ε, μ, η, d₀). The members are the pruned tripartite graphs Nibble.AX1.prune (tripleGraph G (A i) (B i) (C i)) Badᵢ of Nibble.AX1.uniform_triple_member.

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

The bridge, in packaged form.