Theorem: Matrix.PosSemidef.add (CvxLean/Lib/Math/LinearAlgebra/Matrix/PosDef.lean)

State before:
m : Type ?u.47670
n : Type u_1
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
M N : Matrix n n 𝕜
hM : M.PosSemidef
hN : N.PosSemidef
⊢ (M + N).PosSemidef
Tactic:
refine' ⟨hM.1.add hN.1, _⟩
State after:
m : Type ?u.47670
n : Type u_1
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
M N : Matrix n n 𝕜
hM : M.PosSemidef
hN : N.PosSemidef
⊢ ∀ (x : n → 𝕜), 0 ≤ star x ⬝ᵥ (M + N).mulVec x

State before:
m : Type ?u.47670
n : Type u_1
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
M N : Matrix n n 𝕜
hM : M.PosSemidef
hN : N.PosSemidef
⊢ ∀ (x : n → 𝕜), 0 ≤ star x ⬝ᵥ (M + N).mulVec x
Tactic:
intros x
State after:
m : Type ?u.47670
n : Type u_1
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
M N : Matrix n n 𝕜
hM : M.PosSemidef
hN : N.PosSemidef
x : n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ (M + N).mulVec x

State before:
m : Type ?u.47670
n : Type u_1
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
M N : Matrix n n 𝕜
hM : M.PosSemidef
hN : N.PosSemidef
x : n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ (M + N).mulVec x
Tactic:
simp only [add_mulVec, dotProduct_add, map_add]
State after:
m : Type ?u.47670
n : Type u_1
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
M N : Matrix n n 𝕜
hM : M.PosSemidef
hN : N.PosSemidef
x : n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ M.mulVec x + star x ⬝ᵥ N.mulVec x

State before:
m : Type ?u.47670
n : Type u_1
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
M N : Matrix n n 𝕜
hM : M.PosSemidef
hN : N.PosSemidef
x : n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ M.mulVec x + star x ⬝ᵥ N.mulVec x
Tactic:
apply add_nonneg (hM.2 x) (hN.2 x)
State after:
no goals