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

State before:
m : Type ?u.40080
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
⊢ M⁻¹.PosDef
Tactic:
refine' ⟨hM.1.nonsingular_inv (isUnit_iff_ne_zero.2 hM.det_ne_zero), _⟩
State after:
m : Type ?u.40080
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
⊢ ∀ (x : n → 𝕜), x ≠ 0 → 0 < star x ⬝ᵥ M⁻¹.mulVec x

State before:
m : Type ?u.40080
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
⊢ ∀ (x : n → 𝕜), x ≠ 0 → 0 < star x ⬝ᵥ M⁻¹.mulVec x
Tactic:
intros x hx
State after:
m : Type ?u.40080
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ M⁻¹.mulVec x

State before:
m : Type ?u.40080
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ M⁻¹.mulVec x
Tactic:
have hMMinv := mul_nonsing_inv _ (isUnit_iff_ne_zero.2 hM.det_ne_zero)
State after:
m : Type ?u.40080
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
hMMinv : M * M⁻¹ = 1
⊢ 0 < star x ⬝ᵥ M⁻¹.mulVec x

State before:
m : Type ?u.40080
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
hMMinv : M * M⁻¹ = 1
⊢ 0 < star x ⬝ᵥ M⁻¹.mulVec x
Tactic:
have hMinvdet : M⁻¹.det ≠ 0 := det_ne_zero_of_left_inverse hMMinv
State after:
m : Type ?u.40080
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
hMMinv : M * M⁻¹ = 1
hMinvdet : M⁻¹.det ≠ 0
⊢ 0 < star x ⬝ᵥ M⁻¹.mulVec x

State before:
m : Type ?u.40080
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
hMMinv : M * M⁻¹ = 1
hMinvdet : M⁻¹.det ≠ 0
⊢ 0 < star x ⬝ᵥ M⁻¹.mulVec x
Tactic:
have hres :=
  hM.2 (M⁻¹.mulVec x) (fun h => hx (eq_zero_of_mulVec_eq_zero hMinvdet h))
State after:
m : Type ?u.40080
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
hMMinv : M * M⁻¹ = 1
hMinvdet : M⁻¹.det ≠ 0
hres : 0 < star (M⁻¹.mulVec x) ⬝ᵥ M.mulVec (M⁻¹.mulVec x)
⊢ 0 < star x ⬝ᵥ M⁻¹.mulVec x

State before:
m : Type ?u.40080
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
hMMinv : M * M⁻¹ = 1
hMinvdet : M⁻¹.det ≠ 0
hres : 0 < star (M⁻¹.mulVec x) ⬝ᵥ M.mulVec (M⁻¹.mulVec x)
⊢ 0 < star x ⬝ᵥ M⁻¹.mulVec x
Tactic:
rw [mulVec_mulVec, hMMinv, one_mulVec, star_dotProduct] at hres
State after:
m : Type ?u.40080
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
hMMinv : M * M⁻¹ = 1
hMinvdet : M⁻¹.det ≠ 0
hres : 0 < star (star x ⬝ᵥ M⁻¹.mulVec x)
⊢ 0 < star x ⬝ᵥ M⁻¹.mulVec x

State before:
m : Type ?u.40080
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
hMMinv : M * M⁻¹ = 1
hMinvdet : M⁻¹.det ≠ 0
hres : 0 < star (star x ⬝ᵥ M⁻¹.mulVec x)
⊢ 0 < star x ⬝ᵥ M⁻¹.mulVec x
Tactic:
rw [conj_symm ((@isHermitian_inv _ _ _ _ _ _ M hM.Invertible).2 hM.1)] at hres
State after:
m : Type ?u.40080
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
hMMinv : M * M⁻¹ = 1
hMinvdet : M⁻¹.det ≠ 0
hres : 0 < star x ⬝ᵥ M⁻¹.mulVec x
⊢ 0 < star x ⬝ᵥ M⁻¹.mulVec x

State before:
m : Type ?u.40080
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : x ≠ 0
hMMinv : M * M⁻¹ = 1
hMinvdet : M⁻¹.det ≠ 0
hres : 0 < star x ⬝ᵥ M⁻¹.mulVec x
⊢ 0 < star x ⬝ᵥ M⁻¹.mulVec x
Tactic:
exact hres
State after:
no goals