[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosDef M
⊢ PosSemidef M
[PROOFSTEP]
refine' ⟨hM.1, _⟩
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosDef M
⊢ ∀ (x : n → R), 0 ≤ star x ⬝ᵥ mulVec M x
[PROOFSTEP]
intro x
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosDef M
x : n → R
⊢ 0 ≤ star x ⬝ᵥ mulVec M x
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosDef M
x : n → R
hx : x = 0
⊢ 0 ≤ star x ⬝ᵥ mulVec M x
[PROOFSTEP]
simp only [hx, zero_dotProduct, star_zero, IsROrC.zero_re']
[GOAL]
case pos
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosDef M
x : n → R
hx : x = 0
⊢ 0 ≤ 0
[PROOFSTEP]
exact le_rfl
[GOAL]
case neg
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosDef M
x : n → R
hx : ¬x = 0
⊢ 0 ≤ star x ⬝ᵥ mulVec M x
[PROOFSTEP]
exact le_of_lt (hM.2 x hx)
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
⊢ PosSemidef (Matrix.submatrix M ↑e ↑e)
[PROOFSTEP]
refine' ⟨hM.1.submatrix e, fun x => _⟩
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
⊢ 0 ≤ star x ⬝ᵥ mulVec (Matrix.submatrix M ↑e ↑e) x
[PROOFSTEP]
have : (M.submatrix (⇑e) e).mulVec x = (M.mulVec fun i : n => x (e.symm i)) ∘ e :=
  by
  ext i
  dsimp only [(· ∘ ·), mulVec, dotProduct]
  rw [Finset.sum_bij' (fun i _ => e i) _ _ fun i _ => e.symm i] <;>
    simp only [eq_self_iff_true, imp_true_iff, Equiv.symm_apply_apply, Finset.mem_univ, submatrix_apply,
      Equiv.apply_symm_apply]
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
⊢ mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
[PROOFSTEP]
ext i
[GOAL]
case h
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
i : m
⊢ mulVec (Matrix.submatrix M ↑e ↑e) x i = ((mulVec M fun i => x (↑e.symm i)) ∘ ↑e) i
[PROOFSTEP]
dsimp only [(· ∘ ·), mulVec, dotProduct]
[GOAL]
case h
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
i : m
⊢ (Finset.sum Finset.univ fun i_1 => Matrix.submatrix M (↑e) (↑e) i i_1 * x i_1) =
    Finset.sum Finset.univ fun i_1 => M (↑e i) i_1 * x (↑e.symm i_1)
[PROOFSTEP]
rw [Finset.sum_bij' (fun i _ => e i) _ _ fun i _ => e.symm i]
[GOAL]
case h.hj
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
i : m
⊢ ∀ (a : n), a ∈ Finset.univ → ↑e.symm a ∈ Finset.univ
[PROOFSTEP]
simp only [eq_self_iff_true, imp_true_iff, Equiv.symm_apply_apply, Finset.mem_univ, submatrix_apply,
  Equiv.apply_symm_apply]
[GOAL]
case h.left_inv
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
i : m
⊢ ∀ (a : m), a ∈ Finset.univ → ↑e.symm (↑e a) = a
[PROOFSTEP]
simp only [eq_self_iff_true, imp_true_iff, Equiv.symm_apply_apply, Finset.mem_univ, submatrix_apply,
  Equiv.apply_symm_apply]
[GOAL]
case h.right_inv
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
i : m
⊢ ∀ (a : n), a ∈ Finset.univ → ↑e (↑e.symm a) = a
[PROOFSTEP]
simp only [eq_self_iff_true, imp_true_iff, Equiv.symm_apply_apply, Finset.mem_univ, submatrix_apply,
  Equiv.apply_symm_apply]
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
i : m
⊢ ∀ (a : m) (ha : a ∈ Finset.univ), (fun i x => ↑e i) a ha ∈ Finset.univ
[PROOFSTEP]
simp only [eq_self_iff_true, imp_true_iff, Equiv.symm_apply_apply, Finset.mem_univ, submatrix_apply,
  Equiv.apply_symm_apply]
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
i : m
⊢ ∀ (a : m) (ha : a ∈ Finset.univ),
    Matrix.submatrix M (↑e) (↑e) i a * x a = M (↑e i) ((fun i x => ↑e i) a ha) * x (↑e.symm ((fun i x => ↑e i) a ha))
[PROOFSTEP]
simp only [eq_self_iff_true, imp_true_iff, Equiv.symm_apply_apply, Finset.mem_univ, submatrix_apply,
  Equiv.apply_symm_apply]
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
this : mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
⊢ 0 ≤ star x ⬝ᵥ mulVec (Matrix.submatrix M ↑e ↑e) x
[PROOFSTEP]
rw [this]
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
this : mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
⊢ 0 ≤ star x ⬝ᵥ (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
[PROOFSTEP]
convert hM.2 fun i => x (e.symm i) using 3
[GOAL]
case h.e'_4
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
this : mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
⊢ star x ⬝ᵥ (mulVec M fun i => x (↑e.symm i)) ∘ ↑e = (star fun i => x (↑e.symm i)) ⬝ᵥ mulVec M fun i => x (↑e.symm i)
[PROOFSTEP]
unfold dotProduct
[GOAL]
case h.e'_4
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
this : mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
⊢ (Finset.sum Finset.univ fun i => star x i * ((mulVec M fun i => x (↑e.symm i)) ∘ ↑e) i) =
    Finset.sum Finset.univ fun i => star (fun i => x (↑e.symm i)) i * mulVec M (fun i => x (↑e.symm i)) i
[PROOFSTEP]
rw [Finset.sum_bij' (fun i _ => e i) _ _ fun i _ => e.symm i]
[GOAL]
case h.e'_4.hj
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
this : mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
⊢ ∀ (a : n), a ∈ Finset.univ → ↑e.symm a ∈ Finset.univ
[PROOFSTEP]
simp
[GOAL]
case h.e'_4.left_inv
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
this : mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
⊢ ∀ (a : m), a ∈ Finset.univ → ↑e.symm (↑e a) = a
[PROOFSTEP]
simp
[GOAL]
case h.e'_4.right_inv
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
this : mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
⊢ ∀ (a : n), a ∈ Finset.univ → ↑e (↑e.symm a) = a
[PROOFSTEP]
simp
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
this : mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
⊢ ∀ (a : m) (ha : a ∈ Finset.univ), (fun i x => ↑e i) a ha ∈ Finset.univ
[PROOFSTEP]
simp
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
this : mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
⊢ ∀ (a : m) (ha : a ∈ Finset.univ),
    star x a * ((mulVec M fun i => x (↑e.symm i)) ∘ ↑e) a =
      star (fun i => x (↑e.symm i)) ((fun i x => ↑e i) a ha) *
        mulVec M (fun i => x (↑e.symm i)) ((fun i x => ↑e i) a ha)
[PROOFSTEP]
simp
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
e : m ≃ n
h : PosSemidef (submatrix M ↑e ↑e)
⊢ PosSemidef M
[PROOFSTEP]
simpa using h.submatrix e.symm
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosDef M
⊢ PosDef Mᵀ
[PROOFSTEP]
refine ⟨IsHermitian.transpose hM.1, fun x hx => ?_⟩
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosDef M
x : n → R
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ mulVec Mᵀ x
[PROOFSTEP]
convert hM.2 (star x) (star_ne_zero.2 hx) using 1
[GOAL]
case h.e'_4
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosDef M
x : n → R
hx : x ≠ 0
⊢ star x ⬝ᵥ mulVec Mᵀ x = star (star x) ⬝ᵥ mulVec M (star x)
[PROOFSTEP]
rw [mulVec_transpose, Matrix.dotProduct_mulVec, star_star, dotProduct_comm]
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : IsSymm M
hMq : QuadraticForm.PosDef (toQuadraticForm' M)
⊢ PosDef M
[PROOFSTEP]
refine' ⟨hM, fun x hx => _⟩
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : IsSymm M
hMq : QuadraticForm.PosDef (toQuadraticForm' M)
x : n → ℝ
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ mulVec M x
[PROOFSTEP]
simp only [toQuadraticForm', QuadraticForm.PosDef, BilinForm.toQuadraticForm_apply, Matrix.toBilin'_apply'] at hMq 
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : IsSymm M
x : n → ℝ
hx : x ≠ 0
hMq : ∀ (x : n → ℝ), x ≠ 0 → 0 < x ⬝ᵥ mulVec M x
⊢ 0 < star x ⬝ᵥ mulVec M x
[PROOFSTEP]
apply hMq x hx
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : PosDef M
⊢ QuadraticForm.PosDef (toQuadraticForm' M)
[PROOFSTEP]
intro x hx
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : PosDef M
x : n → ℝ
hx : x ≠ 0
⊢ 0 < ↑(toQuadraticForm' M) x
[PROOFSTEP]
simp only [toQuadraticForm', BilinForm.toQuadraticForm_apply, Matrix.toBilin'_apply']
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : PosDef M
x : n → ℝ
hx : x ≠ 0
⊢ 0 < x ⬝ᵥ mulVec M x
[PROOFSTEP]
apply hM.2 x hx
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
A : Matrix m n R
⊢ PosSemidef (Aᴴ * A)
[PROOFSTEP]
refine ⟨isHermitian_transpose_mul_self _, fun x => ?_⟩
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
A : Matrix m n R
x : n → R
⊢ 0 ≤ star x ⬝ᵥ mulVec (Aᴴ * A) x
[PROOFSTEP]
rw [← mulVec_mulVec, dotProduct_mulVec, vecMul_conjTranspose, star_star]
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
A : Matrix m n R
x : n → R
⊢ 0 ≤ star (mulVec A x) ⬝ᵥ mulVec A x
[PROOFSTEP]
exact Finset.sum_nonneg fun i _ => star_mul_self_nonneg _
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
A : Matrix m n R
⊢ PosSemidef (A * Aᴴ)
[PROOFSTEP]
simpa only [conjTranspose_conjTranspose] using posSemidef_conjTranspose_mul_self Aᴴ
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarOrderedRing R
inst✝² : IsROrC 𝕜
inst✝¹ : DecidableEq n
inst✝ : DecidableEq 𝕜
A : Matrix n n 𝕜
hA : PosDef A
i : n
⊢ 0 < IsHermitian.eigenvalues (_ : IsHermitian A) i
[PROOFSTEP]
rw [hA.1.eigenvalues_eq, hA.1.transpose_eigenvectorMatrix_apply]
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarOrderedRing R
inst✝² : IsROrC 𝕜
inst✝¹ : DecidableEq n
inst✝ : DecidableEq 𝕜
A : Matrix n n 𝕜
hA : PosDef A
i : n
⊢ 0 <
    ↑IsROrC.re
      (star (↑(IsHermitian.eigenvectorBasis (_ : IsHermitian A)) i) ⬝ᵥ
        mulVec A (↑(IsHermitian.eigenvectorBasis (_ : IsHermitian A)) i))
[PROOFSTEP]
exact hA.re_dotProduct_pos <| hA.1.eigenvectorBasis.orthonormal.ne_zero i
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
M : Matrix n n ℝ
hM : PosDef M
inst✝ : DecidableEq n
⊢ 0 < det M
[PROOFSTEP]
rw [hM.isHermitian.det_eq_prod_eigenvalues]
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
M : Matrix n n ℝ
hM : PosDef M
inst✝ : DecidableEq n
⊢ 0 < Finset.prod Finset.univ fun i => ↑(IsHermitian.eigenvalues (_ : IsHermitian M) i)
[PROOFSTEP]
apply Finset.prod_pos
[GOAL]
case h0
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
M : Matrix n n ℝ
hM : PosDef M
inst✝ : DecidableEq n
⊢ ∀ (i : n), i ∈ Finset.univ → 0 < ↑(IsHermitian.eigenvalues (_ : IsHermitian M) i)
[PROOFSTEP]
intro i _
[GOAL]
case h0
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
M : Matrix n n ℝ
hM : PosDef M
inst✝ : DecidableEq n
i : n
a✝ : i ∈ Finset.univ
⊢ 0 < ↑(IsHermitian.eigenvalues (_ : IsHermitian M) i)
[PROOFSTEP]
rw [hM.isHermitian.eigenvalues_eq]
[GOAL]
case h0
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
M : Matrix n n ℝ
hM : PosDef M
inst✝ : DecidableEq n
i : n
a✝ : i ∈ Finset.univ
⊢ 0 <
    ↑(↑IsROrC.re
        (star ((IsHermitian.eigenvectorMatrix (_ : IsHermitian M))ᵀ i) ⬝ᵥ
          mulVec M ((IsHermitian.eigenvectorMatrix (_ : IsHermitian M))ᵀ i)))
[PROOFSTEP]
refine hM.2 _ fun h => ?_
[GOAL]
case h0
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
M : Matrix n n ℝ
hM : PosDef M
inst✝ : DecidableEq n
i : n
a✝ : i ∈ Finset.univ
h : (IsHermitian.eigenvectorMatrix (_ : IsHermitian M))ᵀ i = 0
⊢ False
[PROOFSTEP]
have h_det : hM.isHermitian.eigenvectorMatrixᵀ.det = 0 := Matrix.det_eq_zero_of_row_eq_zero i fun j => congr_fun h j
[GOAL]
case h0
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
M : Matrix n n ℝ
hM : PosDef M
inst✝ : DecidableEq n
i : n
a✝ : i ∈ Finset.univ
h : (IsHermitian.eigenvectorMatrix (_ : IsHermitian M))ᵀ i = 0
h_det : det (IsHermitian.eigenvectorMatrix (_ : IsHermitian M))ᵀ = 0
⊢ False
[PROOFSTEP]
simpa only [h_det, not_isUnit_zero] using isUnit_det_of_invertible hM.isHermitian.eigenvectorMatrixᵀ
[GOAL]
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : Matrix.PosDef (toMatrix' Q)
⊢ PosDef Q
[PROOFSTEP]
rw [← toQuadraticForm_associated ℝ Q, ← BilinForm.toMatrix'.left_inv ((associatedHom ℝ) Q)]
[GOAL]
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : Matrix.PosDef (toMatrix' Q)
⊢ PosDef
    (BilinForm.toQuadraticForm
      (LinearEquiv.invFun BilinForm.toMatrix' (AddHom.toFun (↑BilinForm.toMatrix').toAddHom (↑(associatedHom ℝ) Q))))
[PROOFSTEP]
apply Matrix.posDef_toQuadraticForm' hQ
[GOAL]
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : PosDef Q
⊢ Matrix.PosDef (toMatrix' Q)
[PROOFSTEP]
rw [← toQuadraticForm_associated ℝ Q, ← BilinForm.toMatrix'.left_inv ((associatedHom ℝ) Q)] at hQ 
[GOAL]
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ :
  PosDef
    (BilinForm.toQuadraticForm
      (LinearEquiv.invFun BilinForm.toMatrix' (AddHom.toFun (↑BilinForm.toMatrix').toAddHom (↑(associatedHom ℝ) Q))))
⊢ Matrix.PosDef (toMatrix' Q)
[PROOFSTEP]
apply Matrix.posDef_of_toQuadraticForm' (isSymm_toMatrix' Q) hQ
[GOAL]
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
x y : n → 𝕜
⊢ ↑(starRingEnd 𝕜) (inner y x) = inner x y
[PROOFSTEP]
dsimp only [Inner.inner]
[GOAL]
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
x y : n → 𝕜
⊢ ↑(starRingEnd 𝕜) (star y ⬝ᵥ mulVec M x) = star x ⬝ᵥ mulVec M y
[PROOFSTEP]
rw [star_dotProduct, starRingEnd_apply, star_star, star_mulVec, dotProduct_mulVec, hM.isHermitian.eq]
[GOAL]
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
x : n → 𝕜
⊢ 0 ≤ ↑IsROrC.re (inner x x)
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
x : n → 𝕜
h : x = 0
⊢ 0 ≤ ↑IsROrC.re (inner x x)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
x : n → 𝕜
h : ¬x = 0
⊢ 0 ≤ ↑IsROrC.re (inner x x)
[PROOFSTEP]
exact le_of_lt (hM.re_dotProduct_pos h)
[GOAL]
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
x : n → 𝕜
hx : star x ⬝ᵥ mulVec M x = 0
⊢ x = 0
[PROOFSTEP]
by_contra' h
[GOAL]
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
x : n → 𝕜
hx : star x ⬝ᵥ mulVec M x = 0
h : x ≠ 0
⊢ False
[PROOFSTEP]
simpa [hx, lt_irrefl] using hM.re_dotProduct_pos h
[GOAL]
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
⊢ ∀ (x y z : n → 𝕜), inner (x + y) z = inner x z + inner y z
[PROOFSTEP]
simp only [star_add, add_dotProduct, eq_self_iff_true, forall_const]
[GOAL]
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
x y : n → 𝕜
r : 𝕜
⊢ inner (r • x) y = ↑(starRingEnd 𝕜) r * inner x y
[PROOFSTEP]
simp only
[GOAL]
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
x y : n → 𝕜
r : 𝕜
⊢ star (r • x) ⬝ᵥ mulVec M y = ↑(starRingEnd 𝕜) r * star x ⬝ᵥ mulVec M y
[PROOFSTEP]
rw [← smul_eq_mul, ← smul_dotProduct, starRingEnd_apply, ← star_smul]
