The Cai–Govorov Vandermonde argument

This file formalizes the elementary "Vandermonde argument" of Cai and Govorov, On a Theorem of Lovász that hom(·, H) Determines the Isomorphism Type of H (ITCS 2020 / arXiv:1909.03693), §4. These are purely algebraic, graph-free statements that drive the orbit-separation argument for weighted graphs.

Main results

• vandermonde_class_sums_zero (Cai–Govorov Lemma 4.1): if ∑ i, a i * x i ^ j = 0 for all j < |ι|, then the coefficient sum over each level set of x vanishes (equivalently ∑ i, a i * f (x i) = 0 for every f, see vandermonde_apply_eq_zero). Crucially the values x i need not be distinct.

• multivariate_vandermonde_class_sums_zero (Cai–Govorov Corollary 4.2): the multivariate version. Indices are classified by their s-tuple b i : Fin s → ℝ; if ∑ i, a i * ∏ j, b i j ^ ℓ j = 0 for all exponent tuples ℓ bounded by |ι|, then the coefficient sum over each tuple-class vanishes.

The headline lemmas are stated in "class-sum" (level-set) form. The auxiliary *_apply_eq_zero lemmas give the equivalent "∀ f" form which is the convenient engine for the multivariate induction.

theorem Graphon.CaiGovorov.vandermonde_coeffs_zero {ι : Type u_1} [Fintype ι] (s : ι → ℝ) (hs : Function.Injective s) (a : ι → ℝ) (h : ∀ n < Fintype.card ι, ∑ i : ι, a i * s i ^ n = 0) : a = 0

A Vandermonde nonsingularity corollary over an arbitrary finite index type: if the values s i are distinct and ∑ i, a i * s i ^ n = 0 for all n < |ι|, then all coefficients vanish.

theorem Graphon.CaiGovorov.sum_apply_eq_zero_of_fibers {ι : Type u_1} [Fintype ι] {α : Type u_2} [DecidableEq α] (v : ι → α) (a : ι → ℝ) (h : ∀ (c : α), ∑ i : ι with v i = c, a i = 0) (f : α → ℝ) : ∑ i : ι, a i * f (v i) = 0

Bridge from "level-set coefficient sums vanish" to the ∀ f form.

theorem Graphon.CaiGovorov.finset_vandermonde_zero {S : Finset ℝ} (A : ℝ → ℝ) (h : ∀ n < S.card, ∑ d ∈ S, A d * d ^ n = 0) (d : ℝ) : d ∈ S → A d = 0

Vandermonde nonsingularity over a finite set of distinct real nodes: if ∑ d ∈ S, A d * d ^ n = 0 for all n < |S|, then A vanishes on S.

theorem Graphon.CaiGovorov.vandermonde_class_sums_zero {ι : Type u_1} [Fintype ι] (x a : ι → ℝ) (h : ∀ j < Fintype.card ι, ∑ i : ι, a i * x i ^ j = 0) (c : ℝ) : ∑ i : ι with x i = c, a i = 0

Cai–Govorov Lemma 4.1 (Vandermonde argument), level-set form. If ∑ i, a i * x i ^ j = 0 for all j < |ι|, then for every value c the coefficient sum over the level set {i | x i = c} vanishes. The values x i need not be distinct.

theorem Graphon.CaiGovorov.vandermonde_apply_eq_zero {ι : Type u_1} [Fintype ι] (x a : ι → ℝ) (h : ∀ j < Fintype.card ι, ∑ i : ι, a i * x i ^ j = 0) (f : ℝ → ℝ) : ∑ i : ι, a i * f (x i) = 0

Cai–Govorov Lemma 4.1, ∀ f form: if ∑ i, a i * x i ^ j = 0 for all j < |ι|, then ∑ i, a i * f (x i) = 0 for every function f.

theorem Graphon.CaiGovorov.vandermonde_class_sums_zero_of_bound {ι : Type u_1} [Fintype ι] (x a : ι → ℝ) (N : ℕ) (hN : (Finset.image x Finset.univ).card ≤ N) (h : ∀ j < N, ∑ i : ι, a i * x i ^ j = 0) (c : ℝ) : ∑ i : ι with x i = c, a i = 0

Univariate Lemma 4.1 with an explicit bound N on the number of distinct values of x (in place of |ι|).

theorem Graphon.CaiGovorov.vandermonde_apply_eq_zero_of_bound {ι : Type u_1} [Fintype ι] (x a : ι → ℝ) (N : ℕ) (hN : (Finset.image x Finset.univ).card ≤ N) (h : ∀ j < N, ∑ i : ι, a i * x i ^ j = 0) (f : ℝ → ℝ) : ∑ i : ι, a i * f (x i) = 0

Univariate ∀f form with an explicit distinct-value bound.

theorem Graphon.CaiGovorov.multivariate_vandermonde_apply_eq_zero_of_bound (s : ℕ) {ι : Type u_1} [Fintype ι] (b : ι → Fin s → ℝ) (a : ι → ℝ) (M : ℕ) : (∀ (j : Fin s), (Finset.image (fun (i : ι) => b i j) Finset.univ).card ≤ M) → (∀ (ℓ : Fin s → ℕ), (∀ (j : Fin s), ℓ j < M) → ∑ i : ι, a i * ∏ j : Fin s, b i j ^ ℓ j = 0) → ∀ (f : (Fin s → ℝ) → ℝ), ∑ i : ι, a i * f (b i) = 0

Multivariate ∀f form with a UNIFORM bound M such that every coordinate j of the profile b takes at most M distinct values.

theorem Graphon.CaiGovorov.multivariate_vandermonde_class_sums_zero_of_bound {s : ℕ} {ι : Type u_1} [Fintype ι] (b : ι → Fin s → ℝ) (a : ι → ℝ) (M : ℕ) (hM : ∀ (j : Fin s), (Finset.image (fun (i : ι) => b i j) Finset.univ).card ≤ M) (h : ∀ (ℓ : Fin s → ℕ), (∀ (j : Fin s), ℓ j < M) → ∑ i : ι, a i * ∏ j : Fin s, b i j ^ ℓ j = 0) (β : Fin s → ℝ) : ∑ i : ι with b i = β, a i = 0

Multivariate level-set form with a uniform distinct-value bound M.

theorem Graphon.CaiGovorov.multivariate_vandermonde_apply_eq_zero (s : ℕ) {ι : Type u_1} [Fintype ι] (b : ι → Fin s → ℝ) (a : ι → ℝ) : (∀ (ℓ : Fin s → ℕ), (∀ (j : Fin s), ℓ j < Fintype.card ι) → ∑ i : ι, a i * ∏ j : Fin s, b i j ^ ℓ j = 0) → ∀ (f : (Fin s → ℝ) → ℝ), ∑ i : ι, a i * f (b i) = 0

Cai–Govorov Corollary 4.2, ∀ f form: the multivariate Vandermonde argument. If ∑ i, a i * ∏ j, b i j ^ ℓ j = 0 for every exponent tuple ℓ bounded by |ι|, then ∑ i, a i * f (b i) = 0 for every f. Corollary of the bounded engine at M := |ι| (a coordinate image never exceeds |ι|).

theorem Graphon.CaiGovorov.multivariate_vandermonde_class_sums_zero {s : ℕ} {ι : Type u_1} [Fintype ι] (b : ι → Fin s → ℝ) (a : ι → ℝ) (h : ∀ (ℓ : Fin s → ℕ), (∀ (j : Fin s), ℓ j < Fintype.card ι) → ∑ i : ι, a i * ∏ j : Fin s, b i j ^ ℓ j = 0) (β : Fin s → ℝ) : ∑ i : ι with b i = β, a i = 0

Cai–Govorov Corollary 4.2, level-set form. Indices are classified by their tuple b i; under the bounded power-sum hypothesis, the coefficient sum over each tuple-class vanishes. Corollary of the bounded engine at M := |ι|.