internlm/Lean-Github huggingface dataset:
Theorem: Module.End.eigenspace_one
Proof state before:
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ⊤ ≤ eigenspace 1 1
Tactic:
intros x _
Proof state after:
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : M
a✝ : x ∈ ⊤
⊢ x ∈ eigenspace 1 1
Theorem: Module.End.eigenspace_one
Proof state before:
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : M
a✝ : x ∈ ⊤
⊢ x ∈ eigenspace 1 1
Tactic:
simp only [mem_eigenspace_iff, LinearMap.one_apply, one_smul]
Proof state after:
no goals
Theorem: Module.End.has_eigenvector_one
Proof state before:
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : M
hx : x ≠ 0
⊢ x ∈ eigenspace 1 1
Tactic:
rw [eigenspace_one]
Proof state after:
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : M
hx : x ≠ 0
⊢ x ∈ ⊤
Theorem: Module.End.has_eigenvector_one
Proof state before:
K R : Type v
V M : Type w
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : M
hx : x ≠ 0
⊢ x ∈ ⊤
Tactic:
apply Submodule.mem_top
Proof state after:
no goals
Theorem: Matrix.PosSemidef.det_nonneg
Proof state before:
m : Type ?u.340
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.352
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
M : Matrix n n ℝ
hM : M.PosSemidef
inst✝ : DecidableEq n
⊢ 0 ≤ M.det
Tactic:
rw [hM.1.det_eq_prod_eigenvalues]
Proof state after:
m : Type ?u.340
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.352
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
M : Matrix n n ℝ
hM : M.PosSemidef
inst✝ : DecidableEq n
⊢ 0 ≤ Finset.univ.prod fun i => ↑(⋯.eigenvalues i)
Theorem: Matrix.PosSemidef.det_nonneg
Proof state before:
m : Type ?u.340
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.352
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
M : Matrix n n ℝ
hM : M.PosSemidef
inst✝ : DecidableEq n
⊢ 0 ≤ Finset.univ.prod fun i => ↑(⋯.eigenvalues i)
Tactic:
apply Finset.prod_nonneg
Proof state after:
case h0
m : Type ?u.340
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.352
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
M : Matrix n n ℝ
hM : M.PosSemidef
inst✝ : DecidableEq n
⊢ ∀ i ∈ Finset.univ, 0 ≤ ↑(⋯.eigenvalues i)
Theorem: Matrix.PosSemidef.det_nonneg
Proof state before:
case h0
m : Type ?u.340
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.352
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
M : Matrix n n ℝ
hM : M.PosSemidef
inst✝ : DecidableEq n
⊢ ∀ i ∈ Finset.univ, 0 ≤ ↑(⋯.eigenvalues i)
Tactic:
intros i _hi
Proof state after:
case h0
m : Type ?u.340
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.352
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
M : Matrix n n ℝ
hM : M.PosSemidef
inst✝ : DecidableEq n
i : n
_hi : i ∈ Finset.univ
⊢ 0 ≤ ↑(⋯.eigenvalues i)
Theorem: Matrix.PosSemidef.det_nonneg
Proof state before:
case h0
m : Type ?u.340
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.352
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
M : Matrix n n ℝ
hM : M.PosSemidef
inst✝ : DecidableEq n
i : n
_hi : i ∈ Finset.univ
⊢ 0 ≤ ↑(⋯.eigenvalues i)
Tactic:
apply eigenvalues_nonneg hM
Proof state after:
no goals
Theorem: Matrix.PosDef.det_ne_zero
Proof state before:
m : Type ?u.1418
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.det ≠ 0
Tactic:
rw [← Matrix.nondegenerate_iff_det_ne_zero]
Proof state after:
m : Type ?u.1418
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.Nondegenerate
Theorem: Matrix.PosDef.det_ne_zero
Proof state before:
m : Type ?u.1418
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.Nondegenerate
Tactic:
intros v hv
Proof state after:
m : Type ?u.1418
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
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
⊢ v = 0
Theorem: Matrix.PosDef.det_ne_zero
Proof state before:
m : Type ?u.1418
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
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
⊢ v = 0
Tactic:
have hv' := hv (star v)
Proof state after:
m : Type ?u.1418
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
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
hv' : v ⬝ᵥ M.mulVec (star v) = 0
⊢ v = 0
Theorem: Matrix.PosDef.det_ne_zero
Proof state before:
m : Type ?u.1418
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
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
hv' : v ⬝ᵥ M.mulVec (star v) = 0
⊢ v = 0
Tactic:
rw [← star_eq_zero]
Proof state after:
m : Type ?u.1418
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
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
hv' : v ⬝ᵥ M.mulVec (star v) = 0
⊢ star v = 0
Theorem: Matrix.PosDef.det_ne_zero
Proof state before:
m : Type ?u.1418
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
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
hv' : v ⬝ᵥ M.mulVec (star v) = 0
⊢ star v = 0
Tactic:
by_contra h
Proof state after:
m : Type ?u.1418
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
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
hv' : v ⬝ᵥ M.mulVec (star v) = 0
h : ¬star v = 0
⊢ False
Theorem: Matrix.PosDef.det_ne_zero
Proof state before:
m : Type ?u.1418
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
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
hv' : v ⬝ᵥ M.mulVec (star v) = 0
h : ¬star v = 0
⊢ False
Tactic:
have := hM.2 (star v) h
Proof state after:
m : Type ?u.1418
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
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
hv' : v ⬝ᵥ M.mulVec (star v) = 0
h : ¬star v = 0
this : 0 < star (star v) ⬝ᵥ M.mulVec (star v)
⊢ False
Theorem: Matrix.PosDef.det_ne_zero
Proof state before:
m : Type ?u.1418
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
v : n → 𝕜
hv : ∀ (w : n → 𝕜), v ⬝ᵥ M.mulVec w = 0
hv' : v ⬝ᵥ M.mulVec (star v) = 0
h : ¬star v = 0
this : 0 < star (star v) ⬝ᵥ M.mulVec (star v)
⊢ False
Tactic:
simp [star_star, hv'] at this
Proof state after:
no goals
Theorem: Matrix.PosSemidef_diagonal
Proof 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 _, _⟩
Proof 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
Theorem: Matrix.PosSemidef_diagonal
Proof 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
Proof 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
Theorem: Matrix.PosSemidef_diagonal
Proof 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]
Proof 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
Theorem: Matrix.PosSemidef_diagonal
Proof 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'
Proof 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
Theorem: Matrix.PosSemidef_diagonal
Proof 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
Proof 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
Theorem: Matrix.PosSemidef_diagonal
Proof 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]
Proof 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)
Theorem: Matrix.PosSemidef_diagonal
Proof 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))
Proof state after:
no goals
Theorem: Matrix.PosDef_diagonal
Proof 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 _, _⟩
Proof 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
Theorem: Matrix.PosDef_diagonal
Proof 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
Proof 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
Theorem: Matrix.PosDef_diagonal
Proof 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]
Proof 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
Theorem: Matrix.PosDef_diagonal
Proof 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'
Proof 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
Theorem: Matrix.PosDef_diagonal
Proof 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)) }
Proof 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
Theorem: Matrix.PosDef_diagonal
Proof 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 }
Proof state after:
no goals
Theorem: Matrix.PosDef_diagonal
Proof 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 _
Proof 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
Theorem: Matrix.PosDef_diagonal
Proof 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]
Proof 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)
Theorem: Matrix.PosDef_diagonal
Proof 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))
Proof state after:
no goals
Theorem: Matrix.PosDef_diagonal
Proof 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
Proof 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
Theorem: Matrix.PosDef_diagonal
Proof 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 ⊢
Proof 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
Theorem: Matrix.PosDef_diagonal
Proof 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
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
⊢ 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
⊢ x i = 0 i
Tactic:
have := hx 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 : x i * (diagonal f).mulVec x i ≤ 0
⊢ x i = 0 i