Positive rescaling of the factors of a positive Kronecker product

A Kronecker product A ⊗ B determines its factors only up to a reciprocal pair of scalars. This file shows that over ℂ the scalar ambiguity can be used in one direction: if A ⊗ B is positive semidefinite and both factors are nonzero, then there is a nonzero scalar c with c • A and c⁻¹ • B positive semidefinite.

The proof evaluates the quadratic form of A ⊗ B on product vectors, which factors it into the two quadratic forms, and uses the polarization identity: a complex matrix is determined by its quadratic form.

Main results

• Matrix.eq_zero_of_forall_star_dotProduct_mulVec_eq_zero: a complex matrix whose quadratic form vanishes identically is zero.
• Matrix.posSemidef_of_forall_star_dotProduct_mulVec_nonneg: a complex matrix with nonnegative quadratic form is positive semidefinite; over ℂ the Hermitian property is automatic.
• Matrix.star_dotProduct_kronecker_mulVec_prod: on a product vector the quadratic form of a Kronecker product factors.
• Matrix.finKronecker_posSemidef: a finite Kronecker product of positive semidefinite matrices is positive semidefinite.
• Matrix.exists_smul_posSemidef_of_kronecker_posSemidef: the positive rescaling of the two factors of a nonzero positive semidefinite Kronecker product.
• Matrix.smul_kronecker_smul_inv_eq: a reciprocal pair of scalars leaves a Kronecker product unchanged; this is what makes the rescaling of the previous result represent the same product.
• Matrix.exists_pos_real_smul_eq_of_smul_posSemidef: the phase of a positive rescaling of a nonzero matrix is unique.
• Matrix.exists_pi_smul_posSemidef_of_finKronecker_posSemidef: every factor of one finite nonzero positive Kronecker product can be rescaled positively, with product-one rescaling coefficients.

theorem Matrix.eq_zero_of_forall_star_dotProduct_mulVec_eq_zero {n : Type u_2} [Fintype n] {M : Matrix n n ℂ} (h : ∀ (x : n → ℂ), star x ⬝ᵥ M.mulVec x = 0) : M = 0

Polarization. A complex matrix whose quadratic form x ↦ star x ⬝ᵥ M *ᵥ x vanishes identically is the zero matrix.

theorem Matrix.exists_star_dotProduct_mulVec_ne_zero {n : Type u_2} [Fintype n] {M : Matrix n n ℂ} (hM : M ≠ 0) : ∃ (x : n → ℂ), star x ⬝ᵥ M.mulVec x ≠ 0

A nonzero complex matrix has a nonzero quadratic-form value.

theorem Matrix.posSemidef_of_forall_star_dotProduct_mulVec_nonneg {n : Type u_2} [Fintype n] {M : Matrix n n ℂ} (h : ∀ (x : n → ℂ), 0 ≤ star x ⬝ᵥ M.mulVec x) : M.PosSemidef

A complex matrix with nonnegative quadratic form is positive semidefinite. Over ℂ a real-valued quadratic form already forces the Hermitian property, so no symmetry hypothesis is needed.

theorem Matrix.star_dotProduct_kronecker_mulVec_prod {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : Matrix m m ℂ) (B : Matrix n n ℂ) (x : m → ℂ) (y : n → ℂ) : ((star fun (p : m × n) => x p.1 * y p.2) ⬝ᵥ (kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B).mulVec fun (p : m × n) => x p.1 * y p.2) = star x ⬝ᵥ A.mulVec x * star y ⬝ᵥ B.mulVec y

On a product vector, the quadratic form of a Kronecker product is the product of the quadratic forms of the two factors.

theorem Matrix.smul_kronecker_smul_inv_eq {l : Type u_3} {p : Type u_4} {q : Type u_5} {r : Type u_6} (A : Matrix l p ℂ) (B : Matrix q r ℂ) {c : ℂ} (hc : c ≠ 0) : kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (c • A) (c⁻¹ • B) = kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B

A reciprocal pair of scalars leaves a Kronecker product unchanged: for any nonzero c, (c • A) ⊗ (c⁻¹ • B) = A ⊗ B. This holds for arbitrary matrix shapes and needs no positivity hypothesis; it is the algebraic fact that makes the rescaling in Matrix.exists_smul_posSemidef_of_kronecker_posSemidef represent the same product as the original factors.

theorem Matrix.exists_smul_posSemidef_of_kronecker_posSemidef {m : Type u_3} {n : Type u_4} [Finite m] [Finite n] {A : Matrix m m ℂ} {B : Matrix n n ℂ} (hAB : (kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B).PosSemidef) (hA : A ≠ 0) (hB : B ≠ 0) : ∃ (c : ℂ), c ≠ 0 ∧ (c • A).PosSemidef ∧ (c⁻¹ • B).PosSemidef ∧ kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (c • A) (c⁻¹ • B) = kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B

Positive rescaling of Kronecker factors. If a Kronecker product of two nonzero complex matrices is positive semidefinite, then there is a nonzero scalar c such that c • A and c⁻¹ • B are both positive semidefinite. By Matrix.smul_kronecker_smul_inv_eq, (c • A) ⊗ (c⁻¹ • B) = A ⊗ B, so the rescaled factors represent the same product.

Uniqueness of the rescaling phase, and an N-ary generalization

The rescaling scalar c of exists_smul_posSemidef_of_kronecker_posSemidef is not unique: any positive real multiple of a valid c is again valid. It is unique in every other respect — two valid scalars for the same nonzero matrix always agree up to a positive real ratio. Combined with an inductive extension of the two-factor rescaling to a Kronecker product of finitely many factors, this gives a compatible choice of phases around one fixed cycle of nonzero matrices whose iterated Kronecker product is positive semidefinite. It does not assert compatibility between different cycles in a graph.

theorem Matrix.PosSemidef.eq_zero_of_neg_posSemidef {n : Type u_3} [Finite n] {X : Matrix n n ℂ} (hX : X.PosSemidef) (hX' : (-X).PosSemidef) : X = 0

A positive semidefinite matrix that is also negative semidefinite is zero.

theorem Matrix.exists_pos_real_smul_eq_of_smul_posSemidef {n : Type u_3} [Finite n] {M : Matrix n n ℂ} (hM : M ≠ 0) {c₁ c₂ : ℂ} (h₁ : (c₁ • M).PosSemidef) (h₂ : (c₂ • M).PosSemidef) (hc₁ : c₁ ≠ 0) (hc₂ : c₂ ≠ 0) : ∃ (t : ℝ), 0 < t ∧ c₁ = ↑t * c₂

Uniqueness of the rescaling phase. If two nonzero scalar multiples of the same nonzero matrix are both positive semidefinite, the two scalars agree up to a positive real factor: rescaling to positive semidefiniteness pins down a phase, only the positive magnitude remains free.

An N-ary Kronecker product

def Matrix.finKronecker {N : ℕ} {α : Fin N → Type u_3} [(n : Fin N) → Fintype (α n)] (A : (n : Fin N) → Matrix (α n) (α n) ℂ) : Matrix ((n : Fin N) → α n) ((n : Fin N) → α n) ℂ

The iterated Kronecker product of a family of square matrices indexed by Fin N, each with its own (possibly varying) index type. Its (x, y) entry is the product of the n-th factor's (x n, y n) entry over every position n.

Equations

• Matrix.finKronecker A = Matrix.of fun (x y : (n : Fin N) → α n) => ∏ n : Fin N, A n (x n) (y n)

@[simp]

theorem Matrix.finKronecker_apply {N : ℕ} {α : Fin N → Type u_3} [(n : Fin N) → Fintype (α n)] (A : (n : Fin N) → Matrix (α n) (α n) ℂ) (x y : (n : Fin N) → α n) : finKronecker A x y = ∏ n : Fin N, A n (x n) (y n)

theorem Matrix.finKronecker_posSemidef {N : ℕ} {I : Fin N → Type u_3} [(i : Fin N) → Fintype (I i)] (M : (i : Fin N) → Matrix (I i) (I i) ℂ) : (∀ (i : Fin N), (M i).PosSemidef) → (finKronecker M).PosSemidef

A finite Kronecker product of positive semidefinite matrices is positive semidefinite.

theorem Matrix.finKronecker_ne_zero {N : ℕ} {α : Fin N → Type u_3} [(n : Fin N) → Fintype (α n)] {A : (n : Fin N) → Matrix (α n) (α n) ℂ} (hA : ∀ (n : Fin N), A n ≠ 0) : finKronecker A ≠ 0

A finite Kronecker product of nonzero matrices is nonzero: the entry at a choice of nonzero-witnessing row/column pair for each factor is itself nonzero.

theorem Matrix.finKronecker_update_smul {N : ℕ} {α : Fin N → Type u_3} [(n : Fin N) → Fintype (α n)] (A : (n : Fin N) → Matrix (α n) (α n) ℂ) (i : Fin N) (c : ℂ) : finKronecker (Function.update A i (c • A i)) = c • finKronecker A

Rescaling one factor of a finite Kronecker product by a scalar rescales the whole product by that scalar.

theorem Matrix.exists_pi_smul_posSemidef_of_finKronecker_posSemidef {N : ℕ} : 1 ≤ N → ∀ {α : Fin N → Type u_3} [inst : (n : Fin N) → Fintype (α n)] (A : (n : Fin N) → Matrix (α n) (α n) ℂ), (finKronecker A).PosSemidef → (∀ (n : Fin N), A n ≠ 0) → ∃ (c : Fin N → ℂ), (∀ (n : Fin N), c n ≠ 0) ∧ ∏ n : Fin N, c n = 1 ∧ ∀ (n : Fin N), (c n • A n).PosSemidef

Positive rescaling of a finite Kronecker product. If a Kronecker product of finitely many nonzero factors, indexed by Fin N, is positive semidefinite, then there is a scalar for each factor, all nonzero, whose product is 1, such that rescaling every factor by its scalar makes it positive semidefinite. This is the N-ary generalization of exists_smul_posSemidef_of_kronecker_posSemidef, obtained by peeling off one factor at a time.