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

State before:
m : Type ?u.6640
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.6652
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ (diagonal f).PosSemidef
Tactic:
refine' ⟨isHermitian_diagonal _, _⟩
State after:
m : Type ?u.6640
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.6652
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ ∀ (x : n → ℝ), 0 ≤ star x ⬝ᵥ (diagonal f).mulVec x

State before:
m : Type ?u.6640
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.6652
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ ∀ (x : n → ℝ), 0 ≤ star x ⬝ᵥ (diagonal f).mulVec x
Tactic:
intro x
State after:
m : Type ?u.6640
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.6652
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
x : n → ℝ
⊢ 0 ≤ star x ⬝ᵥ (diagonal f).mulVec x

State before:
m : Type ?u.6640
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.6652
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
x : n → ℝ
⊢ 0 ≤ star x ⬝ᵥ (diagonal f).mulVec x
Tactic:
simp only [star, id_def, RCLike.re_to_real]
State after:
m : Type ?u.6640
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.6652
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
x : n → ℝ
⊢ 0 ≤ (fun i => x i) ⬝ᵥ (diagonal f).mulVec x

State before:
m : Type ?u.6640
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.6652
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
x : n → ℝ
⊢ 0 ≤ (fun i => x i) ⬝ᵥ (diagonal f).mulVec x
Tactic:
apply Finset.sum_nonneg'
State after:
case h
m : Type ?u.6640
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.6652
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
x : n → ℝ
⊢ ∀ (i : n), 0 ≤ (fun i => x i) i * (diagonal f).mulVec x i

State before:
case h
m : Type ?u.6640
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.6652
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
x : n → ℝ
⊢ ∀ (i : n), 0 ≤ (fun i => x i) i * (diagonal f).mulVec x i
Tactic:
intro i
State after:
case h
m : Type ?u.6640
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.6652
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
x : n → ℝ
i : n
⊢ 0 ≤ (fun i => x i) i * (diagonal f).mulVec x i

State before:
case h
m : Type ?u.6640
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.6652
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
x : n → ℝ
i : n
⊢ 0 ≤ (fun i => x i) i * (diagonal f).mulVec x i
Tactic:
rw [mulVec_diagonal f x i, mul_comm, mul_assoc]
State after:
case h
m : Type ?u.6640
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.6652
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
x : n → ℝ
i : n
⊢ 0 ≤ f i * (x i * (fun i => x i) i)

State before:
case h
m : Type ?u.6640
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.6652
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
x : n → ℝ
i : n
⊢ 0 ≤ f i * (x i * (fun i => x i) i)
Tactic:
exact mul_nonneg (hf i) (mul_self_nonneg (x i))
State after:
no goals