internlm/Lean-Github huggingface dataset:
Theorem: Matrix.PosDef_diagonal
Proof 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
Proof 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
Theorem: Matrix.PosDef_diagonal
Proof 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)
Proof 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
Theorem: Matrix.PosDef_diagonal
Proof 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)))]
Proof 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
Theorem: Matrix.PosDef_diagonal
Proof 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
Proof state after:
no goals
Theorem: Matrix.PosSemidef.conjTranspose_mul_mul
Proof state before:
m : Type ?u.23145
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
⊢ (N.conjTranspose * M * N).PosSemidef
Tactic:
refine' ⟨isHermitian_conjTranspose_mul_mul _ hM.1, _⟩
Proof state after:
m : Type ?u.23145
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
⊢ ∀ (x : n → 𝕜), 0 ≤ star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x
Theorem: Matrix.PosSemidef.conjTranspose_mul_mul
Proof state before:
m : Type ?u.23145
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
⊢ ∀ (x : n → 𝕜), 0 ≤ star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x
Tactic:
intro x
Proof state after:
m : Type ?u.23145
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
x : n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x
Theorem: Matrix.PosSemidef.conjTranspose_mul_mul
Proof state before:
m : Type ?u.23145
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
x : n → 𝕜
⊢ 0 ≤ star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x
Tactic:
convert hM.2 (N.mulVec x) using 1
Proof state after:
case h.e'_4
m : Type ?u.23145
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
x : n → 𝕜
⊢ star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x = star (N.mulVec x) ⬝ᵥ M.mulVec (N.mulVec x)
Theorem: Matrix.PosSemidef.conjTranspose_mul_mul
Proof state before:
case h.e'_4
m : Type ?u.23145
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
x : n → 𝕜
⊢ star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x = star (N.mulVec x) ⬝ᵥ M.mulVec (N.mulVec x)
Tactic:
rw [mul_assoc, mulVec_mulVec, ← mulVec_mulVec, dotProduct_mulVec, star_mulVec]
Proof state after:
no goals
Theorem: Matrix.PosDef.conjTranspose_mul_mul
Proof state before:
m : Type ?u.28307
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 N : Matrix n n 𝕜
hM : M.PosDef
hN : N.det ≠ 0
⊢ (N.conjTranspose * M * N).PosDef
Tactic:
refine' ⟨isHermitian_conjTranspose_mul_mul _ hM.1, _⟩
Proof state after:
m : Type ?u.28307
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 N : Matrix n n 𝕜
hM : M.PosDef
hN : N.det ≠ 0
⊢ ∀ (x : n → 𝕜), x ≠ 0 → 0 < star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x
Theorem: Matrix.PosDef.conjTranspose_mul_mul
Proof state before:
m : Type ?u.28307
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 N : Matrix n n 𝕜
hM : M.PosDef
hN : N.det ≠ 0
⊢ ∀ (x : n → 𝕜), x ≠ 0 → 0 < star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x
Tactic:
intros x hx
Proof state after:
m : Type ?u.28307
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 N : Matrix n n 𝕜
hM : M.PosDef
hN : N.det ≠ 0
x : n → 𝕜
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x
Theorem: Matrix.PosDef.conjTranspose_mul_mul
Proof state before:
m : Type ?u.28307
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 N : Matrix n n 𝕜
hM : M.PosDef
hN : N.det ≠ 0
x : n → 𝕜
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x
Tactic:
convert
  hM.2 (N.mulVec x) (fun h => hx (eq_zero_of_mulVec_eq_zero hN h)) using 1
Proof state after:
case h.e'_4
m : Type ?u.28307
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 N : Matrix n n 𝕜
hM : M.PosDef
hN : N.det ≠ 0
x : n → 𝕜
hx : x ≠ 0
⊢ star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x = star (N.mulVec x) ⬝ᵥ M.mulVec (N.mulVec x)
Theorem: Matrix.PosDef.conjTranspose_mul_mul
Proof state before:
case h.e'_4
m : Type ?u.28307
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 N : Matrix n n 𝕜
hM : M.PosDef
hN : N.det ≠ 0
x : n → 𝕜
hx : x ≠ 0
⊢ star x ⬝ᵥ (N.conjTranspose * M * N).mulVec x = star (N.mulVec x) ⬝ᵥ M.mulVec (N.mulVec x)
Tactic:
rw [Matrix.mul_assoc, mulVec_mulVec, ← mulVec_mulVec, dotProduct_mulVec,
  star_mulVec]
Proof state after:
no goals
Theorem: Matrix.IsHermitian.nonsingular_inv
Proof state before:
m : Type ?u.34280
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.IsHermitian
hMdet : IsUnit M.det
⊢ M⁻¹.IsHermitian
Tactic:
refine' (Matrix.inv_eq_right_inv _).symm
Proof state after:
m : Type ?u.34280
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.IsHermitian
hMdet : IsUnit M.det
⊢ M * M⁻¹.conjTranspose = 1
Theorem: Matrix.IsHermitian.nonsingular_inv
Proof state before:
m : Type ?u.34280
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.IsHermitian
hMdet : IsUnit M.det
⊢ M * M⁻¹.conjTranspose = 1
Tactic:
rw [conjTranspose_nonsing_inv, hM.eq, mul_nonsing_inv _ hMdet]
Proof state after:
no goals
Theorem: Matrix.conj_symm
Proof state before:
m : Type ?u.36361
n : Type u_1
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
x : n → 𝕜
M : Matrix n n 𝕜
hM : M.IsHermitian
⊢ star (star x ⬝ᵥ M.mulVec x) = star x ⬝ᵥ M.mulVec x
Tactic:
nth_rewrite 1 [star_dotProduct, star_mulVec]
Proof state after:
m : Type ?u.36361
n : Type u_1
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
x : n → 𝕜
M : Matrix n n 𝕜
hM : M.IsHermitian
⊢ star (star (star x ᵥ* M.conjTranspose ⬝ᵥ x)) = star x ⬝ᵥ M.mulVec x
Theorem: Matrix.conj_symm
Proof state before:
m : Type ?u.36361
n : Type u_1
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
x : n → 𝕜
M : Matrix n n 𝕜
hM : M.IsHermitian
⊢ star (star (star x ᵥ* M.conjTranspose ⬝ᵥ x)) = star x ⬝ᵥ M.mulVec x
Tactic:
rw [star_star, dotProduct_mulVec, hM.eq]
Proof state after:
no goals
Theorem: Matrix.PosDef.nonsingular_inv
Proof 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), _⟩
Proof 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
Theorem: Matrix.PosDef.nonsingular_inv
Proof 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
Proof 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
Theorem: Matrix.PosDef.nonsingular_inv
Proof 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)
Proof 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
Theorem: Matrix.PosDef.nonsingular_inv
Proof 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
Proof 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
Theorem: Matrix.PosDef.nonsingular_inv
Proof 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))
Proof 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
Theorem: Matrix.PosDef.nonsingular_inv
Proof 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
Proof 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
Theorem: Matrix.PosDef.nonsingular_inv
Proof 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
Proof 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
Theorem: Matrix.PosDef.nonsingular_inv
Proof 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
Proof state after:
no goals
Theorem: Matrix.PosSemidef.mul_mul_of_IsHermitian
Proof state before:
m : Type ?u.45085
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.IsHermitian
⊢ (N * M * N).PosSemidef
Tactic:
convert hM.conjTranspose_mul_mul M N
Proof state after:
case h.e'_8.h.e'_5.h.e'_5
m : Type ?u.45085
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.IsHermitian
⊢ N = N.conjTranspose
Theorem: Matrix.PosSemidef.mul_mul_of_IsHermitian
Proof state before:
case h.e'_8.h.e'_5.h.e'_5
m : Type ?u.45085
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.IsHermitian
⊢ N = N.conjTranspose
Tactic:
exact hN.symm
Proof state after:
no goals
Theorem: Matrix.PosSemidef.add
Proof 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, _⟩
Proof 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
Theorem: Matrix.PosSemidef.add
Proof 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
Proof 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
Theorem: Matrix.PosSemidef.add
Proof 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]
Proof 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
Theorem: Matrix.PosSemidef.add
Proof 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)
Proof state after:
no goals
Theorem: Matrix.isUnit_det_of_PosDef_inv
Proof state before:
m : Type ?u.49238
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.49250
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
h : M⁻¹.PosDef
⊢ IsUnit M.det
Tactic:
apply isUnit_iff_ne_zero.2
Proof state after:
m : Type ?u.49238
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.49250
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
h : M⁻¹.PosDef
⊢ M.det ≠ 0
Theorem: Matrix.isUnit_det_of_PosDef_inv
Proof state before:
m : Type ?u.49238
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.49250
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
h : M⁻¹.PosDef
⊢ M.det ≠ 0
Tactic:
have := h.isUnit_det
Proof state after:
m : Type ?u.49238
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.49250
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
h : M⁻¹.PosDef
this : IsUnit M⁻¹.det
⊢ M.det ≠ 0
Theorem: Matrix.isUnit_det_of_PosDef_inv
Proof state before:
m : Type ?u.49238
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.49250
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
h : M⁻¹.PosDef
this : IsUnit M⁻¹.det
⊢ M.det ≠ 0
Tactic:
rw [det_nonsing_inv, isUnit_ring_inverse] at this
Proof state after:
m : Type ?u.49238
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.49250
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
h : M⁻¹.PosDef
this : IsUnit M.det
⊢ M.det ≠ 0
Theorem: Matrix.isUnit_det_of_PosDef_inv
Proof state before:
m : Type ?u.49238
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.49250
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
h : M⁻¹.PosDef
this : IsUnit M.det
⊢ M.det ≠ 0
Tactic:
apply IsUnit.ne_zero this
Proof state after:
no goals