CoreGapCoverCapacity

The six rectangles of a block sub-triple

theorem Nibble.AX1.prod_subset_tripleRect_AB {V : Type} [DecidableEq V] (A B C : Finset V) : A ×ˢ B ⊆ tripleRect A B C

theorem Nibble.AX1.prod_subset_tripleRect_BA {V : Type} [DecidableEq V] (A B C : Finset V) : B ×ˢ A ⊆ tripleRect A B C

theorem Nibble.AX1.prod_subset_tripleRect_AC {V : Type} [DecidableEq V] (A B C : Finset V) : A ×ˢ C ⊆ tripleRect A B C

theorem Nibble.AX1.prod_subset_tripleRect_CA {V : Type} [DecidableEq V] (A B C : Finset V) : C ×ˢ A ⊆ tripleRect A B C

theorem Nibble.AX1.prod_subset_tripleRect_BC {V : Type} [DecidableEq V] (A B C : Finset V) : B ×ˢ C ⊆ tripleRect A B C

theorem Nibble.AX1.prod_subset_tripleRect_CB {V : Type} [DecidableEq V] (A B C : Finset V) : C ×ˢ B ⊆ tripleRect A B C

The density-weighted area occupied in one ordered cluster pair

noncomputable def Nibble.AX1.pairArea {V : Type} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Finset (V × V)) (p : Finset V × Finset V) : ℝ

The density-weighted area a rectangle set occupies inside the ordered cluster pair p.

Equations

• Nibble.AX1.pairArea G R p = ↑(G.edgeDensity p.1 p.2) * ↑(R ∩ p.1 ×ˢ p.2).card

theorem Nibble.AX1.pairArea_nonneg {V : Type} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (R : Finset (V × V)) (p : Finset V × Finset V) : 0 ≤ pairArea G R p

theorem Nibble.AX1.rect_le_pairArea {V : Type} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {R : Finset (V × V)} {S T D E : Finset V} (hDS : D ⊆ S) (hET : E ⊆ T) (hDE : D ×ˢ E ⊆ R) : ↑(G.edgeDensity S T) * ↑D.card * ↑E.card ≤ pairArea G R (S, T)

A rectangle inside the ordered pair (S, T) contributes at most the pair's occupied area.

theorem Nibble.AX1.sum_card_inter_le {V : Type} [DecidableEq V] (R : ℕ → Finset (V × V)) (F : Finset ℕ) (S : Finset (V × V)) (hdisj : ∀ i ∈ F, ∀ j ∈ F, i ≠ j → Disjoint (R i) (R j)) : ∑ i ∈ F, ↑(R i ∩ S).card ≤ ↑S.card

Pairwise disjoint sets meet a fixed set in at most its cardinality.

theorem Nibble.AX1.two_cover_le_sum_pairArea {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) {U W X A B C : Finset V} (hU : U ∈ P.parts) (hW : W ∈ P.parts) (hX : X ∈ P.parts) (hUW : U ≠ W) (hUX : U ≠ X) (hWX : W ≠ X) (hA : A ⊆ U) (hB : B ⊆ W) (hC : C ⊆ X) : 2 * (↑(G.edgeDensity U W) * ↑A.card * ↑B.card + ↑(G.edgeDensity U X) * ↑A.card * ↑C.card + ↑(G.edgeDensity W X) * ↑B.card * ↑C.card) ≤ ∑ p ∈ P.parts.offDiag, pairArea G (tripleRect A B C) p

The six-term lower bound. Twice the (undivided) covering sum of one block sub-triple is picked up by the six ordered cluster pairs it occupies.

theorem Nibble.AX1.cover_sum_le_cluster_capacity {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) (hU : ∀ i < k, U i ∈ P.parts) (hW : ∀ i < k, W i ∈ P.parts) (hX : ∀ i < k, X i ∈ P.parts) (hUW : ∀ i < k, U i ≠ W i) (hUX : ∀ i < k, U i ≠ X i) (hWX : ∀ i < k, W i ≠ X i) (hA : ∀ i < k, A i ⊆ U i) (hB : ∀ i < k, B i ⊆ W i) (hC : ∀ i < k, C i ⊆ X i) (hdisj : ∀ i < k, ∀ j < k, i ≠ j → Disjoint (tripleRect (A i) (B i) (C i)) (tripleRect (A j) (B j) (C j))) : ∑ i ∈ Finset.range k, (↑(G.edgeDensity (U i) (W i)) * ↑(A i).card * ↑(B i).card + ↑(G.edgeDensity (U i) (X i)) * ↑(A i).card * ↑(C i).card + ↑(G.edgeDensity (W i) (X i)) * ↑(B i).card * ↑(C i).card) / 3 ≤ (∑ p ∈ P.parts.offDiag, ↑(G.edgeDensity p.1 p.2) * ↑p.1.card * ↑p.2.card) / 6

The conservation law of the fine block-allocation residual. A family of block sub-triples whose three clusters are distinct parts of P and whose vertex-pair rectangles are pairwise disjoint has covering sum at most one third of the total capacity ∑ d(S,T)·#S·#T of the cluster pairs (the sum on the right runs over ordered pairs, whence the 6).

CoreGapClusterLP

Two elementary facts about interedges

theorem Nibble.AX1.edgeDensity_mul_card_mul_card {V : Type} (G : SimpleGraph V) [DecidableRel G.Adj] (S T : Finset V) : ↑(G.edgeDensity S T) * ↑S.card * ↑T.card = ↑(G.interedges S T).card

The density-weighted area of a pair is its number of crossing edges.

theorem Nibble.AX1.card_interedges_mono {V : Type} {G H : SimpleGraph V} [DecidableRel G.Adj] [DecidableRel H.Adj] (h : H ≤ G) (S T : Finset V) : (H.interedges S T).card ≤ (G.interedges S T).card

Interedges are monotone in the graph.

Triangles of the reduced graph span three distinct parts

theorem Nibble.AX1.regularityReduced_parts_ne {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) {ep de : ℝ} {a b : V} (hab : (SimpleGraph.regularityReduced P G ep de).Adj a b) {A B : Finset V} (hA : A ∈ P.parts) (hB : B ∈ P.parts) (ha : a ∈ A) (hb : b ∈ B) : A ≠ B

Adjacent vertices of the regularity-reduced graph lie in different parts.

theorem Nibble.AX1.six_le_card_partPairs_of_mem_triangleHypergraph {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) {ep de : ℝ} {T : Finset (Finset V)} (hT : T ∈ YusterE.triangleHypergraphE (SimpleGraph.regularityReduced P G ep de)) : 6 ≤ {p ∈ P.parts.offDiag | ∃ x ∈ p.1, ∃ y ∈ p.2, {x, y} ∈ T}.card

Each triangle of the reduced graph is charged to at least six ordered cluster pairs.

The capacity bound

theorem Nibble.AX1.nu3star_regularityReduced_le_cluster_capacity {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (ep de : ℝ) : YusterE.nu3star (SimpleGraph.regularityReduced P G ep de) ≤ (∑ p ∈ P.parts.offDiag, ↑(G.edgeDensity p.1 p.2) * ↑p.1.card * ↑p.2.card) / 6

The cluster capacity LP caps ν₃* of the regularity-reduced graph. The right-hand side is exactly the ceiling of the covering sum of a family of block sub-triples with disjoint rectangles (Nibble.AX1.cover_sum_le_cluster_capacity), so the fine block-allocation residual carries no slack.

Discarding the sparse cluster pairs

theorem Nibble.AX1.sum_area_offDiag_le {V : Type} [Fintype V] [DecidableEq V] (P : Finpartition Finset.univ) : ∑ p ∈ P.parts.offDiag, ↑p.1.card * ↑p.2.card ≤ ↑(Fintype.card V) ^ 2

The total area of the ordered cluster pairs is at most |V|².

theorem Nibble.AX1.nu3star_regularityReduced_le_dense_cluster_capacity {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (P : Finpartition Finset.univ) (ep de : ℝ) {θ : ℝ} (hθ : 0 ≤ θ) : YusterE.nu3star (SimpleGraph.regularityReduced P G ep de) ≤ (∑ p ∈ P.parts.offDiag with θ ≤ ↑(G.edgeDensity p.1 p.2), ↑(G.edgeDensity p.1 p.2) * ↑p.1.card * ↑p.2.card) / 6 + θ * ↑(Fintype.card V) ^ 2 / 6

The capacity bound after discarding the sparse cluster pairs. Cluster pairs of density below θ can be thrown away at a total cost of θ·|V|²/6: this is why the block-allocation construction may assume that all cluster pairs it uses have density in [θ, 1], so that the block sizes τ·d of Nibble.AX1.IsGridSubTriple vary only within the bounded range [τθ, τ].

Axiom check