Top regularity over polyads

A coloring H of the unordered triples is (δ, r)-top-regular over a polyad P when, for every top color c and every union of at most r subpolyads of P carrying at least a δ-fraction of the support of P, the relative density of c on that union is within δ of its relative density over P. Subpolyads select arbitrary subgraphs of the three pair graphs of P, so this is the rank-r test surface of Rödl–Schacht and Nagle–Rödl–Schacht; rank one is the disc-regular case. Each top color is controlled separately.

The weaker vertex-box condition IsVertexBoxRegularOverPolyad only tests restrictions of the three vertex cells, keeping the full pair graphs. It follows from top regularity at any positive rank.

Top regularity passes to smaller polyads. If the three pair graphs of a polyad P', possibly over another skeleton such as a refinement of the skeleton of P, lie in those of P, then every subpolyad of P' is a subpolyad of P with the same support. Hence a large P' inherits the relative densities of P up to δ, and the slicing lemma makes H top-regular over P' with a parameter worsened by a factor depending only on the relative size of P'.

Main definitions

• TauCeti.Colored3Graph.IsTopRegularOverPolyad: (δ, r)-regularity over a polyad.
• TauCeti.Colored3Graph.IsVertexBoxRegularOverPolyad: regularity on vertex-box restrictions.

Main results

• TauCeti.Colored3Graph.IsTopRegularOverPolyad.abs_relDensityOn_sub_le: the test applies to every family of at most r subpolyads, indexed by any finite type.
• Colored3Graph.IsTopRegularOverPolyad.abs_relDensityOn_unionSupport_sub_mul_card_le_of_card_le: the count-scaled form of the test, valid also below the size threshold.
• TauCeti.Colored3Graph.IsTopRegularOverPolyad.of_rank_le: regularity at a higher rank implies regularity at every lower rank.
• TauCeti.Colored3Graph.isTopRegularOverPolyad_one_iff: at rank one the condition tests single subpolyads.
• TauCeti.Colored3Graph.IsTopRegularOverPolyad.nonneg: the parameter of a top-regular coloring is nonnegative.
• TauCeti.Colored3Graph.IsTopRegularOverPolyad.abs_relativeDensity_sub_le: a large polyad with smaller pair graphs inherits the relative densities up to δ.
• TauCeti.Colored3Graph.IsTopRegularOverPolyad.of_pairSupport_subset: the slicing lemma; top regularity passes to every polyad with smaller pair graphs and at least an α-fraction of the support, with parameter max (2δ) (δ / α).
• TauCeti.Colored3Graph.IsTopRegularOverPolyad.isVertexBoxRegularOverPolyad: top regularity at a positive rank implies vertex-box regularity.
• TauCeti.Colored3Graph.isTopRegularOverPolyad_const: a constant coloring is top-regular over every polyad, at every rank and every positive parameter.

References

• J. Komlós and M. Simonovits, Szemerédi's regularity lemma and its applications in graph theory, in Combinatorics, Paul Erdős is Eighty, Vol. 2 (1996), Fact 1.5 (the graph slicing lemma, whose argument the hypergraph slicing lemma follows).
• V. Rödl and M. Schacht, Regular partitions of hypergraphs: regularity lemmas, Combin. Probab. Comput. 16 (2007).
• B. Nagle, V. Rödl and M. Schacht, The counting lemma for regular k-uniform hypergraphs, Random Structures Algorithms 28 (2006).

def TauCeti.Colored3Graph.IsTopRegularOverPolyad {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_3} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ₂ V} (P : Polyad3 S) [DecidableEq κ] (H : Colored3Graph κ V) (δ : ℝ) (r : ℕ) : Prop

H is (δ, r)-top-regular over the polyad P when, for every top color c and every family of r subpolyads of P whose union support has at least δ times the size of the support of P, the relative density of c on that union is within δ of the relative density of c over P. Members of the family may repeat, so this tests unions of at most r subpolyads.

theorem TauCeti.Colored3Graph.isTopRegularOverPolyad_iff {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_3} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ₂ V} {P : Polyad3 S} [DecidableEq κ] {H : Colored3Graph κ V} {δ : ℝ} {r : ℕ} : IsTopRegularOverPolyad P H δ r ↔ ∀ (c : κ) (Q : Fin r → Subpolyad3 P), δ * ↑P.support.card ≤ ↑(Subpolyad3.unionSupport Q).card → |↑(H.relDensityOn c (Subpolyad3.unionSupport Q)) - ↑(H.relativeDensity c P)| ≤ δ

Unfolded form of Colored3Graph.IsTopRegularOverPolyad.

theorem TauCeti.Colored3Graph.exists_subpolyads_witnessing_irregularity {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_3} [Fintype V] [DecidableEq V] [DecidableEq κ] (H : Colored3Graph κ V) {δ : ℝ} (r : ℕ) (S : PairSkeleton3 κ₂ V) : ∃ (Q : (P : Polyad3 S) → Fin r → Subpolyad3 P), ∀ (P : Polyad3 S), ¬IsTopRegularOverPolyad P H δ r → ∃ (c : κ), δ * ↑P.support.card ≤ ↑(Subpolyad3.unionSupport (Q P)).card ∧ δ ≤ |↑(H.relDensityOn c (Subpolyad3.unionSupport (Q P))) - ↑(H.relativeDensity c P)|

Every polyad over S that is not (δ, r)-top-regular has r subpolyads whose union carries at least a δ-proportion of its support and whose relative density in some top color deviates from that of the polyad by at least δ.

theorem TauCeti.Colored3Graph.IsTopRegularOverPolyad.abs_relDensityOn_sub_le {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_3} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ₂ V} {P : Polyad3 S} [DecidableEq κ] {H : Colored3Graph κ V} {δ : ℝ} {r : ℕ} (h : IsTopRegularOverPolyad P H δ r) (c : κ) {ι : Type u_4} [Fintype ι] (hι : Fintype.card ι ≤ r) (Q : ι → Subpolyad3 P) (hQ : δ * ↑P.support.card ≤ ↑(Subpolyad3.unionSupport Q).card) : |↑(H.relDensityOn c (Subpolyad3.unionSupport Q)) - ↑(H.relativeDensity c P)| ≤ δ

The rank-r test. A (δ, r)-top-regular coloring passes the test on the union of any family of at most r subpolyads, indexed by an arbitrary finite type.

theorem TauCeti.Colored3Graph.IsTopRegularOverPolyad.of_rank_le {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_3} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ₂ V} {P : Polyad3 S} [DecidableEq κ] {H : Colored3Graph κ V} {δ : ℝ} {r r' : ℕ} (h : IsTopRegularOverPolyad P H δ r') (hr : r ≤ r') : IsTopRegularOverPolyad P H δ r

Top regularity at a rank implies top regularity at every lower rank.

theorem TauCeti.Colored3Graph.IsTopRegularOverPolyad.mono {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_3} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ₂ V} {P : Polyad3 S} [DecidableEq κ] {H : Colored3Graph κ V} {δ δ' : ℝ} {r : ℕ} (h : IsTopRegularOverPolyad P H δ r) (hδ : δ ≤ δ') : IsTopRegularOverPolyad P H δ' r

Top regularity is monotone in its parameter.

theorem TauCeti.Colored3Graph.isTopRegularOverPolyad_one_iff {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_3} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ₂ V} {P : Polyad3 S} [DecidableEq κ] {H : Colored3Graph κ V} {δ : ℝ} : IsTopRegularOverPolyad P H δ 1 ↔ ∀ (c : κ) (Q : Subpolyad3 P), δ * ↑P.support.card ≤ ↑Q.support.card → |↑(H.relDensityOn c Q.support) - ↑(H.relativeDensity c P)| ≤ δ

At rank one, top regularity tests single subpolyads.

theorem TauCeti.Colored3Graph.isTopRegularOverPolyad_of_one_le {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_3} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ₂ V} (P : Polyad3 S) [DecidableEq κ] (H : Colored3Graph κ V) {δ : ℝ} (r : ℕ) (hδ : 1 ≤ δ) : IsTopRegularOverPolyad P H δ r

Every coloring is top-regular once 1 ≤ δ, since relative densities lie in [0, 1].

theorem TauCeti.Colored3Graph.IsTopRegularOverPolyad.nonneg {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_3} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ₂ V} {P : Polyad3 S} [DecidableEq κ] {H : Colored3Graph κ V} {δ : ℝ} {r : ℕ} [Nonempty κ] (h : IsTopRegularOverPolyad P H δ r) : 0 ≤ δ

Top regularity over a polyad forces a nonnegative parameter when the top palette is nonempty: for a negative parameter, every family passes the size threshold.

theorem TauCeti.Colored3Graph.IsTopRegularOverPolyad.abs_relDensityOn_unionSupport_sub_mul_card_le_of_card_le {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_3} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ₂ V} {P : Polyad3 S} [DecidableEq κ] {H : Colored3Graph κ V} {δ : ℝ} {r : ℕ} (h : IsTopRegularOverPolyad P H δ r) (c : κ) {ι : Type u_4} [Fintype ι] (hι : Fintype.card ι ≤ r) (Q : ι → Subpolyad3 P) : |↑(H.relDensityOn c (Subpolyad3.unionSupport Q)) - ↑(H.relativeDensity c P)| * ↑(Subpolyad3.unionSupport Q).card ≤ δ * ↑P.support.card

Count-scaled rank-r test. A (δ, r)-top-regular coloring bounds the count-scaled discrepancy of each top color on the union of any family of at most r subpolyads by δ |P|. Unlike the test itself, this also covers unions below the size threshold.

theorem TauCeti.Colored3Graph.IsTopRegularOverPolyad.abs_relativeDensity_sub_le {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_3} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ₂ V} {P : Polyad3 S} [DecidableEq κ] {H : Colored3Graph κ V} {δ : ℝ} {r : ℕ} {κ₂' : Type u_4} {S' : PairSkeleton3 κ₂' V} {P' : Polyad3 S'} (h₀₁ : P'.pairSupport₀₁ ⊆ P.pairSupport₀₁) (h₀₂ : P'.pairSupport₀₂ ⊆ P.pairSupport₀₂) (h₁₂ : P'.pairSupport₁₂ ⊆ P.pairSupport₁₂) (h : IsTopRegularOverPolyad P H δ r) (hr : 1 ≤ r) (hP' : δ * ↑P.support.card ≤ ↑P'.support.card) (c : κ) : |↑(H.relativeDensity c P') - ↑(H.relativeDensity c P)| ≤ δ

Density inheritance. If H is top-regular over P at a positive rank, then over every polyad P' whose pair graphs lie in those of P and whose support passes the size threshold, each top color has relative density within δ of its relative density over P. The polyad P' may live over a different skeleton, for instance one refining the skeleton of P.

theorem TauCeti.Colored3Graph.IsTopRegularOverPolyad.of_pairSupport_subset {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_3} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ₂ V} {P : Polyad3 S} [DecidableEq κ] {H : Colored3Graph κ V} {δ : ℝ} {r : ℕ} {κ₂' : Type u_4} {S' : PairSkeleton3 κ₂' V} {P' : Polyad3 S'} (h₀₁ : P'.pairSupport₀₁ ⊆ P.pairSupport₀₁) (h₀₂ : P'.pairSupport₀₂ ⊆ P.pairSupport₀₂) (h₁₂ : P'.pairSupport₁₂ ⊆ P.pairSupport₁₂) (h : IsTopRegularOverPolyad P H δ r) (hr : 1 ≤ r) {α : ℝ} (hα : 0 < α) (hP' : α * ↑P.support.card ≤ ↑P'.support.card) : IsTopRegularOverPolyad P' H (max (2 * δ) (δ / α)) r

Slicing lemma. If H is (δ, r)-top-regular over P at a positive rank, then it is (max (2δ) (δ / α), r)-top-regular over every polyad P' whose pair graphs lie in those of P and whose support is at least an α-fraction of the support of P. The polyad P' may live over a different skeleton, so this is how top regularity passes to a refined lower skeleton.

theorem TauCeti.Colored3Graph.isTopRegularOverPolyad_const {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_3} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ₂ V} (P : Polyad3 S) [DecidableEq κ] {δ : ℝ} (r : ℕ) (c₀ : κ) (hδ : 0 < δ) : IsTopRegularOverPolyad P (const c₀) δ r

A constant coloring is (δ, r)-top-regular over every polyad, for every rank and every positive parameter.

def TauCeti.Colored3Graph.IsVertexBoxRegularOverPolyad {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_3} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ₂ V} (P : Polyad3 S) [DecidableEq κ] (H : Colored3Graph κ V) (ε : ℝ) : Prop

H is ε-vertex-box-regular over the polyad P when, for every top color c and all subsets of the three cells of P whose restriction of P keeps at least an ε-fraction of its support, the relative density of c on the restriction is within ε of the relative density of c over P. The restriction keeps the full pair graphs of P between the subsets.

theorem TauCeti.Colored3Graph.isVertexBoxRegularOverPolyad_iff {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_3} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ₂ V} {P : Polyad3 S} [DecidableEq κ] {H : Colored3Graph κ V} {ε : ℝ} : IsVertexBoxRegularOverPolyad P H ε ↔ ∀ (c : κ), ∀ a₀ ⊆ P.c₀, ∀ a₁ ⊆ P.c₁, ∀ a₂ ⊆ P.c₂, ε * ↑P.support.card ≤ ↑{x ∈ P.support | ↑x 0 ∈ a₀ ∧ ↑x 1 ∈ a₁ ∧ ↑x 2 ∈ a₂}.card → |↑(H.relDensityOn c ({x ∈ P.support | ↑x 0 ∈ a₀ ∧ ↑x 1 ∈ a₁ ∧ ↑x 2 ∈ a₂})) - ↑(H.relativeDensity c P)| ≤ ε

Unfolded form of Colored3Graph.IsVertexBoxRegularOverPolyad, with the restricted support written as a filter of the support of P.

theorem TauCeti.Colored3Graph.IsVertexBoxRegularOverPolyad.mono {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_3} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ₂ V} {P : Polyad3 S} [DecidableEq κ] {H : Colored3Graph κ V} {ε ε' : ℝ} (h : IsVertexBoxRegularOverPolyad P H ε) (hε : ε ≤ ε') : IsVertexBoxRegularOverPolyad P H ε'

Vertex-box regularity is monotone in its parameter.

theorem TauCeti.Colored3Graph.IsTopRegularOverPolyad.isVertexBoxRegularOverPolyad {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_3} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ₂ V} {P : Polyad3 S} [DecidableEq κ] {H : Colored3Graph κ V} {δ : ℝ} {r : ℕ} (h : IsTopRegularOverPolyad P H δ r) (hr : 1 ≤ r) : IsVertexBoxRegularOverPolyad P H δ

Top regularity at a positive rank implies vertex-box regularity: a vertex-box restriction is a single subpolyad.