Real block reduction of complex Gram matrices

Adapted for Lean Pool from the Apache-2.0 upstream formalization, with module-system, Mathlib API, and compilation changes.

theorem OlevskiiGram.realBlock_quadraticForm {n : Type u_1} [Fintype n] (G : Matrix n n ℂ) (x : n ⊕ n → ℝ) : realQuadraticForm (realBlockMatrix (complexReMatrix G) (complexImMatrix G)) x = complexQuadraticFormRe G fun (i : n) => ↑(x (Sum.inl i)) + Complex.I * ↑(x (Sum.inr i))

theorem OlevskiiGram.realBlock_one_sub_quadraticForm {n : Type u_1} [Fintype n] [DecidableEq n] (G : Matrix n n ℂ) (x : n ⊕ n → ℝ) : realQuadraticForm (1 - realBlockMatrix (complexReMatrix G) (complexImMatrix G)) x = complexQuadraticFormRe (1 - G) fun (i : n) => ↑(x (Sum.inl i)) + Complex.I * ↑(x (Sum.inr i))

theorem OlevskiiGram.complexPSD_of_posSemidef {n : Type u_1} [Fintype n] (A : Matrix n n ℂ) : A.PosSemidef → ComplexPSD A

Bridge from Mathlib's complex matrix PSD predicate to the quadratic-form predicate.

theorem OlevskiiGram.complexQuadraticFormRe_eq_operator_inner {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) (x : Fin N → ℂ) : complexQuadraticFormRe A x = (inner ℂ (WithLp.toLp 2 x) ((matrixL2Operator A) (WithLp.toLp 2 x))).re

The complex quadratic form is the real part of the Euclidean operator form.

theorem OlevskiiGram.matrixL2Operator_one_sub_apply {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) (x : Fin N → ℂ) : (matrixL2Operator (1 - A)) (WithLp.toLp 2 x) = WithLp.toLp 2 x - (matrixL2Operator A) (WithLp.toLp 2 x)

theorem OlevskiiGram.complexPSD_one_sub_of_operatorNorm {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) : matrixL2OperatorNormLE A 1 → ComplexPSD (1 - A)

theorem OlevskiiGram.gramMatrix_psd_le_one {N : ℕ} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (z : Fin N → H) : matrixL2OperatorNormLE (gramMatrix z) 1 → ComplexHermitian (gramMatrix z) ∧ ComplexLoewnerBetweenZeroAndOne (gramMatrix z)

The Gram matrix with operator norm at most one satisfies the Hermitian and Loewner-order hypotheses needed for the decomposition.

theorem OlevskiiGram.realBlock_psd_le_one {n : Type u_1} [Fintype n] [DecidableEq n] (G : Matrix n n ℂ) : ComplexHermitian G → ComplexLoewnerBetweenZeroAndOne G → have Gtilde := realBlockMatrix (complexReMatrix G) (complexImMatrix G); RealSymmetric Gtilde ∧ RealLoewnerBetweenZeroAndOne Gtilde

The real block matrix of a Hermitian complex matrix 0 ≤ G ≤ I also satisfies 0 ≤ G_real ≤ I.

theorem OlevskiiGram.finiteComplexDecomposition {n : Type u_1} [Fintype n] [DecidableEq n] (G : Matrix n n ℂ) : HasRealConvexDecomposition (n ⊕ n) → ComplexHermitian G → ComplexLoewnerBetweenZeroAndOne G → ∃ (m : ℕ) (_ : 0 < m) (p : Fin m → ℝ) (ζ : Fin m → n → ℂ), (∀ (r : Fin m), 0 ≤ p r) ∧ ∑ r : Fin m, p r = 1 ∧ (∀ (r : Fin m) (j : n), ‖ζ r j‖ ≤ 1) ∧ ∀ (j k : n), G j k = ∑ r : Fin m, ↑(p r) * ζ r j * star (ζ r k)

Finite complex rank-one decomposition of a Hermitian matrix 0 ≤ G ≤ I by vectors with coordinatewise norm at most one.