Edit discrepancy of colored three-uniform hypergraphs

The edit discrepancy H.editDiscrepancy3 H' of two colorings of the triples of V is six times the number of unordered triples on which they disagree, divided by |V|³. Equivalently, it is the fraction of all |V|³ ordered triples of vertices whose entries are distinct and form a triple on which the colorings disagree. H.Approximates3 H' ε says that the edit discrepancy is at most ε.

The discrepancy is a pseudometric: it is nonnegative, symmetric, zero on the diagonal, and satisfies the triangle inequality, so approximations compose with their errors added. The vertex count is Nat.card V, so no finiteness hypothesis is needed: on an infinite vertex type the denominator vanishes and every discrepancy is 0.

The finite set H.editedOn H' supp records the edited injective triples on a given support, counting each supported ordering separately. Its cardinality is additive over disjoint supports.

Main definitions

• TauCeti.Colored3Graph.editDiscrepancy3: the normalized number of disagreeing triples.
• TauCeti.Colored3Graph.Approximates3: approximation within a given edit discrepancy.
• TauCeti.Colored3Graph.editedOn: the supported injective triples whose colors differ.

Main results

• TauCeti.Colored3Graph.editDiscrepancy3_triangle: the triangle inequality.
• TauCeti.Colored3Graph.Approximates3.trans: approximations compose, adding their errors.
• TauCeti.Colored3Graph.card_editedOn_biUnion: edit counts add over disjoint supports.

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

The supported injective triples whose underlying unordered triple has different colors in H and H'. Each supported ordering is counted separately.

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

Edited triples are obtained by filtering the support for unequal colors.

@[simp]

theorem TauCeti.Colored3Graph.mem_editedOn {κ : Type u_1} {V : Type u_2} [DecidableEq κ] (H H' : Colored3Graph κ V) (supp : Finset { x : Fin 3 → V // Function.Injective x }) (x : { x : Fin 3 → V // Function.Injective x }) : x ∈ H.editedOn H' supp ↔ x ∈ supp ∧ H.color (Set.powersetCard.ofFinEmb 3 V { toFun := ↑x, inj' := ⋯ }) ≠ H'.color (Set.powersetCard.ofFinEmb 3 V { toFun := ↑x, inj' := ⋯ })

Membership means being supported and having different colors.

theorem TauCeti.Colored3Graph.editedOn_subset {κ : Type u_1} {V : Type u_2} [DecidableEq κ] (H H' : Colored3Graph κ V) (supp : Finset { x : Fin 3 → V // Function.Injective x }) : H.editedOn H' supp ⊆ supp

Every edited triple belongs to the given support.

theorem TauCeti.Colored3Graph.editedOn_mono {κ : Type u_1} {V : Type u_2} [DecidableEq κ] (H H' : Colored3Graph κ V) {A B : Finset { x : Fin 3 → V // Function.Injective x }} (h : A ⊆ B) : H.editedOn H' A ⊆ H.editedOn H' B

Enlarging the support can only enlarge the set of edited triples.

theorem TauCeti.Colored3Graph.editedOn_comm {κ : Type u_1} {V : Type u_2} [DecidableEq κ] (H H' : Colored3Graph κ V) (supp : Finset { x : Fin 3 → V // Function.Injective x }) : H.editedOn H' supp = H'.editedOn H supp

The edited support is independent of the direction of recoloring.

@[simp]

theorem TauCeti.Colored3Graph.editedOn_self {κ : Type u_1} {V : Type u_2} [DecidableEq κ] (H : Colored3Graph κ V) (supp : Finset { x : Fin 3 → V // Function.Injective x }) : H.editedOn H supp = ∅

A coloring has no edits relative to itself.

@[simp]

theorem TauCeti.Colored3Graph.editedOn_empty {κ : Type u_1} {V : Type u_2} [DecidableEq κ] (H H' : Colored3Graph κ V) : H.editedOn H' ∅ = ∅

There are no edited triples on the empty support.

theorem TauCeti.Colored3Graph.card_editedOn_biUnion {κ : Type u_1} {V : Type u_2} [DecidableEq κ] {ι : Type u_3} [DecidableEq V] (H H' : Colored3Graph κ V) (s : Finset ι) (supp : ι → Finset { x : Fin 3 → V // Function.Injective x }) (h : (↑s).PairwiseDisjoint supp) : (H.editedOn H' (s.biUnion supp)).card = ∑ i ∈ s, (H.editedOn H' (supp i)).card

The edit count is additive over a finite family of pairwise disjoint supports.

noncomputable def TauCeti.Colored3Graph.editDiscrepancy3 {κ : Type u_1} {V : Type u_2} (H H' : Colored3Graph κ V) : ℚ

Six times the number of unordered triples on which H and H' disagree, normalized by |V|³.

theorem TauCeti.Colored3Graph.editDiscrepancy3_def {κ : Type u_1} {V : Type u_2} (H H' : Colored3Graph κ V) : H.editDiscrepancy3 H' = 6 * ↑{s : ↑(Set.powersetCard V 3) | H.color s ≠ H'.color s}.ncard / ↑(Nat.card V) ^ 3

The edit discrepancy counts disagreeing triples, normalized by |V|³.

theorem TauCeti.Colored3Graph.editDiscrepancy3_mul_card_pow {κ : Type u_1} {V : Type u_2} [Finite V] (H H' : Colored3Graph κ V) : H.editDiscrepancy3 H' * ↑(Nat.card V) ^ 3 = 6 * ↑{s : ↑(Set.powersetCard V 3) | H.color s ≠ H'.color s}.ncard

Multiplying edit discrepancy by the host-size cube recovers six times the edit count. The finite-host hypothesis is necessary because Nat.card vanishes on infinite types.

theorem TauCeti.Colored3Graph.editDiscrepancy3_nonneg {κ : Type u_1} {V : Type u_2} (H H' : Colored3Graph κ V) : 0 ≤ H.editDiscrepancy3 H'

The edit discrepancy is nonnegative.

theorem TauCeti.Colored3Graph.editDiscrepancy3_comm {κ : Type u_1} {V : Type u_2} (H H' : Colored3Graph κ V) : H.editDiscrepancy3 H' = H'.editDiscrepancy3 H

The edit discrepancy is symmetric.

@[simp]

theorem TauCeti.Colored3Graph.editDiscrepancy3_self {κ : Type u_1} {V : Type u_2} (H : Colored3Graph κ V) : H.editDiscrepancy3 H = 0

A coloring has edit discrepancy 0 from itself.

theorem TauCeti.Colored3Graph.editDiscrepancy3_triangle {κ : Type u_1} {V : Type u_2} (H₁ H₂ H₃ : Colored3Graph κ V) : H₁.editDiscrepancy3 H₃ ≤ H₁.editDiscrepancy3 H₂ + H₂.editDiscrepancy3 H₃

The triangle inequality for the edit discrepancy.

def TauCeti.Colored3Graph.Approximates3 {κ : Type u_1} {V : Type u_2} (H H' : Colored3Graph κ V) (ε : ℝ) : Prop

H approximates H' within ε when their edit discrepancy is at most ε.

theorem TauCeti.Colored3Graph.approximates3_iff {κ : Type u_1} {V : Type u_2} (H H' : Colored3Graph κ V) (ε : ℝ) : H.Approximates3 H' ε ↔ ↑(H.editDiscrepancy3 H') ≤ ε

Approximation within ε means that the edit discrepancy is at most ε.

theorem TauCeti.Colored3Graph.approximates3_self {κ : Type u_1} {V : Type u_2} (H : Colored3Graph κ V) {ε : ℝ} (hε : 0 ≤ ε) : H.Approximates3 H ε

A coloring approximates itself within any nonnegative error.

theorem TauCeti.Colored3Graph.Approximates3.symm {κ : Type u_1} {V : Type u_2} {H₁ H₂ : Colored3Graph κ V} {ε : ℝ} (h : H₁.Approximates3 H₂ ε) : H₂.Approximates3 H₁ ε

Approximation is symmetric.

theorem TauCeti.Colored3Graph.Approximates3.mono {κ : Type u_1} {V : Type u_2} {H₁ H₂ : Colored3Graph κ V} {ε δ : ℝ} (h : H₁.Approximates3 H₂ ε) (hεδ : ε ≤ δ) : H₁.Approximates3 H₂ δ

Approximation within ε implies approximation within any larger error.

theorem TauCeti.Colored3Graph.Approximates3.trans {κ : Type u_1} {V : Type u_2} {H₁ H₂ H₃ : Colored3Graph κ V} {ε δ : ℝ} (h₁₂ : H₁.Approximates3 H₂ ε) (h₂₃ : H₂.Approximates3 H₃ δ) : H₁.Approximates3 H₃ (ε + δ)

Approximations compose, with their errors added.