Regularity of pair colors and of the lower skeleton

For a pair-color system S and two vertex sets s and t, S.IsRegularPair ε s t says that the density of every palette color on (s, t) is within ε of its density on every pair of subsets s' ⊆ s, t' ⊆ t with ε * #s ≤ #s' and ε * #t ≤ #t'. The condition is coordinatewise: each color is controlled separately. Densities are taken among ordered distinct pairs, so the condition is meaningful also when s = t.

For disjoint s and t, an ε-regular pair has small rectangle discrepancy: for every color c, the number of pairs of color c in s' ×ˢ t' is within ε |s| |t| of the count d_c(s, t) |s'| |t'| predicted by the density on (s, t). The same bound holds when the indicator of c is tested against functions with values in [0, 1]; this is the input of counting lemmas. Both follow the corresponding bounds for uniform pairs of a graph, SimpleGraph.IsUniform.abs_card_interedges_sub_le and SimpleGraph.IsUniform.abs_sum_sum_mul_sub_le.

A PairSkeleton3 bundles a partition of the host into vertex cells with a pair-color system. It is the lower skeleton over which triple densities and their regularity are measured. PairSkeleton3.IsPairColorRegular S ε asks for ε-regularity of every ordered pair of vertex cells, diagonal pairs included; PairSkeleton3.LowerSkeletonRegular S F evaluates an error schedule F : ℕ → ℝ at the lower complexity, the number of vertex cells plus the palette size.

Main declarations

• TauCeti.PairColorSystem.IsRegularPair: coordinatewise ε-regularity of a pair of sets.
• TauCeti.PairColorSystem.isRegularPair_comm: regularity is symmetric in the two sets.
• TauCeti.PairColorSystem.IsRegularPair.of_subset: the slicing lemma; subsets of at least an α-fraction of the sizes form a max (2ε) (ε / α)-regular pair.
• TauCeti.PairColorSystem.IsRegularPair.abs_card_filter_colorOfPair_sub_le: rectangle discrepancy of a regular pair of disjoint sets.
• TauCeti.PairColorSystem.IsRegularPair.abs_sum_sum_mul_sub_le: the same bound for tests with values in [0, 1].
• TauCeti.PairSkeleton3: vertex cells together with a pair-color system.
• TauCeti.PairSkeleton3.IsPairColorRegular: every pair of vertex cells is regular.
• TauCeti.PairSkeleton3.isPairColorRegular_bot: the partition into singletons is regular.
• TauCeti.PairSkeleton3.LowerSkeletonRegular: regularity at the lower complexity.
• TauCeti.PairSkeleton3.relabel: renaming the pair palette along an equivalence.

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 slicing lemma).
• V. Rödl, M. Schacht, Regular partitions of hypergraphs: regularity lemmas, Combin. Probab. Comput. 16 (2007).
• C. Terry, Growth of regular partitions 4: strong regularity and the pairs partition, arXiv:2404.02030.

def TauCeti.PairColorSystem.IsRegularPair {κ : Type u_1} {V : Type u_2} (S : PairColorSystem κ V) (ε : ℝ) (s t : Finset V) : Prop

A pair (s, t) of vertex sets is ε-regular for the pair-color system S when, for every color, its density on any s' ⊆ s and t' ⊆ t with ε * #s ≤ #s' and ε * #t ≤ #t' is within ε of its density on (s, t). Each color is controlled separately.

theorem TauCeti.PairColorSystem.isRegularPair_iff {κ : Type u_1} {V : Type u_2} {S : PairColorSystem κ V} {ε : ℝ} {s t : Finset V} : S.IsRegularPair ε s t ↔ ∀ (c : κ), ∀ s' ⊆ s, ∀ t' ⊆ t, ε * ↑s.card ≤ ↑s'.card → ε * ↑t.card ≤ ↑t'.card → |↑(pairColorDensity S c s' t') - ↑(pairColorDensity S c s t)| ≤ ε

Unfolded form of PairColorSystem.IsRegularPair.

theorem TauCeti.PairColorSystem.IsRegularPair.mono {κ : Type u_1} {V : Type u_2} {S : PairColorSystem κ V} {ε ε' : ℝ} {s t : Finset V} (h : S.IsRegularPair ε s t) (hε : ε ≤ ε') : S.IsRegularPair ε' s t

Regularity is monotone in its parameter.

theorem TauCeti.PairColorSystem.isRegularPair_of_one_le {κ : Type u_1} {V : Type u_2} {S : PairColorSystem κ V} {ε : ℝ} {s t : Finset V} (hε : 1 ≤ ε) : S.IsRegularPair ε s t

Every pair is ε-regular once 1 ≤ ε, since densities lie in [0, 1].

theorem TauCeti.PairColorSystem.IsRegularPair.symm {κ : Type u_1} {V : Type u_2} {S : PairColorSystem κ V} {ε : ℝ} {s t : Finset V} (h : S.IsRegularPair ε s t) : S.IsRegularPair ε t s

Exchanging the two sets preserves regularity.

theorem TauCeti.PairColorSystem.isRegularPair_comm {κ : Type u_1} {V : Type u_2} {S : PairColorSystem κ V} {ε : ℝ} {s t : Finset V} : S.IsRegularPair ε s t ↔ S.IsRegularPair ε t s

Regularity is symmetric in the two sets.

theorem TauCeti.PairColorSystem.IsRegularPair.nonneg {κ : Type u_1} {V : Type u_2} {S : PairColorSystem κ V} {ε : ℝ} {s t : Finset V} [Nonempty κ] (h : S.IsRegularPair ε s t) : 0 ≤ ε

A regular pair for a nonempty palette has a nonnegative parameter: for a negative parameter, the empty subsets pass the size thresholds.

theorem TauCeti.PairColorSystem.IsRegularPair.of_subset {κ : Type u_1} {V : Type u_2} {S : PairColorSystem κ V} {ε : ℝ} {s t : Finset V} (h : S.IsRegularPair ε s t) {s₁ t₁ : Finset V} (hs : s₁ ⊆ s) (ht : t₁ ⊆ t) {α : ℝ} (hα : 0 < α) (hs₁ : α * ↑s.card ≤ ↑s₁.card) (ht₁ : α * ↑t.card ≤ ↑t₁.card) : S.IsRegularPair (max (2 * ε) (ε / α)) s₁ t₁

Slicing lemma. If (s, t) is ε-regular, then every pair of subsets s₁ ⊆ s and t₁ ⊆ t of at least an α-fraction of the sizes of s and t is max (2ε) (ε / α)-regular.

theorem TauCeti.PairColorSystem.isRegularPair_singleton {κ : Type u_1} {V : Type u_2} {S : PairColorSystem κ V} {ε : ℝ} (hε : 0 < ε) (u v : V) : S.IsRegularPair ε {u} {v}

Two singletons form an ε-regular pair for every ε > 0.

theorem TauCeti.PairColorSystem.IsRegularPair.abs_card_filter_colorOfPair_sub_le {κ : Type u_1} {V : Type u_2} {S : PairColorSystem κ V} {ε : ℝ} {s t : Finset V} [DecidableEq κ] {s' t' : Finset V} {c : κ} (h : S.IsRegularPair ε s t) (hst : Disjoint s t) (hs' : s' ⊆ s) (ht' : t' ⊆ t) : |↑{p ∈ s' ×ˢ t' | S.colorOfPair p.1 p.2 = some c}.card - ↑(pairColorDensity S c s t) * ↑s'.card * ↑t'.card| ≤ ε * ↑s.card * ↑t.card

Rectangle discrepancy of a regular pair. If (s, t) is an ε-regular pair of disjoint sets, then for all s' ⊆ s and t' ⊆ t the number of pairs of color c in s' ×ˢ t' is within ε |s| |t| of the count d_c(s, t) |s'| |t'| predicted by the density of c on (s, t).

theorem TauCeti.PairColorSystem.IsRegularPair.abs_sum_sum_mul_sub_le {κ : Type u_1} {V : Type u_2} {S : PairColorSystem κ V} {ε : ℝ} {s t : Finset V} [DecidableEq κ] (h : S.IsRegularPair ε s t) (hst : Disjoint s t) (c : κ) {f g : V → ℝ} (hf₀ : ∀ x ∈ s, 0 ≤ f x) (hf₁ : ∀ x ∈ s, f x ≤ 1) (hg₀ : ∀ y ∈ t, 0 ≤ g y) (hg₁ : ∀ y ∈ t, g y ≤ 1) : |∑ x ∈ s, ∑ y ∈ t, f x * g y * ((if S.colorOfPair x y = some c then 1 else 0) - ↑(pairColorDensity S c s t))| ≤ ε * ↑s.card * ↑t.card

Test-function discrepancy of a regular pair. If (s, t) is an ε-regular pair of disjoint sets, then testing the deviation of the indicator of a color c from its density on (s, t) against functions f on s and g on t with values in [0, 1] gives at most ε |s| |t|.

structure TauCeti.PairSkeleton3 (κ : Type u_3) (V : Type u_4) [Fintype V] [DecidableEq V] : Type (max u_3 u_4)

The lower skeleton of an arity-three complex: a partition of the host into vertex cells, together with a coherent coloring of the ordered distinct vertex pairs.

• vertexPart : Finpartition Finset.univ

  The partition of the host into vertex cells.

• pairColors : PairColorSystem κ V

  The coloring of ordered distinct vertex pairs.

theorem TauCeti.PairSkeleton3.ext {κ : Type u_3} {V : Type u_4} {inst✝ : Fintype V} {inst✝¹ : DecidableEq V} {x y : PairSkeleton3 κ V} (vertexPart : x.vertexPart = y.vertexPart) (pairColors : x.pairColors = y.pairColors) : x = y

theorem TauCeti.PairSkeleton3.ext_iff {κ : Type u_3} {V : Type u_4} {inst✝ : Fintype V} {inst✝¹ : DecidableEq V} {x y : PairSkeleton3 κ V} : x = y ↔ x.vertexPart = y.vertexPart ∧ x.pairColors = y.pairColors

def TauCeti.PairSkeleton3.IsPairColorRegular {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : PairSkeleton3 κ V) (ε : ℝ) : Prop

The lower skeleton is ε-regular when every ordered pair of its vertex cells, including a cell paired with itself, is ε-regular for its pair colors. The test subsets range over the subsets of the actual cells, tying pair regularity to the skeleton.

theorem TauCeti.PairSkeleton3.isPairColorRegular_iff {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {ε : ℝ} : S.IsPairColorRegular ε ↔ ∀ (c : κ), ∀ A ∈ S.vertexPart.parts, ∀ B ∈ S.vertexPart.parts, ∀ A' ⊆ A, ∀ B' ⊆ B, ε * ↑A.card ≤ ↑A'.card → ε * ↑B.card ≤ ↑B'.card → |↑(pairColorDensity S.pairColors c A' B') - ↑(pairColorDensity S.pairColors c A B)| ≤ ε

Unfolded form of PairSkeleton3.IsPairColorRegular: for every color and every ordered pair of vertex cells, the color density is stable on all large enough subcells.

theorem TauCeti.PairSkeleton3.IsPairColorRegular.isRegularPair {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {ε : ℝ} (h : S.IsPairColorRegular ε) {A B : Finset V} (hA : A ∈ S.vertexPart.parts) (hB : B ∈ S.vertexPart.parts) : S.pairColors.IsRegularPair ε A B

In a regular lower skeleton, every ordered pair of vertex cells is a regular pair.

theorem TauCeti.PairSkeleton3.IsPairColorRegular.mono {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {ε ε' : ℝ} (h : S.IsPairColorRegular ε) (hε : ε ≤ ε') : S.IsPairColorRegular ε'

Pair-color regularity is monotone in its parameter.

theorem TauCeti.PairSkeleton3.isPairColorRegular_of_one_le {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {ε : ℝ} (hε : 1 ≤ ε) : S.IsPairColorRegular ε

Every lower skeleton is ε-regular once 1 ≤ ε.

theorem TauCeti.PairSkeleton3.IsPairColorRegular.nonneg {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {ε : ℝ} [Nonempty κ] [Nonempty V] (h : S.IsPairColorRegular ε) : 0 ≤ ε

A regular lower skeleton on a nonempty host with a nonempty palette has a nonnegative parameter.

theorem TauCeti.PairSkeleton3.isPairColorRegular_bot {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {ε : ℝ} (hε : 0 < ε) (C : PairColorSystem κ V) : { vertexPart := ⊥, pairColors := C }.IsPairColorRegular ε

A lower skeleton whose vertex cells are the singletons is ε-regular for every ε > 0.

def TauCeti.PairSkeleton3.LowerSkeletonRegular {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : PairSkeleton3 κ V) [Fintype κ] (F : ℕ → ℝ) : Prop

Lower-skeleton regularity for an error schedule F : ℕ → ℝ: pair-color regularity at the parameter F takes at the lower complexity, the number of vertex cells plus the palette size.

theorem TauCeti.PairSkeleton3.lowerSkeletonRegular_iff {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} [Fintype κ] {F : ℕ → ℝ} : S.LowerSkeletonRegular F ↔ S.IsPairColorRegular (F (S.vertexPart.parts.card + Fintype.card κ))

Unfolded form of PairSkeleton3.LowerSkeletonRegular.

theorem TauCeti.PairSkeleton3.LowerSkeletonRegular.isPairColorRegular {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {ε : ℝ} [Fintype κ] {F : ℕ → ℝ} (h : S.LowerSkeletonRegular F) (hε : F (S.vertexPart.parts.card + Fintype.card κ) ≤ ε) : S.IsPairColorRegular ε

A lower skeleton regular for a schedule is regular at every parameter dominating the scheduled one.

def TauCeti.PairSkeleton3.relabel {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : PairSkeleton3 κ V) {κ' : Type u_3} (e : κ ≃ κ') : PairSkeleton3 κ' V

Rename the pair palette of a lower skeleton along an equivalence, keeping its vertex cells.

@[simp]

theorem TauCeti.PairSkeleton3.relabel_vertexPart {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {κ' : Type u_3} (e : κ ≃ κ') : (S.relabel e).vertexPart = S.vertexPart

@[simp]

theorem TauCeti.PairSkeleton3.relabel_pairColors {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {κ' : Type u_3} (e : κ ≃ κ') : (S.relabel e).pairColors = S.pairColors.relabel e