Documentation

TauCeti.Combinatorics.Hypergraph.Colored.Density

Relative color densities and their stability under edits #

For a coloring H of the unordered triples of V, the relative density H.relDensityOn c supp of a color c over a finite support of injective triples is the fraction of the supported triples whose underlying unordered triple has color c. Colors are read through the underlying unordered triple, while the normalization counts the supported ordered injections, so a triple contributes once for each of its supported orderings, both to the count and to the normalization. The relative density is 0 on the empty support.

Relative densities lie between 0 and 1, and on a nonempty support the densities of all colors sum to one. Recoloring changes relDensityOn, multiplied by the support size, by at most the number of supported edited triples editedOn, defined in TauCeti.Combinatorics.Hypergraph.Colored.EditDiscrepancy.

Main definitions #

Main results #

source
def TauCeti.Colored3Graph.relDensityOn {κ : Type u_1} {V : Type u_2} [DecidableEq κ] (H : Colored3Graph κ V) (c : κ) (supp : Finset { x : Fin 3 → V // Function.Injective x }) :
ℚ

The relative density of the color c over a finite support of injective triples: the fraction of supported triples whose underlying unordered triple has color c. It is 0 on the empty support.

Instances For
    source
    theorem TauCeti.Colored3Graph.relDensityOn_def {κ : Type u_1} {V : Type u_2} [DecidableEq κ] (H : Colored3Graph κ V) (c : κ) (supp : Finset { x : Fin 3 → V // Function.Injective x }) :
    H.relDensityOn c supp = ↑{x ∈ supp | H.color (Set.powersetCard.ofFinEmb 3 V { toFun := ↑x, inj' := ⋯ }) = c}.card / ↑supp.card

    The relative density counts supported triples whose underlying triple has color c.

    source
    theorem TauCeti.Colored3Graph.relDensityOn_mul_card {κ : Type u_1} {V : Type u_2} [DecidableEq κ] (H : Colored3Graph κ V) (c : κ) (supp : Finset { x : Fin 3 → V // Function.Injective x }) :
    H.relDensityOn c supp * ↑supp.card = ↑{x ∈ supp | H.color (Set.powersetCard.ofFinEmb 3 V { toFun := ↑x, inj' := ⋯ }) = c}.card

    Multiplying a relative density by the support size recovers the color count, including when the support is empty.

    source
    theorem TauCeti.Colored3Graph.abs_relDensityOn_sub_mul_card_le_card_editedOn {κ : Type u_1} {V : Type u_2} [DecidableEq κ] (H H' : Colored3Graph κ V) (c : κ) (supp : Finset { x : Fin 3 → V // Function.Injective x }) :
    |H.relDensityOn c supp - H'.relDensityOn c supp| * ↑supp.card ≤ ↑(H.editedOn H' supp).card

    Recoloring changes a color count by at most the number of edited supported triples. The count-scaled form includes empty supports and does not require a finite palette.

    source
    theorem TauCeti.Colored3Graph.abs_relDensityOn_sub_le_div_of_card_editedOn_le {κ : Type u_1} {V : Type u_2} [DecidableEq κ] (H H' : Colored3Graph κ V) (c : κ) {A B : Finset { x : Fin 3 → V // Function.Injective x }} {ε η : ℝ} (hAB : A ⊆ B) (hε : 0 < ε) (hη : 0 ≤ η) (hsize : ε * ↑B.card ≤ ↑A.card) (hedit : ↑(H.editedOn H' B).card ≤ η * ↑B.card) :
    |↑(H.relDensityOn c A) - ↑(H'.relDensityOn c A)| ≤ η / ε

    Recoloring at most an η-fraction of B changes the density on any subsupport A carrying at least an ε-fraction of B by at most η / ε. Empty supports are allowed.

    source
    theorem TauCeti.Colored3Graph.relDensityOn_nonneg {κ : Type u_1} {V : Type u_2} [DecidableEq κ] (H : Colored3Graph κ V) (c : κ) (supp : Finset { x : Fin 3 → V // Function.Injective x }) :
    0 ≤ H.relDensityOn c supp

    Relative densities are nonnegative.

    source
    theorem TauCeti.Colored3Graph.relDensityOn_le_one {κ : Type u_1} {V : Type u_2} [DecidableEq κ] (H : Colored3Graph κ V) (c : κ) (supp : Finset { x : Fin 3 → V // Function.Injective x }) :
    H.relDensityOn c supp ≤ 1

    Relative densities are at most one.

    source
    theorem TauCeti.Colored3Graph.abs_relDensityOn_sub_mul_card_le_card_sdiff {κ : Type u_1} {V : Type u_2} [DecidableEq κ] [DecidableEq V] (H : Colored3Graph κ V) (c : κ) {A B : Finset { x : Fin 3 → V // Function.Injective x }} (hAB : A ⊆ B) :
    |H.relDensityOn c B - H.relDensityOn c A| * ↑B.card ≤ ↑(B \ A).card

    Shrinking a support to a subsupport changes the count-scaled density by at most the number of removed triples. Empty supports are allowed.

    source
    theorem TauCeti.Colored3Graph.abs_relDensityOn_sub_le_div_of_card_sdiff_le {κ : Type u_1} {V : Type u_2} [DecidableEq κ] [DecidableEq V] (H : Colored3Graph κ V) (c : κ) {A B : Finset { x : Fin 3 → V // Function.Injective x }} {N ε η : ℝ} (hAB : A ⊆ B) (hε : 0 < ε) (hη : 0 ≤ η) (hsize : ε * N ≤ ↑B.card) (hsdiff : ↑(B \ A).card ≤ η * N) :
    |↑(H.relDensityOn c B) - ↑(H.relDensityOn c A)| ≤ η / ε

    If at most η N triples are removed from a support B with ε N ≤ #B, the density of every color changes by at most η / ε. Empty supports are allowed.

    source
    @[simp]
    theorem TauCeti.Colored3Graph.relDensityOn_empty {κ : Type u_1} {V : Type u_2} [DecidableEq κ] (H : Colored3Graph κ V) (c : κ) :
    H.relDensityOn c ∅ = 0

    Every relative density over the empty support is 0.

    source
    theorem TauCeti.Colored3Graph.relDensityOn_const_self {κ : Type u_1} {V : Type u_2} [DecidableEq κ] {c : κ} {supp : Finset { x : Fin 3 → V // Function.Injective x }} (h : supp.Nonempty) :
    (const c).relDensityOn c supp = 1

    The relative density of the color of a constant coloring is one on a nonempty support.

    source
    @[simp]
    theorem TauCeti.Colored3Graph.relDensityOn_const_of_ne {κ : Type u_1} {V : Type u_2} [DecidableEq κ] {c₀ c : κ} (h : c₀ ≠ c) (supp : Finset { x : Fin 3 → V // Function.Injective x }) :
    (const c₀).relDensityOn c supp = 0

    The relative density of any other color of a constant coloring is zero.

    source
    theorem TauCeti.Colored3Graph.sum_relDensityOn {κ : Type u_1} {V : Type u_2} [DecidableEq κ] [Fintype κ] (H : Colored3Graph κ V) {supp : Finset { x : Fin 3 → V // Function.Injective x }} (h : supp.Nonempty) :
    ∑ c : κ, H.relDensityOn c supp = 1

    The relative densities of all colors sum to one on a nonempty support.