Theorem: Matrix.PosSemidef.PosDef_iff_det_ne_zero (CvxLean/Lib/Math/Subadditivity.lean)

State before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
⊢ M.PosDef ↔ M.det ≠ 0
Tactic:
refine' ⟨PosDef.det_ne_zero, _⟩
State after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
⊢ M.det ≠ 0 → M.PosDef

State before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
⊢ M.det ≠ 0 → M.PosDef
Tactic:
intro hdet
State after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
⊢ M.PosDef

State before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
⊢ M.PosDef
Tactic:
refine' ⟨hM.1, _⟩
State after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
⊢ ∀ (x : n → ℝ), x ≠ 0 → 0 < star x ⬝ᵥ M.mulVec x

State before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
⊢ ∀ (x : n → ℝ), x ≠ 0 → 0 < star x ⬝ᵥ M.mulVec x
Tactic:
intros x hx
State after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
x : n → ℝ
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ M.mulVec x

State before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
x : n → ℝ
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ M.mulVec x
Tactic:
apply lt_of_le_of_ne' (hM.2 x)
State after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
x : n → ℝ
hx : x ≠ 0
⊢ star x ⬝ᵥ M.mulVec x ≠ 0

State before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
x : n → ℝ
hx : x ≠ 0
⊢ star x ⬝ᵥ M.mulVec x ≠ 0
Tactic:
rw [← hM.sqrt_mul_sqrt, ← mulVec_mulVec, dotProduct_mulVec, ← transpose_transpose hM.1.sqrt,
  vecMul_transpose, transpose_transpose, ← conjTranspose_eq_transpose,
  hM.PosSemidef_sqrt.1.eq]
State after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
x : n → ℝ
hx : x ≠ 0
⊢ ⋯.sqrt.mulVec (star x) ⬝ᵥ ⋯.sqrt.mulVec x ≠ 0

State before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
x : n → ℝ
hx : x ≠ 0
⊢ ⋯.sqrt.mulVec (star x) ⬝ᵥ ⋯.sqrt.mulVec x ≠ 0
Tactic:
simp only [RCLike.re_to_real, star, id]
State after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
x : n → ℝ
hx : x ≠ 0
⊢ (⋯.sqrt.mulVec fun i => x i) ⬝ᵥ ⋯.sqrt.mulVec x ≠ 0

State before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
x : n → ℝ
hx : x ≠ 0
⊢ (⋯.sqrt.mulVec fun i => x i) ⬝ᵥ ⋯.sqrt.mulVec x ≠ 0
Tactic:
change @inner ℝ (EuclideanSpace ℝ _) _ (hM.1.sqrt.mulVec x) (hM.1.sqrt.mulVec x) ≠ 0
State after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
x : n → ℝ
hx : x ≠ 0
⊢ ⟪⋯.sqrt.mulVec x, ⋯.sqrt.mulVec x⟫_ℝ ≠ 0

State before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
x : n → ℝ
hx : x ≠ 0
⊢ ⟪⋯.sqrt.mulVec x, ⋯.sqrt.mulVec x⟫_ℝ ≠ 0
Tactic:
intro hinner
State after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
x : n → ℝ
hx : x ≠ 0
hinner : ⟪⋯.sqrt.mulVec x, ⋯.sqrt.mulVec x⟫_ℝ = 0
⊢ False

State before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
x : n → ℝ
hx : x ≠ 0
hinner : ⟪⋯.sqrt.mulVec x, ⋯.sqrt.mulVec x⟫_ℝ = 0
⊢ False
Tactic:
have sqrtMdet0 : hM.1.sqrt.det = 0 := by
  refine' exists_mulVec_eq_zero_iff.1 ⟨x, hx, _⟩
  rw [inner_self_eq_zero.1 hinner]
State after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
x : n → ℝ
hx : x ≠ 0
hinner : ⟪⋯.sqrt.mulVec x, ⋯.sqrt.mulVec x⟫_ℝ = 0
sqrtMdet0 : ⋯.sqrt.det = 0
⊢ False

State before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
x : n → ℝ
hx : x ≠ 0
hinner : ⟪⋯.sqrt.mulVec x, ⋯.sqrt.mulVec x⟫_ℝ = 0
sqrtMdet0 : ⋯.sqrt.det = 0
⊢ False
Tactic:
rw [← hM.sqrt_mul_sqrt, det_mul, sqrtMdet0, mul_zero] at hdet
State after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : 0 ≠ 0
x : n → ℝ
hx : x ≠ 0
hinner : ⟪⋯.sqrt.mulVec x, ⋯.sqrt.mulVec x⟫_ℝ = 0
sqrtMdet0 : ⋯.sqrt.det = 0
⊢ False

State before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : 0 ≠ 0
x : n → ℝ
hx : x ≠ 0
hinner : ⟪⋯.sqrt.mulVec x, ⋯.sqrt.mulVec x⟫_ℝ = 0
sqrtMdet0 : ⋯.sqrt.det = 0
⊢ False
Tactic:
apply hdet rfl
State after:
no goals

State before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
x : n → ℝ
hx : x ≠ 0
hinner : ⟪⋯.sqrt.mulVec x, ⋯.sqrt.mulVec x⟫_ℝ = 0
⊢ ⋯.sqrt.det = 0
Tactic:
refine' exists_mulVec_eq_zero_iff.1 ⟨x, hx, _⟩
State after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
x : n → ℝ
hx : x ≠ 0
hinner : ⟪⋯.sqrt.mulVec x, ⋯.sqrt.mulVec x⟫_ℝ = 0
⊢ ⋯.sqrt.mulVec x = 0

State before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosSemidef
hdet : M.det ≠ 0
x : n → ℝ
hx : x ≠ 0
hinner : ⟪⋯.sqrt.mulVec x, ⋯.sqrt.mulVec x⟫_ℝ = 0
⊢ ⋯.sqrt.mulVec x = 0
Tactic:
rw [inner_self_eq_zero.1 hinner]
State after:
no goals