dotProduct_mulVec_zero_iff — Mathlib

English

For A PSD and x, the linear-map form x^* A x = 0 is equivalent to A x = 0.

Русский

Для PSD A и вектора x равенство x^* A x = 0 эквивалентно A x = 0.

LaTeX

$$$\text{PosSemidef}(A)\Rightarrow\forall x,\ (x^* A x = 0) \iff (A x = 0).$$$

Lean4

/-- For `A` positive semidefinite, we have `x⋆ A x = 0` iff `A x = 0`. -/
theorem dotProduct_mulVec_zero_iff {A : Matrix n n 𝕜} (hA : PosSemidef A) (x : n → 𝕜) :
    star x ⬝ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0 := by
  classical
  refine ⟨fun h ↦ ?_, fun h ↦ h ▸ dotProduct_zero _⟩
  obtain ⟨B, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hA.nonneg
  simp_rw [← Matrix.mulVec_mulVec, dotProduct_mulVec _ _ (B *ᵥ x), star_eq_conjTranspose, vecMul_conjTranspose,
    star_star, dotProduct_star_self_eq_zero] at h ⊢
  rw [h, mulVec_zero]

Похожие утверждения