AcceptedProposition · Statement with omitted proof

Congruence preserves positive semidefinite order

Multiplying on both sides by a matrix and its adjoint preserves positive semidefiniteness and order.

Halko, Martinsson & Tropp ↗
Source label: prop:conjugation

Download Lean file ↓

Formal statement. The assumptions and conclusion are explicit; the theorem proof is omitted (sorry).

01 / MATHEMATICAL STATEMENT

Meaning & conditions

Mathematical summary

Multiplying on both sides by a matrix and its adjoint preserves positive semidefiniteness and order.

M\succeq0\Rightarrow A^*MA\succeq0,\qquad M\preceq N\Rightarrow A^*MA\preceq A^*NA

Assumptions & context

The matrices have compatible dimensions over ℝ or ℂ; the order is defined by positive semidefinite differences.

Source

Halko, Martinsson & Tropp. Finding structure with randomness.

Source label: prop:conjugation

02 / LEAN REPRESENTATION

Formal statement

Statement with omitted proof. Expand the complete file below to read imports, local definitions and surrounding context.

theorem prop_conjugation {𝕜 : Type*} [RCLike 𝕜] {n k : ℕ} :
    (∀ M : Matrix (Fin n) (Fin n) 𝕜, M.PosSemidef →
      ∀ A : Matrix (Fin n) (Fin k) 𝕜, (Aᴴ * M * A).PosSemidef) ∧
    (∀ (M N : Matrix (Fin n) (Fin n) 𝕜) (A : Matrix (Fin n) (Fin k) 𝕜),
      PsdLe M N → PsdLe (Aᴴ * M * A) (Aᴴ * N * A)) := by
  sorry

Complete Lean file and local definitions

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

open MeasureTheory
open scoped Matrix
open scoped Matrix.Norms.L2Operator
open scoped BigOperators
open scoped ENNReal
open scoped ComplexOrder

namespace RNLAPhaseB.HMT2011.PropConjugation

/-- The semidefinite (Loewner) order `M ⪯ N`: the difference `N - M` is positive semidefinite. -/
def PsdLe {𝕜 : Type*} [RCLike 𝕜] {n : ℕ}
    (M N : Matrix (Fin n) (Fin n) 𝕜) : Prop :=
  (N - M).PosSemidef

/-- HMT 2011, Proposition (conjugation rule).
If `M ⪰ 0`, then for every `A` the matrix `A^* M A ⪰ 0`.
In particular, `M ⪯ N` implies `A^* M A ⪯ A^* N A`.
The field is real or complex (`RCLike 𝕜`), and `A^*` is the conjugate transpose `Aᴴ`.
`A` has as many rows as `M` has columns, so that `A^* M A` is defined; its column count `k` is arbitrary. -/
theorem prop_conjugation {𝕜 : Type*} [RCLike 𝕜] {n k : ℕ} :
    (∀ M : Matrix (Fin n) (Fin n) 𝕜, M.PosSemidef →
      ∀ A : Matrix (Fin n) (Fin k) 𝕜, (Aᴴ * M * A).PosSemidef) ∧
    (∀ (M N : Matrix (Fin n) (Fin n) 𝕜) (A : Matrix (Fin n) (Fin k) 𝕜),
      PsdLe M N → PsdLe (Aᴴ * M * A) (Aᴴ * N * A)) := by
  sorry

end RNLAPhaseB.HMT2011.PropConjugation

How to read the formalization

The formal statement includes both preservation of positivity and monotonicity under congruence.

← Back to all statements