internlm/Lean-Github huggingface dataset:
Theorem: repr_gramSchmidt_diagonal
Proof state before:
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : IsWellOrder ι fun x x_1 => x < x_1
i : ι
b : Basis ι 𝕜 E
j : ι
hj : j < i
⊢ (b.repr ↑((orthogonalProjection (Submodule.span 𝕜 {gramSchmidt 𝕜 (⇑b) j})) (b i))) i = 0
Tactic:
simp [orthogonalProjection_singleton, gramSchmidt_triangular hj]
Proof state after:
no goals
Theorem: CvxLean.norm2₂_eq_norm2
Proof state before:
x y : ℝ
⊢ ‖![x, y]‖ = (x ^ 2 + y ^ 2).sqrt
Tactic:
simp [Norm.norm, sqrt_eq_rpow]
Proof state after:
no goals
Theorem: Finset.one_add_prod_le_prod_one_add
Proof state before:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ 1 + ∏ i : n, f i ≤ ∏ i : n, (1 + f i)
Tactic:
classical
calc 1 + (∏ i, f i)
  = (∏ _a : n, 1 : ℝ) * ∏ a : n in univ \ univ, f a
    + (∏ a : n in ∅, 1) * ∏ a : n in univ \ ∅, f a := by
  { simp }
_ = ∑ x in {univ, ∅}, (∏ _a : n in x, 1 : ℝ) * ∏ a : n in univ \ x, f a := by
  { rw [Finset.sum_pair]; simp; exact Finset.univ_nonempty.ne_empty }
_ ≤ ∑ t : Finset n, (∏ _a : n in t, 1 : ℝ) * ∏ a : n in univ \ t, f a := by
  { convert @Finset.sum_le_univ_sum_of_nonneg (Finset n) ℝ _ _ _ _ _
    simp [hf, prod_nonneg] }
_ = ∏ i, (1 + f i) := by
  { rw [prod_add, powerset_univ] }
Proof state after:
no goals
Theorem: Finset.one_add_prod_le_prod_one_add
Proof state before:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ 1 + ∏ i : n, f i ≤ ∏ i : n, (1 + f i)
Tactic:
calc 1 + (∏ i, f i)
  = (∏ _a : n, 1 : ℝ) * ∏ a : n in univ \ univ, f a
    + (∏ a : n in ∅, 1) * ∏ a : n in univ \ ∅, f a := by
  { simp }
_ = ∑ x in {univ, ∅}, (∏ _a : n in x, 1 : ℝ) * ∏ a : n in univ \ x, f a := by
  { rw [Finset.sum_pair]; simp; exact Finset.univ_nonempty.ne_empty }
_ ≤ ∑ t : Finset n, (∏ _a : n in t, 1 : ℝ) * ∏ a : n in univ \ t, f a := by
  { convert @Finset.sum_le_univ_sum_of_nonneg (Finset n) ℝ _ _ _ _ _
    simp [hf, prod_nonneg] }
_ = ∏ i, (1 + f i) := by
  { rw [prod_add, powerset_univ] }
Proof state after:
no goals
Theorem: Finset.one_add_prod_le_prod_one_add
Proof state before:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ 1 + ∏ i : n, f i = (∏ _a : n, 1) * ∏ a ∈ univ \ univ, f a + (∏ a ∈ ∅, 1) * ∏ a ∈ univ \ ∅, f a
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.one_add_prod_le_prod_one_add
Proof state before:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ (∏ _a : n, 1) * ∏ a ∈ univ \ univ, f a + (∏ a ∈ ∅, 1) * ∏ a ∈ univ \ ∅, f a =
    ∑ x ∈ {univ, ∅}, (∏ _a ∈ x, 1) * ∏ a ∈ univ \ x, f a
Tactic:
rw [Finset.sum_pair]
Proof state after:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ univ ≠ ∅
Theorem: Finset.one_add_prod_le_prod_one_add
Proof state before:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ univ ≠ ∅
Tactic:
simp
Proof state after:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ ¬univ = ∅
Theorem: Finset.one_add_prod_le_prod_one_add
Proof state before:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ ¬univ = ∅
Tactic:
exact Finset.univ_nonempty.ne_empty
Proof state after:
no goals
Theorem: Finset.one_add_prod_le_prod_one_add
Proof state before:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ ∑ x ∈ {univ, ∅}, (∏ _a ∈ x, 1) * ∏ a ∈ univ \ x, f a ≤ ∑ t : Finset n, (∏ _a ∈ t, 1) * ∏ a ∈ univ \ t, f a
Tactic:
convert @Finset.sum_le_univ_sum_of_nonneg (Finset n) ℝ _ _ _ _ _
Proof state after:
case convert_3
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ ∀ (x : Finset n), 0 ≤ (∏ _a ∈ x, 1) * ∏ a ∈ univ \ x, f a
Theorem: Finset.one_add_prod_le_prod_one_add
Proof state before:
case convert_3
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ ∀ (x : Finset n), 0 ≤ (∏ _a ∈ x, 1) * ∏ a ∈ univ \ x, f a
Tactic:
simp [hf, prod_nonneg]
Proof state after:
no goals
Theorem: Finset.one_add_prod_le_prod_one_add
Proof state before:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : Nonempty n
f : n → ℝ
hf : ∀ (i : n), 0 ≤ f i
⊢ ∑ t : Finset n, (∏ _a ∈ t, 1) * ∏ a ∈ univ \ t, f a = ∏ i : n, (1 + f i)
Tactic:
rw [prod_add, powerset_univ]
Proof state after:
no goals
Theorem: Matrix.IsHermitian.eigenvectorMatrix_inv_mul
Proof state before:
n : Type u_1
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : LinearOrder n
inst✝² : LocallyFiniteOrderBot n
𝕜 : Type u_2
inst✝¹ : DecidableEq 𝕜
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.IsHermitian
⊢ hA.eigenvectorMatrixInv * hA.eigenvectorMatrix = 1
Tactic:
apply Basis.toMatrix_mul_toMatrix_flip
Proof state after:
no goals
Theorem: Matrix.IsHermitian.spectral_theorem''
Proof state before:
n : Type u_1
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : LinearOrder n
inst✝² : LocallyFiniteOrderBot n
𝕜 : Type u_2
inst✝¹ : DecidableEq 𝕜
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.IsHermitian
⊢ hA.eigenvectorMatrix * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * hA.eigenvectorMatrix.conjTranspose = A
Tactic:
rw [conjTranspose_eigenvectorMatrix, Matrix.mul_assoc, ← spectral_theorem,
  ← Matrix.mul_assoc, eigenvectorMatrix_mul_inv, Matrix.one_mul]
Proof state after:
no goals
Theorem: Matrix.PosSemidef.sqrt_mul_sqrt
Proof state before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosSemidef
⊢ ⋯.sqrt * ⋯.sqrt =
    ⋯.eigenvectorMatrix *
        ((diagonal fun i => (⋯.eigenvalues i).sqrt) * (⋯.eigenvectorMatrix.transpose * ⋯.eigenvectorMatrix) *
          diagonal fun i => (⋯.eigenvalues i).sqrt) *
      ⋯.eigenvectorMatrix.transpose
Tactic:
simp [IsHermitian.sqrt, Matrix.mul_assoc]
Proof state after:
no goals
Theorem: Matrix.PosSemidef.sqrt_mul_sqrt
Proof state before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosSemidef
⊢ ⋯.eigenvectorMatrix *
        ((diagonal fun i => (⋯.eigenvalues i).sqrt) * (⋯.eigenvectorMatrix.transpose * ⋯.eigenvectorMatrix) *
          diagonal fun i => (⋯.eigenvalues i).sqrt) *
      ⋯.eigenvectorMatrix.transpose =
    A
Tactic:
rw [← conjTranspose_eq_transpose, hA.1.conjTranspose_eigenvectorMatrix,
  hA.1.eigenvectorMatrix_inv_mul, Matrix.mul_one, diagonal_mul_diagonal,
  ← hA.1.conjTranspose_eigenvectorMatrix]
Proof state after:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosSemidef
⊢ (⋯.eigenvectorMatrix * diagonal fun i => (⋯.eigenvalues i).sqrt * (⋯.eigenvalues i).sqrt) *
      ⋯.eigenvectorMatrix.conjTranspose =
    A
Theorem: Matrix.PosSemidef.sqrt_mul_sqrt
Proof state before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosSemidef
⊢ (⋯.eigenvectorMatrix * diagonal fun i => (⋯.eigenvalues i).sqrt * (⋯.eigenvalues i).sqrt) *
      ⋯.eigenvectorMatrix.conjTranspose =
    A
Tactic:
convert hA.1.spectral_theorem''
Proof state after:
case h.e'_2.h.e'_5.h.e'_6.h.e'_5.h
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosSemidef
x✝ : n
⊢ (⋯.eigenvalues x✝).sqrt * (⋯.eigenvalues x✝).sqrt = (RCLike.ofReal ∘ ⋯.eigenvalues) x✝
Theorem: Matrix.PosSemidef.sqrt_mul_sqrt
Proof state before:
case h.e'_2.h.e'_5.h.e'_6.h.e'_5.h
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosSemidef
x✝ : n
⊢ (⋯.eigenvalues x✝).sqrt * (⋯.eigenvalues x✝).sqrt = (RCLike.ofReal ∘ ⋯.eigenvalues) x✝
Tactic:
rw [← Real.sqrt_mul (hA.eigenvalues_nonneg _), Real.sqrt_mul_self (hA.eigenvalues_nonneg _)]
Proof state after:
case h.e'_2.h.e'_5.h.e'_6.h.e'_5.h
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosSemidef
x✝ : n
⊢ ⋯.eigenvalues x✝ = (RCLike.ofReal ∘ ⋯.eigenvalues) x✝
Theorem: Matrix.PosSemidef.sqrt_mul_sqrt
Proof state before:
case h.e'_2.h.e'_5.h.e'_6.h.e'_5.h
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosSemidef
x✝ : n
⊢ ⋯.eigenvalues x✝ = (RCLike.ofReal ∘ ⋯.eigenvalues) x✝
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.IsHermitian.one_add
Proof state before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.IsHermitian
⊢ (1 + A).IsHermitian
Tactic:
dsimp [IsHermitian]
Proof state after:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.IsHermitian
⊢ (1 + A).conjTranspose = 1 + A
Theorem: Matrix.IsHermitian.one_add
Proof state before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.IsHermitian
⊢ (1 + A).conjTranspose = 1 + A
Tactic:
rw [IsHermitian.add _ hA]
Proof state after:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.IsHermitian
⊢ IsHermitian 1
Theorem: Matrix.IsHermitian.one_add
Proof state before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.IsHermitian
⊢ IsHermitian 1
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.PosDef.PosDef_sqrt
Proof state before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosDef
⊢ ⋯.sqrt.PosDef
Tactic:
unfold IsHermitian.sqrt
Proof state after:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosDef
⊢ ((⋯.eigenvectorMatrix * diagonal fun i => (⋯.eigenvalues i).sqrt) * ⋯.eigenvectorMatrix.transpose).PosDef
Theorem: Matrix.PosDef.PosDef_sqrt
Proof state before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosDef
⊢ ((⋯.eigenvectorMatrix * diagonal fun i => (⋯.eigenvalues i).sqrt) * ⋯.eigenvectorMatrix.transpose).PosDef
Tactic:
refine'
  PosDef.conjTranspose_mul_mul _ (hA.1.eigenvectorMatrixᵀ)
    (PosDef_diagonal (fun i => Real.sqrt_pos.2 (hA.eigenvalues_pos i))) _
Proof state after:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosDef
⊢ ⋯.eigenvectorMatrix.transpose.det ≠ 0
Theorem: Matrix.PosDef.PosDef_sqrt
Proof state before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosDef
⊢ ⋯.eigenvectorMatrix.transpose.det ≠ 0
Tactic:
rw [det_transpose]
Proof state after:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosDef
⊢ ⋯.eigenvectorMatrix.det ≠ 0
Theorem: Matrix.PosDef.PosDef_sqrt
Proof state before:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : LinearOrder n
inst✝ : LocallyFiniteOrderBot n
A : Matrix n n ℝ
hA : A.PosDef
⊢ ⋯.eigenvectorMatrix.det ≠ 0
Tactic:
apply det_ne_zero_of_right_inverse hA.1.eigenvectorMatrix_mul_inv
Proof state after:
no goals
Theorem: Matrix.PosSemidef.PosDef_iff_det_ne_zero
Proof 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, _⟩
Proof 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
Theorem: Matrix.PosSemidef.PosDef_iff_det_ne_zero
Proof 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
Proof 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
Theorem: Matrix.PosSemidef.PosDef_iff_det_ne_zero
Proof 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, _⟩
Proof 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
Theorem: Matrix.PosSemidef.PosDef_iff_det_ne_zero
Proof 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
Proof 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
Theorem: Matrix.PosSemidef.PosDef_iff_det_ne_zero
Proof 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)
Proof 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
Theorem: Matrix.PosSemidef.PosDef_iff_det_ne_zero
Proof 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]
Proof 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
Theorem: Matrix.PosSemidef.PosDef_iff_det_ne_zero
Proof 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]
Proof 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
Theorem: Matrix.PosSemidef.PosDef_iff_det_ne_zero
Proof 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
Proof 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
Theorem: Matrix.PosSemidef.PosDef_iff_det_ne_zero
Proof 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
Proof 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
Theorem: Matrix.PosSemidef.PosDef_iff_det_ne_zero
Proof 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]
Proof 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
Theorem: Matrix.PosSemidef.PosDef_iff_det_ne_zero
Proof 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
Proof 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
Theorem: Matrix.PosSemidef.PosDef_iff_det_ne_zero
Proof 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
Proof state after:
no goals
Theorem: Matrix.PosSemidef.PosDef_iff_det_ne_zero
Proof 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, _⟩
Proof 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
Theorem: Matrix.PosSemidef.PosDef_iff_det_ne_zero
Proof 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]
Proof state after:
no goals
Theorem: Matrix.det_add_det_le_det_add'
Proof state before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosDef
hB : B.PosSemidef
⊢ A.det + B.det ≤ (A + B).det
Tactic:
let sqrtA := hA.1.sqrt
Proof state after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosDef
hB : B.PosSemidef
sqrtA : Matrix n n ℝ := ⋯.sqrt
⊢ A.det + B.det ≤ (A + B).det
Theorem: Matrix.det_add_det_le_det_add'
Proof state before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosDef
hB : B.PosSemidef
sqrtA : Matrix n n ℝ := ⋯.sqrt
⊢ A.det + B.det ≤ (A + B).det
Tactic:
have isUnit_det_sqrtA :=
  isUnit_iff_ne_zero.2 hA.PosDef_sqrt.det_ne_zero
Proof state after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosDef
hB : B.PosSemidef
sqrtA : Matrix n n ℝ := ⋯.sqrt
isUnit_det_sqrtA : IsUnit ⋯.sqrt.det
⊢ A.det + B.det ≤ (A + B).det
Theorem: Matrix.det_add_det_le_det_add'
Proof state before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosDef
hB : B.PosSemidef
sqrtA : Matrix n n ℝ := ⋯.sqrt
isUnit_det_sqrtA : IsUnit ⋯.sqrt.det
⊢ A.det + B.det ≤ (A + B).det
Tactic:
have : IsUnit sqrtA :=
  (isUnit_iff_isUnit_det _).2 isUnit_det_sqrtA
Proof state after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosDef
hB : B.PosSemidef
sqrtA : Matrix n n ℝ := ⋯.sqrt
isUnit_det_sqrtA : IsUnit ⋯.sqrt.det
this : IsUnit sqrtA
⊢ A.det + B.det ≤ (A + B).det
Theorem: Matrix.det_add_det_le_det_add'
Proof state before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosDef
hB : B.PosSemidef
sqrtA : Matrix n n ℝ := ⋯.sqrt
isUnit_det_sqrtA : IsUnit ⋯.sqrt.det
this : IsUnit sqrtA
⊢ A.det + B.det ≤ (A + B).det
Tactic:
have IsHermitian_sqrtA : sqrtA⁻¹.IsHermitian := by
{ apply IsHermitian.nonsingular_inv (hA.posSemidef.PosSemidef_sqrt.1)
  exact isUnit_det_sqrtA }
Proof state after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosDef
hB : B.PosSemidef
sqrtA : Matrix n n ℝ := ⋯.sqrt
isUnit_det_sqrtA : IsUnit ⋯.sqrt.det
this : IsUnit sqrtA
IsHermitian_sqrtA : sqrtA⁻¹.IsHermitian
⊢ A.det + B.det ≤ (A + B).det
Theorem: Matrix.det_add_det_le_det_add'
Proof state before:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosDef
hB : B.PosSemidef
sqrtA : Matrix n n ℝ := ⋯.sqrt
isUnit_det_sqrtA : IsUnit ⋯.sqrt.det
this : IsUnit sqrtA
IsHermitian_sqrtA : sqrtA⁻¹.IsHermitian
⊢ A.det + B.det ≤ (A + B).det
Tactic:
have PosSemidef_ABA : (sqrtA⁻¹ * B * sqrtA⁻¹).PosSemidef :=
  PosSemidef.mul_mul_of_IsHermitian hB IsHermitian_sqrtA
Proof state after:
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : LinearOrder n
inst✝¹ : LocallyFiniteOrderBot n
inst✝ : Nonempty n
A B : Matrix n n ℝ
hA : A.PosDef
hB : B.PosSemidef
sqrtA : Matrix n n ℝ := ⋯.sqrt
isUnit_det_sqrtA : IsUnit ⋯.sqrt.det
this : IsUnit sqrtA
IsHermitian_sqrtA : sqrtA⁻¹.IsHermitian
PosSemidef_ABA : (sqrtA⁻¹ * B * sqrtA⁻¹).PosSemidef
⊢ A.det + B.det ≤ (A + B).det