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

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

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

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

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

case hs
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : x ≠ 0
⊢ ∃ i ∈ Finset.univ, 0 < (fun i => x i) i * (diagonal f).mulVec x i

State before:
case h
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : x ≠ 0
⊢ ∀ i ∈ Finset.univ, 0 ≤ (fun i => x i) i * (diagonal f).mulVec x i

case hs
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : x ≠ 0
⊢ ∃ i ∈ Finset.univ, 0 < (fun i => x i) i * (diagonal f).mulVec x i
Tactic:
{ intros i _
  rw [mulVec_diagonal f x i, mul_comm, mul_assoc]
  exact mul_nonneg (le_of_lt (hf i)) (mul_self_nonneg (x i)) }
State after:
case hs
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : x ≠ 0
⊢ ∃ i ∈ Finset.univ, 0 < (fun i => x i) i * (diagonal f).mulVec x i

State before:
case hs
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : x ≠ 0
⊢ ∃ i ∈ Finset.univ, 0 < (fun i => x i) i * (diagonal f).mulVec x i
Tactic:
{ contrapose hx; simp at hx ⊢
  ext i
  have := hx i
  rw [mulVec_diagonal f x i, mul_comm, mul_assoc] at this
  have := nonpos_of_mul_nonpos_right this (hf i)
  rw [mul_self_eq_zero.1 (le_antisymm this (mul_self_nonneg (x i)))]
  rfl }
State after:
no goals

State before:
case h
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : x ≠ 0
⊢ ∀ i ∈ Finset.univ, 0 ≤ (fun i => x i) i * (diagonal f).mulVec x i
Tactic:
intros i _
State after:
case h
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : x ≠ 0
i : n
a✝ : i ∈ Finset.univ
⊢ 0 ≤ (fun i => x i) i * (diagonal f).mulVec x i

State before:
case h
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : x ≠ 0
i : n
a✝ : i ∈ Finset.univ
⊢ 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.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : x ≠ 0
i : n
a✝ : i ∈ Finset.univ
⊢ 0 ≤ f i * (x i * (fun i => x i) i)

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

State before:
case hs
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : x ≠ 0
⊢ ∃ i ∈ Finset.univ, 0 < (fun i => x i) i * (diagonal f).mulVec x i
Tactic:
contrapose hx
State after:
case hs
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : ¬∃ i ∈ Finset.univ, 0 < (fun i => x i) i * (diagonal f).mulVec x i
⊢ ¬x ≠ 0

State before:
case hs
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : ¬∃ i ∈ Finset.univ, 0 < (fun i => x i) i * (diagonal f).mulVec x i
⊢ ¬x ≠ 0
Tactic:
simp at hx ⊢
State after:
case hs
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : ∀ (x_1 : n), x x_1 * (diagonal f).mulVec x x_1 ≤ 0
⊢ x = 0

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

State before:
case hs.h
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : ∀ (x_1 : n), x x_1 * (diagonal f).mulVec x x_1 ≤ 0
i : n
⊢ x i = 0 i
Tactic:
have := hx i
State after:
case hs.h
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : ∀ (x_1 : n), x x_1 * (diagonal f).mulVec x x_1 ≤ 0
i : n
this : x i * (diagonal f).mulVec x i ≤ 0
⊢ x i = 0 i

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

State before:
case hs.h
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : ∀ (x_1 : n), x x_1 * (diagonal f).mulVec x x_1 ≤ 0
i : n
this : f i * (x i * x i) ≤ 0
⊢ x i = 0 i
Tactic:
have := nonpos_of_mul_nonpos_right this (hf i)
State after:
case hs.h
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : ∀ (x_1 : n), x x_1 * (diagonal f).mulVec x x_1 ≤ 0
i : n
this✝ : f i * (x i * x i) ≤ 0
this : x i * x i ≤ 0
⊢ x i = 0 i

State before:
case hs.h
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : ∀ (x_1 : n), x x_1 * (diagonal f).mulVec x x_1 ≤ 0
i : n
this✝ : f i * (x i * x i) ≤ 0
this : x i * x i ≤ 0
⊢ x i = 0 i
Tactic:
rw [mul_self_eq_zero.1 (le_antisymm this (mul_self_nonneg (x i)))]
State after:
case hs.h
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : ∀ (x_1 : n), x x_1 * (diagonal f).mulVec x x_1 ≤ 0
i : n
this✝ : f i * (x i * x i) ≤ 0
this : x i * x i ≤ 0
⊢ 0 = 0 i

State before:
case hs.h
m : Type ?u.8318
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.8330
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
f : n → ℝ
hf : ∀ (i : n), 0 < f i
x : n → ℝ
hx : ∀ (x_1 : n), x x_1 * (diagonal f).mulVec x x_1 ≤ 0
i : n
this✝ : f i * (x i * x i) ≤ 0
this : x i * x i ≤ 0
⊢ 0 = 0 i
Tactic:
rfl
State after:
no goals