Balanced weighted colourings

TheoremBalanced coloring of a weighted symmetric matrix#✓fully proved

A finite symmetric natural-valued matrix with zero diagonal and bounded row sums has a coloring with balanced fibers and bounded weight in every ordered color block.

theorem exists_balanced_coloring (c : Matrix ι ι ℕ) (hd : ∀ a, c a a = 0)
    (hs : c.IsSymm) (P : ℕ) (hP : ∀ a, ∑ b, c a b ≤ P) (hK : 0 < K)
    (hg : 4 * K ^ 6 + K ^ 2 < g) :
    ∃ χ : ι → κ, (∀ γ, K * #{a | χ a = γ} < 2 * g) ∧
      ∀ γ γ', K ^ 3 * (∑ a with χ a = γ, ∑ b with χ b = γ', c a b) ≤
        K * (∑ a, ∑ b, c a b) + g * P

Uses 2 · Used by 1

Proof usesMoment count bound over the whole type · Division-free count of functions with prescribed values

Used byBalanced coloring with bounded off-diagonal block weight

TheoremBalanced coloring with bounded off-diagonal block weight#✓fully proved

A finite symmetric natural-valued matrix with bounded off-diagonal row sums has a balanced coloring whose blocks between distinct colors have bounded off-diagonal weight. Diagonal entries are unrestricted and ignored.

theorem exists_balanced_coloring_offDiagonal (c : Matrix ι ι ℕ) (hK : 2 ≤ K)
    (hg : 3 * K ^ 8 ≤ g) (hs : c.IsSymm) (P : ℕ)
    (hP : ∀ a, ∑ b with b ≠ a, c a b ≤ P) :
    ∃ χ : ι → κ, (∀ γ, K * #{a | χ a = γ} < 2 * g) ∧
      ∀ γ γ', γ ≠ γ' →
        K ^ 3 * (∑ a with χ a = γ, ∑ b with χ b = γ', c a b) ≤
          K * (∑ a, ∑ b with b ≠ a, c a b) + g * P

Uses 1 · Used by 1

Proof usesBalanced coloring of a weighted symmetric matrix

Used byBalanced off-diagonal coloring for matrices indexed by \(\{0,\dots,n-1\}\)

TheoremBalanced off-diagonal coloring for matrices indexed by \(\{0,\dots,n-1\}\)#✓fully proved

The Fin-indexed form of Matrix.exists_balanced_coloring_offDiagonal.

theorem exists_balanced_coloring_fin {K g : ℕ} (hK : 2 ≤ K) (hg : 3 * K ^ 8 ≤ g)
    (c : Matrix (Fin g) (Fin g) ℕ) (hs : c.IsSymm) (P : ℕ)
    (hP : ∀ a, ∑ b with b ≠ a, c a b ≤ P) :
    ∃ χ : Fin g → Fin K, (∀ γ, K * #{a | χ a = γ} < 2 * g) ∧
      ∀ γ γ', γ ≠ γ' →
        K ^ 3 * (∑ a with χ a = γ, ∑ b with χ b = γ', c a b) ≤
          K * (∑ a, ∑ b with b ≠ a, c a b) + g * P

Uses 1

Proof usesBalanced coloring with bounded off-diagonal block weight

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.