The polyad energy of a coloring of triples

For a coloring H of the unordered triples of a finite vertex type V with a finite palette, and a lower skeleton S (vertex cells and pair colors), every injective triple x lies in the support of exactly one polyad P_x = Polyad3.ofTriple S x. The polyad energy is the mean, over the |V| (|V| - 1) (|V| - 2) injective triples, of the squared relative color densities at their polyads: H.polyadEnergy S = (∑ x, ∑ c, d_H(c | P_x)²) / |V|.descFactorial 3. Grouping the triples by their polyads, it is the support-weighted sum ∑ P, ∑ c, (|P.support| / |V|.descFactorial 3) · d_H(c | P)² (Colored3Graph.polyadEnergy_eq_sum_polyad). This is the index of Rödl and Schacht, with one term for each top color; it is the arity-three analogue of the size-weighted graph energy SimpleGraph.weightedEnergy, with polyads in place of pairs of vertex cells.

The energy is the mean square of a conditional expectation. The relative density of c at the polyad of x is the average, over the support of that polyad, of the indicator that a triple has color c; hence weighting any function constant on polyad supports by these densities is the same as summing it over the triples of color c (Colored3Graph.sum_relativeDensity_ofTriple_mul). Consequently, if every polyad over a skeleton T lies inside a polyad over S (for instance when the cells and pair colors of T refine those of S, Polyad3.ofTriple_eq_ofTriple_of_le), the mean square deviation of the fine densities from the coarse ones is exactly the energy gap (Colored3Graph.polyadDensityDeviation_sq). So the energy does not decrease under refinement, it lies in [0, 1], and an energy gap of at most ε bounds the mean absolute deviation of each color density by √ε. These are the inputs of an energy-increment argument that regularizes a coloring over a refined lower skeleton.

Main definitions

• TauCeti.Colored3Graph.polyadEnergy: the polyad energy of a coloring over a lower skeleton.

Main results

• TauCeti.Colored3Graph.sum_relativeDensity_ofTriple_mul: relative densities at polyads act as conditional expectations of the color indicators.
• TauCeti.Colored3Graph.polyadEnergy_nonneg and TauCeti.Colored3Graph.polyadEnergy_le_one.
• TauCeti.Colored3Graph.polyadEnergy_eq_sum_polyad: the support-weighted sum over polyads.
• TauCeti.Colored3Graph.polyadDensityDeviation_sq: the refinement defect identity.
• TauCeti.Colored3Graph.polyadEnergy_mono_of_refines: refining the skeleton does not decrease the energy.
• TauCeti.Colored3Graph.polyadDensityDeviation_abs_le: the absolute-deviation bound from an energy gap.
• TauCeti.Colored3Graph.polyadEnergy_const: a constant coloring has energy one.

References

• V. Rödl and M. Schacht, Regular partitions of hypergraphs: regularity lemmas, Combin. Probab. Comput. 16 (2007), the index of a partition.
• The mass-weighted polyad energy and its monotonicity under merging cells appear as polyadEnergy and polyadEnergy_comp_le in the Lean library cameronfreer/regularity-lemmata (Hypergraph/PolyadEnergy.lean), for observables on ordered tuples and colorings of lower faces by Fin K.

theorem TauCeti.Colored3Graph.sum_relativeDensity_ofTriple_mul {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_4} [Fintype V] [DecidableEq V] [DecidableEq κ] (H : Colored3Graph κ V) {S : PairSkeleton3 κ₂ V} (c : κ) (φ : { x : Fin 3 → V // Function.Injective x } → ℝ) (hφ : ∀ (x y : { x : Fin 3 → V // Function.Injective x }), Polyad3.ofTriple S x = Polyad3.ofTriple S y → φ x = φ y) : ∑ x : { x : Fin 3 → V // Function.Injective x }, ↑(H.relativeDensity c (Polyad3.ofTriple S x)) * φ x = ∑ x : { x : Fin 3 → V // Function.Injective x } with H.color (Set.powersetCard.ofFinEmb 3 V { toFun := ↑x, inj' := ⋯ }) = c, φ x

Relative densities are conditional expectations. If φ is constant on the support of each polyad over S, then weighting φ at each injective triple by the relative density of c at the polyad of that triple gives the sum of φ over the triples of color c.

noncomputable def TauCeti.Colored3Graph.polyadEnergy {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_4} [Fintype V] [DecidableEq V] [DecidableEq κ] (H : Colored3Graph κ V) [Fintype κ] (S : PairSkeleton3 κ₂ V) : ℝ

The polyad energy of a coloring H over a lower skeleton S: the mean, over the injective triples x, of ∑ c, d_H(c | P_x)², where P_x is the polyad of x over S and d_H(c | P) = H.relativeDensity c P. It is the support-weighted sum of the squared relative densities over all polyads (Colored3Graph.polyadEnergy_eq_sum_polyad), and it is 0 when V has fewer than three vertices.

theorem TauCeti.Colored3Graph.polyadEnergy_def {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_4} [Fintype V] [DecidableEq V] [DecidableEq κ] (H : Colored3Graph κ V) [Fintype κ] (S : PairSkeleton3 κ₂ V) : H.polyadEnergy S = (∑ x : { x : Fin 3 → V // Function.Injective x }, ∑ c : κ, ↑(H.relativeDensity c (Polyad3.ofTriple S x)) ^ 2) / ↑((Fintype.card V).descFactorial 3)

Unfolding lemma for Colored3Graph.polyadEnergy.

theorem TauCeti.Colored3Graph.polyadEnergy_nonneg {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_4} [Fintype V] [DecidableEq V] [DecidableEq κ] (H : Colored3Graph κ V) [Fintype κ] (S : PairSkeleton3 κ₂ V) : 0 ≤ H.polyadEnergy S

The polyad energy is nonnegative.

theorem TauCeti.Colored3Graph.polyadEnergy_le_one {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_4} [Fintype V] [DecidableEq V] [DecidableEq κ] (H : Colored3Graph κ V) [Fintype κ] (S : PairSkeleton3 κ₂ V) : H.polyadEnergy S ≤ 1

The polyad energy is at most one, since at each triple the relative densities of all colors lie in [0, 1] and sum to one.

theorem TauCeti.Colored3Graph.polyadEnergy_eq_sum_polyad {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_4} [Fintype V] [DecidableEq V] [DecidableEq κ] (H : Colored3Graph κ V) [Fintype κ] (S : PairSkeleton3 κ₂ V) [Fintype κ₂] : H.polyadEnergy S = ∑ P : Polyad3 S, ∑ c : κ, ↑P.support.card / ↑((Fintype.card V).descFactorial 3) * ↑(H.relativeDensity c P) ^ 2

The polyad energy is the sum over all polyads P and colors c of (|P.support| / |V|.descFactorial 3) · d_H(c | P)².

Refinement

theorem TauCeti.Colored3Graph.polyadDensityDeviation_sq {κ : Type u_1} {κ₂ : Type u_2} {κ₂' : Type u_3} {V : Type u_4} [Fintype V] [DecidableEq V] [DecidableEq κ] (H : Colored3Graph κ V) [Fintype κ] {S : PairSkeleton3 κ₂ V} {T : PairSkeleton3 κ₂' V} (h : ∀ (x y : { x : Fin 3 → V // Function.Injective x }), Polyad3.ofTriple T x = Polyad3.ofTriple T y → Polyad3.ofTriple S x = Polyad3.ofTriple S y) : (∑ x : { x : Fin 3 → V // Function.Injective x }, ∑ c : κ, (↑(H.relativeDensity c (Polyad3.ofTriple T x)) - ↑(H.relativeDensity c (Polyad3.ofTriple S x))) ^ 2) / ↑((Fintype.card V).descFactorial 3) = H.polyadEnergy T - H.polyadEnergy S

Refinement defect identity. If every polyad over T lies in a polyad over S, the mean over the injective triples of the squared deviations of the relative densities at the fine polyads from those at the coarse polyads, summed over colors, equals the energy gap.

theorem TauCeti.Colored3Graph.polyadEnergy_mono_of_refines {κ : Type u_1} {κ₂ : Type u_2} {κ₂' : Type u_3} {V : Type u_4} [Fintype V] [DecidableEq V] [DecidableEq κ] (H : Colored3Graph κ V) [Fintype κ] {S : PairSkeleton3 κ₂ V} {T : PairSkeleton3 κ₂' V} (h : ∀ (x y : { x : Fin 3 → V // Function.Injective x }), Polyad3.ofTriple T x = Polyad3.ofTriple T y → Polyad3.ofTriple S x = Polyad3.ofTriple S y) : H.polyadEnergy S ≤ H.polyadEnergy T

Monotonicity under refinement. If every polyad over T lies in a polyad over S, the energy over T is at least the energy over S.

theorem TauCeti.Colored3Graph.polyadDensityDeviation_abs_le {κ : Type u_1} {κ₂ : Type u_2} {κ₂' : Type u_3} {V : Type u_4} [Fintype V] [DecidableEq V] [DecidableEq κ] (H : Colored3Graph κ V) [Fintype κ] {S : PairSkeleton3 κ₂ V} {T : PairSkeleton3 κ₂' V} (h : ∀ (x y : { x : Fin 3 → V // Function.Injective x }), Polyad3.ofTriple T x = Polyad3.ofTriple T y → Polyad3.ofTriple S x = Polyad3.ofTriple S y) {ε : ℝ} (hgap : H.polyadEnergy T - H.polyadEnergy S ≤ ε) (c : κ) : ∑ x : { x : Fin 3 → V // Function.Injective x }, |↑(H.relativeDensity c (Polyad3.ofTriple T x)) - ↑(H.relativeDensity c (Polyad3.ofTriple S x))| ≤ √ε * ↑((Fintype.card V).descFactorial 3)

Energy gap controls absolute deviation. If every polyad over T lies in a polyad over S and the energy gap is at most ε, then for each color c the relative densities of c at the fine and at the coarse polyads differ by at most √ε on average over the injective triples.

theorem TauCeti.Colored3Graph.polyadEnergy_const {κ : Type u_1} {κ₂ : Type u_2} {V : Type u_4} [Fintype V] [DecidableEq V] [DecidableEq κ] [Fintype κ] (S : PairSkeleton3 κ₂ V) (c₀ : κ) (hV : 3 ≤ Fintype.card V) : (const c₀).polyadEnergy S = 1

A constant coloring has polyad energy one over every lower skeleton, once there are injective triples: each triple sees density one for the constant color and zero for the others.