Relative color densities over polyads

H.relativeDensity c P is the relative density H.relDensityOn c P.support of the color c over the computed support of the polyad P: the fraction of the supported role-ordered injective triples whose underlying unordered triple has color c. It inherits the bounds, the value 0 on an empty support, and the sum to one over colors on a nonempty support.

Main definitions

• TauCeti.Colored3Graph.relativeDensity: the relative density of a color over a polyad.

Main results

• TauCeti.Colored3Graph.sum_relativeDensity: over a polyad with nonempty support, the densities of all colors sum to one.
• TauCeti.Colored3Graph.relDensityOn_sub_mul_card_eq_sum_inter_support: the count-scaled deviation of a color density on a set of triples splits over the polyads of any skeleton.

noncomputable def TauCeti.Colored3Graph.relativeDensity {κ : Type u_1} {V : Type u_2} [DecidableEq κ] [Fintype V] [DecidableEq V] {κ₂ : Type u_3} {S : PairSkeleton3 κ₂ V} (H : Colored3Graph κ V) (c : κ) (P : Polyad3 S) : ℚ

The relative density of the color c over the support of a polyad.

theorem TauCeti.Colored3Graph.relativeDensity_def {κ : Type u_1} {V : Type u_2} [DecidableEq κ] [Fintype V] [DecidableEq V] {κ₂ : Type u_3} {S : PairSkeleton3 κ₂ V} (H : Colored3Graph κ V) (c : κ) (P : Polyad3 S) : H.relativeDensity c P = H.relDensityOn c P.support

The relative density over a polyad is the relative density over its support.

theorem TauCeti.Colored3Graph.relativeDensity_nonneg {κ : Type u_1} {V : Type u_2} [DecidableEq κ] [Fintype V] [DecidableEq V] {κ₂ : Type u_3} {S : PairSkeleton3 κ₂ V} (H : Colored3Graph κ V) (c : κ) (P : Polyad3 S) : 0 ≤ H.relativeDensity c P

Relative densities over a polyad are nonnegative.

theorem TauCeti.Colored3Graph.relativeDensity_le_one {κ : Type u_1} {V : Type u_2} [DecidableEq κ] [Fintype V] [DecidableEq V] {κ₂ : Type u_3} {S : PairSkeleton3 κ₂ V} (H : Colored3Graph κ V) (c : κ) (P : Polyad3 S) : H.relativeDensity c P ≤ 1

Relative densities over a polyad are at most one.

theorem TauCeti.Colored3Graph.abs_relDensityOn_sub_relativeDensity_le_one {κ : Type u_1} {V : Type u_2} [DecidableEq κ] [Fintype V] [DecidableEq V] {κ₂ : Type u_3} {S : PairSkeleton3 κ₂ V} (H : Colored3Graph κ V) (c : κ) (s : Finset { x : Fin 3 → V // Function.Injective x }) (P : Polyad3 S) : |↑(H.relDensityOn c s) - ↑(H.relativeDensity c P)| ≤ 1

The relative density on any set of triples and the relative density over a polyad differ by at most one, since both lie in [0, 1].

theorem TauCeti.Colored3Graph.relativeDensity_of_support_eq_empty {κ : Type u_1} {V : Type u_2} [DecidableEq κ] [Fintype V] [DecidableEq V] {κ₂ : Type u_3} {S : PairSkeleton3 κ₂ V} (H : Colored3Graph κ V) (c : κ) {P : Polyad3 S} (hP : P.support = ∅) : H.relativeDensity c P = 0

Every relative density over a polyad with empty support is 0.

theorem TauCeti.Colored3Graph.sum_relativeDensity {κ : Type u_1} {V : Type u_2} [DecidableEq κ] [Fintype V] [DecidableEq V] {κ₂ : Type u_3} {S : PairSkeleton3 κ₂ V} [Fintype κ] (H : Colored3Graph κ V) {P : Polyad3 S} (hP : P.support.Nonempty) : ∑ c : κ, H.relativeDensity c P = 1

The relative densities of all colors over a polyad with nonempty support sum to one.

theorem TauCeti.Colored3Graph.relDensityOn_sub_mul_card_eq_sum_inter_support {κ : Type u_1} {V : Type u_2} [DecidableEq κ] [Fintype V] [DecidableEq V] {κ₂ : Type u_3} (S : PairSkeleton3 κ₂ V) [Fintype κ₂] (H : Colored3Graph κ V) (c : κ) (s : Finset { x : Fin 3 → V // Function.Injective x }) (a : ℝ) : (↑(H.relDensityOn c s) - a) * ↑s.card = ∑ P : Polyad3 S, (↑(H.relDensityOn c (s ∩ P.support)) - a) * ↑(s ∩ P.support).card

The count-scaled deviation of a color density on a finite set of injective triples from a constant splits over the polyads of any lower skeleton.