Documentation

TauCeti.Combinatorics.Hypergraph.PairColor.Energy

The energy of a vertex partition for a pair-color system #

For a pair-color system S with a finite palette on a finite vertex type V, and a partition P of the vertices, every ordered distinct pair (u, v) lies in the block P.part u ×ˢ P.part v. The energy of P is the mean, over the |V| (|V| - 1) ordered distinct pairs, of the squared color densities of the blocks through them: S.energy P = (∑ (u, v), ∑ c, d_c(P.part u, P.part v)²) / |V| (|V| - 1), where d_c = pairColorDensity S c is taken among ordered distinct pairs. This is the index of a vertex partition for a coloring of pairs, with one term for each color; it is the pair-level analogue of the polyad energy TauCeti.Colored3Graph.polyadEnergy. Diagonal blocks A ×ˢ A are included, with their densities taken among distinct pairs.

The block density of c at (u, v) is the average over the block of the indicator that a pair has color c. Hence weighting any function constant on blocks by these densities is the same as summing it over the pairs of color c (TauCeti.PairColorSystem.sum_pairColorDensity_part_mul). Consequently, for a refinement Q ≤ P, the mean square deviation of the fine block densities from the coarse ones is exactly the energy gap (TauCeti.PairColorSystem.sum_sq_pairColorDensity_sub_div_eq_energy_sub), so the energy does not decrease under refinement and lies in [0, 1]. Since each block contributes a term in [0, 1], moving a few points between parts changes the energy only a little, even when neither partition refines the other.

If a family of coarse blocks has rectangles X ×ˢ Y inside them whose sides are unions of parts of Q, each carrying a positive proportion of its block and a color density far from the block density, then the energy of Q exceeds that of P by a definite amount (TauCeti.PairColorSystem.energy_increment_of_witnesses). Applied to the witnesses of irregular pairs of parts, this is the energy increment of the regularity lemma for pair-color systems.

Main definitions #

Main results #

References #

source
theorem TauCeti.PairColorSystem.sum_pairColorDensity_part_mul {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : PairColorSystem κ V) [DecidableEq κ] (P : Finpartition Finset.univ) (c : κ) (φ : V × V → ℝ) (hφ : ∀ (x y : V × V), P.part x.1 = P.part y.1 → P.part x.2 = P.part y.2 → φ x = φ y) :
∑ p ∈ Finset.univ.offDiag, ↑(pairColorDensity S c (P.part p.1) (P.part p.2)) * φ p = ∑ p ∈ Finset.univ.offDiag with S.colorOfPair p.1 p.2 = some c, φ p

Block densities are conditional expectations. If φ is constant on each block P.part u ×ˢ P.part v, then weighting φ at each ordered distinct pair by the density of c on the block through it gives the sum of φ over the pairs of color c.

source
theorem TauCeti.PairColorSystem.sum_pairColorDensity_part_eq_card {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : PairColorSystem κ V) {Q : Finpartition Finset.univ} [DecidableEq κ] {X Y : Finset V} (hX : ∀ C ∈ Q.parts, C ⊆ X ∨ Disjoint C X) (hY : ∀ C ∈ Q.parts, C ⊆ Y ∨ Disjoint C Y) (c : κ) :
∑ p ∈ X ×ˢ Y with p.1 ≠ p.2, ↑(pairColorDensity S c (Q.part p.1) (Q.part p.2)) = ↑{p ∈ X ×ˢ Y | S.colorOfPair p.1 p.2 = some c}.card

On a rectangle X ×ˢ Y whose sides are unions of parts of Q, the block densities of c sum, over the ordered distinct pairs of the rectangle, to the number of its pairs of color c.

source
theorem TauCeti.PairColorSystem.card_mul_sq_pairColorDensity_sub_le_sum {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : PairColorSystem κ V) {Q : Finpartition Finset.univ} {X Y : Finset V} (hX : ∀ C ∈ Q.parts, C ⊆ X ∨ Disjoint C X) (hY : ∀ C ∈ Q.parts, C ⊆ Y ∨ Disjoint C Y) (c : κ) (a : ℝ) :
↑{p ∈ X ×ˢ Y | p.1 ≠ p.2}.card * (↑(pairColorDensity S c X Y) - a) ^ 2 ≤ ∑ p ∈ X ×ˢ Y with p.1 ≠ p.2, (↑(pairColorDensity S c (Q.part p.1) (Q.part p.2)) - a) ^ 2

Cauchy–Schwarz on a resolved rectangle. For a rectangle X ×ˢ Y whose sides are unions of parts of Q, the squared deviation of the density of c on the rectangle from any real number a, multiplied by the number of ordered distinct pairs of the rectangle, is at most the sum over those pairs of the squared deviations of the block densities of Q from a.

source
noncomputable def TauCeti.PairColorSystem.energy {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : PairColorSystem κ V) [Fintype κ] (P : Finpartition Finset.univ) :
ℝ

The energy of a partition P of the vertices for the pair-color system S: the mean, over the ordered distinct pairs (u, v), of ∑ c, d_c(P.part u, P.part v)², where d_c = pairColorDensity S c is the density of c among the ordered distinct pairs of a block. It is 0 when V has fewer than two vertices.

Instances For
    source
    theorem TauCeti.PairColorSystem.energy_def {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : PairColorSystem κ V) [Fintype κ] (P : Finpartition Finset.univ) :
    S.energy P = (∑ p ∈ Finset.univ.offDiag, ∑ c : κ, ↑(pairColorDensity S c (P.part p.1) (P.part p.2)) ^ 2) / ↑Finset.univ.offDiag.card

    Unfolding lemma for TauCeti.PairColorSystem.energy.

    source
    theorem TauCeti.PairColorSystem.energy_nonneg {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : PairColorSystem κ V) [Fintype κ] (P : Finpartition Finset.univ) :
    0 ≤ S.energy P

    The energy is nonnegative.

    source
    theorem TauCeti.PairColorSystem.sum_sq_pairColorDensity_le_one {κ : Type u_1} {V : Type u_2} (S : PairColorSystem κ V) [Fintype κ] (s t : Finset V) :
    ∑ c : κ, ↑(pairColorDensity S c s t) ^ 2 ≤ 1

    The squared color densities of a pair of sets sum to at most one, since the densities lie in [0, 1] and sum to at most one.

    source
    theorem TauCeti.PairColorSystem.energy_le_one {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : PairColorSystem κ V) [Fintype κ] (P : Finpartition Finset.univ) :
    S.energy P ≤ 1

    The energy is at most one, since on each block the color densities lie in [0, 1] and sum to at most one.

    source
    theorem TauCeti.PairColorSystem.abs_energy_sub_energy_le {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : PairColorSystem κ V) {P Q : Finpartition Finset.univ} [Fintype κ] (B : Finset V) (hB : ∀ u ∉ B, P.part u = Q.part u) :
    |S.energy P - S.energy Q| ≤ 2 * ↑B.card * ↑(Fintype.card V) / ↑Finset.univ.offDiag.card

    Energy is stable under moving few points. If two partitions have the same part through every point outside a set B, then their energies differ by at most 2 #B |V| divided by the number |V| (|V| - 1) of ordered distinct pairs: only the blocks through pairs meeting B change, and each contributes a term in [0, 1].

    Refinement #

    source
    theorem TauCeti.PairColorSystem.sum_sq_pairColorDensity_sub_div_eq_energy_sub {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : PairColorSystem κ V) {P Q : Finpartition Finset.univ} [Fintype κ] (h : Q ≤ P) :
    (∑ p ∈ Finset.univ.offDiag, ∑ c : κ, (↑(pairColorDensity S c (Q.part p.1) (Q.part p.2)) - ↑(pairColorDensity S c (P.part p.1) (P.part p.2))) ^ 2) / ↑Finset.univ.offDiag.card = S.energy Q - S.energy P

    Refinement defect identity. For a refinement Q ≤ P, the mean over the ordered distinct pairs of the squared deviations of the block densities of Q from those of P, summed over colors, equals the energy gap.

    source
    theorem TauCeti.PairColorSystem.energy_mono_of_refines {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : PairColorSystem κ V) {P Q : Finpartition Finset.univ} [Fintype κ] (h : Q ≤ P) :
    S.energy P ≤ S.energy Q

    Monotonicity under refinement. If Q refines P, the energy of Q is at least the energy of P.

    source
    theorem TauCeti.PairColorSystem.mul_card_le_sum_sq_pairColorDensity_sub_of_witness {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : PairColorSystem κ V) {P Q : Finpartition Finset.univ} [Fintype κ] {A B X Y : Finset V} (hA : A ∈ P.parts) (hB : B ∈ P.parts) (hXA : X ⊆ A) (hYB : Y ⊆ B) (hX : ∀ C ∈ Q.parts, C ⊆ X ∨ Disjoint C X) (hY : ∀ C ∈ Q.parts, C ⊆ Y ∨ Disjoint C Y) (c : κ) {α δ : ℝ} (hδ : 0 ≤ δ) (hsize : α * ↑{p ∈ A ×ˢ B | p.1 ≠ p.2}.card ≤ ↑{p ∈ X ×ˢ Y | p.1 ≠ p.2}.card) (hdev : δ ≤ |↑(pairColorDensity S c X Y) - ↑(pairColorDensity S c A B)|) :
    α * δ ^ 2 * ↑{p ∈ A ×ˢ B | p.1 ≠ p.2}.card ≤ ∑ x ∈ A ×ˢ B with x.1 ≠ x.2, ∑ k : κ, (↑(pairColorDensity S k (Q.part x.1) (Q.part x.2)) - ↑(pairColorDensity S k (P.part x.1) (P.part x.2))) ^ 2

    A resolved witness forces a gain on its block. Let A ×ˢ B be a block of parts of P, and let X ×ˢ Y ⊆ A ×ˢ B be a rectangle whose sides are unions of parts of Q. If the rectangle has at least an α-fraction of the ordered distinct pairs of the block, and its density of c is at least δ away from that of the block, then the squared deviations of the block densities of Q from those of P, summed over the colors and over the ordered distinct pairs of the block, total at least α δ² times the number of those pairs.

    source
    theorem TauCeti.PairColorSystem.energy_increment_of_witnesses {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] (S : PairColorSystem κ V) {P Q : Finpartition Finset.univ} [Fintype κ] (h : Q ≤ P) (B : Finset (Finset V × Finset V)) (hB : ∀ AB ∈ B, AB.1 ∈ P.parts ∧ AB.2 ∈ P.parts) (c : Finset V × Finset V → κ) (X Y : Finset V × Finset V → Finset V) {α δ : ℝ} (hδ : 0 ≤ δ) (hXsub : ∀ AB ∈ B, X AB ⊆ AB.1) (hYsub : ∀ AB ∈ B, Y AB ⊆ AB.2) (hX : ∀ AB ∈ B, ∀ C ∈ Q.parts, C ⊆ X AB ∨ Disjoint C (X AB)) (hY : ∀ AB ∈ B, ∀ C ∈ Q.parts, C ⊆ Y AB ∨ Disjoint C (Y AB)) (hsize : ∀ AB ∈ B, α * ↑{p ∈ AB.1 ×ˢ AB.2 | p.1 ≠ p.2}.card ≤ ↑{p ∈ X AB ×ˢ Y AB | p.1 ≠ p.2}.card) (hdev : ∀ AB ∈ B, δ ≤ |↑(pairColorDensity S (c AB) (X AB) (Y AB)) - ↑(pairColorDensity S (c AB) AB.1 AB.2)|) :
    α * δ ^ 2 * ((∑ AB ∈ B, ↑{p ∈ AB.1 ×ˢ AB.2 | p.1 ≠ p.2}.card) / ↑Finset.univ.offDiag.card) ≤ S.energy Q - S.energy P

    Resolved witnesses force an energy gain. Let Q refine P, and let B be a family of pairs of parts of P. For each block A ×ˢ B in the family choose a color and a rectangle X ×ˢ Y ⊆ A ×ˢ B whose sides are unions of parts of Q. If each rectangle has at least an α-fraction of the ordered distinct pairs of its block, and a color density at least δ away from the density on the block, then the energy gap is at least α δ² times the proportion of ordered distinct pairs lying in the blocks of the family.