Theorem: Matrix.det_add_det_le_det_add' (CvxLean/Lib/Math/Subadditivity.lean)

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
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

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
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

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
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

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 }
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

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
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

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
PosSemidef_ABA : (sqrtA⁻¹ * B * sqrtA⁻¹).PosSemidef
⊢ A.det + B.det ≤ (A + B).det
Tactic:
let μ := PosSemidef_ABA.1.eigenvalues
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
μ : n → ℝ := ⋯.eigenvalues
⊢ A.det + B.det ≤ (A + B).det

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
PosSemidef_ABA : (sqrtA⁻¹ * B * sqrtA⁻¹).PosSemidef
μ : n → ℝ := ⋯.eigenvalues
⊢ A.det + B.det ≤ (A + B).det
Tactic:
calc A.det + B.det
  = A.det * (1 + (sqrtA⁻¹ * B * sqrtA⁻¹).det) := by
      rw [det_mul, det_mul, mul_comm _ B.det, mul_assoc, ← det_mul, ← Matrix.mul_inv_rev,
        hA.posSemidef.sqrt_mul_sqrt, mul_add, mul_one, mul_comm, mul_assoc, ← det_mul,
        nonsing_inv_mul _ (isUnit_iff_ne_zero.2 hA.det_ne_zero), det_one, mul_one]
_ = A.det * (1 + ∏ i, μ i) := by
      rw [PosSemidef_ABA.1.det_eq_prod_eigenvalues]
      rfl
_ ≤ A.det * ∏ i, (1 + μ i) := by
      apply (mul_le_mul_left hA.det_pos).2
      apply Finset.one_add_prod_le_prod_one_add μ PosSemidef_ABA.eigenvalues_nonneg
_ = A.det * (1 + sqrtA⁻¹ * B * sqrtA⁻¹).det := by
      rw [mul_eq_mul_left_iff]; left; symm
      rw [det_eq_prod_eigenvalues PosSemidef_ABA.1.eigenvectorBasis
        (fun i => 1 + (PosSemidef_ABA.1.eigenvalues i)) _]
      { simp }
      intro i
      convert PosSemidef_ABA.1.has_eigenvector_one_add i using 1
      simp only [map_add, toLin'_one, toLin'_mul, add_left_inj]
      rfl
_ = (A + B).det := by
      rw [← det_mul, ← det_conj this (A + B)]
      apply congr_arg
      rw [← hA.posSemidef.sqrt_mul_sqrt]
      change sqrtA * sqrtA * (1 + sqrtA⁻¹ * B * sqrtA⁻¹) = sqrtA * (sqrtA * sqrtA + B) * sqrtA⁻¹
      rw [Matrix.mul_add, Matrix.mul_one, Matrix.mul_add, Matrix.add_mul,
        Matrix.mul_assoc, Matrix.mul_assoc, Matrix.mul_assoc, Matrix.mul_assoc,
        ← Matrix.mul_assoc _ _ (B * _),
        Matrix.mul_nonsing_inv _ isUnit_det_sqrtA, Matrix.one_mul, Matrix.mul_one,
        hA.posSemidef.sqrt_mul_sqrt, Matrix.mul_assoc]
State after:
no goals

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
⊢ sqrtA⁻¹.IsHermitian
Tactic:
apply IsHermitian.nonsingular_inv (hA.posSemidef.PosSemidef_sqrt.1)
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
⊢ IsUnit ⋯.sqrt.det

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
⊢ IsUnit ⋯.sqrt.det
Tactic:
exact isUnit_det_sqrtA
State after:
no goals

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
PosSemidef_ABA : (sqrtA⁻¹ * B * sqrtA⁻¹).PosSemidef
μ : n → ℝ := ⋯.eigenvalues
⊢ A.det + B.det = A.det * (1 + (sqrtA⁻¹ * B * sqrtA⁻¹).det)
Tactic:
rw [det_mul, det_mul, mul_comm _ B.det, mul_assoc, ← det_mul, ← Matrix.mul_inv_rev,
  hA.posSemidef.sqrt_mul_sqrt, mul_add, mul_one, mul_comm, mul_assoc, ← det_mul,
  nonsing_inv_mul _ (isUnit_iff_ne_zero.2 hA.det_ne_zero), det_one, mul_one]
State after:
no goals

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
PosSemidef_ABA : (sqrtA⁻¹ * B * sqrtA⁻¹).PosSemidef
μ : n → ℝ := ⋯.eigenvalues
⊢ A.det * (1 + (sqrtA⁻¹ * B * sqrtA⁻¹).det) = A.det * (1 + ∏ i : n, μ i)
Tactic:
rw [PosSemidef_ABA.1.det_eq_prod_eigenvalues]
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
μ : n → ℝ := ⋯.eigenvalues
⊢ A.det * (1 + ∏ i : n, ↑(⋯.eigenvalues i)) = A.det * (1 + ∏ i : n, μ i)

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
PosSemidef_ABA : (sqrtA⁻¹ * B * sqrtA⁻¹).PosSemidef
μ : n → ℝ := ⋯.eigenvalues
⊢ A.det * (1 + ∏ i : n, ↑(⋯.eigenvalues i)) = A.det * (1 + ∏ i : n, μ i)
Tactic:
rfl
State after:
no goals

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
PosSemidef_ABA : (sqrtA⁻¹ * B * sqrtA⁻¹).PosSemidef
μ : n → ℝ := ⋯.eigenvalues
⊢ A.det * (1 + ∏ i : n, μ i) ≤ A.det * ∏ i : n, (1 + μ i)
Tactic:
apply (mul_le_mul_left hA.det_pos).2
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
μ : n → ℝ := ⋯.eigenvalues
⊢ 1 + ∏ i : n, μ i ≤ ∏ i : n, (1 + μ i)

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
PosSemidef_ABA : (sqrtA⁻¹ * B * sqrtA⁻¹).PosSemidef
μ : n → ℝ := ⋯.eigenvalues
⊢ 1 + ∏ i : n, μ i ≤ ∏ i : n, (1 + μ i)
Tactic:
apply Finset.one_add_prod_le_prod_one_add μ PosSemidef_ABA.eigenvalues_nonneg
State after:
no goals

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
PosSemidef_ABA : (sqrtA⁻¹ * B * sqrtA⁻¹).PosSemidef
μ : n → ℝ := ⋯.eigenvalues
⊢ A.det * ∏ i : n, (1 + μ i) = A.det * (1 + sqrtA⁻¹ * B * sqrtA⁻¹).det
Tactic:
rw [mul_eq_mul_left_iff]
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
μ : n → ℝ := ⋯.eigenvalues
⊢ ∏ i : n, (1 + μ i) = (1 + sqrtA⁻¹ * B * sqrtA⁻¹).det ∨ A.det = 0

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
PosSemidef_ABA : (sqrtA⁻¹ * B * sqrtA⁻¹).PosSemidef
μ : n → ℝ := ⋯.eigenvalues
⊢ ∏ i : n, (1 + μ i) = (1 + sqrtA⁻¹ * B * sqrtA⁻¹).det ∨ A.det = 0
Tactic:
left
State after:
case h
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
μ : n → ℝ := ⋯.eigenvalues
⊢ ∏ i : n, (1 + μ i) = (1 + sqrtA⁻¹ * B * sqrtA⁻¹).det

State before:
case h
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
μ : n → ℝ := ⋯.eigenvalues
⊢ ∏ i : n, (1 + μ i) = (1 + sqrtA⁻¹ * B * sqrtA⁻¹).det
Tactic:
symm
State after:
case h
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
μ : n → ℝ := ⋯.eigenvalues
⊢ (1 + sqrtA⁻¹ * B * sqrtA⁻¹).det = ∏ i : n, (1 + μ i)

State before:
case h
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
μ : n → ℝ := ⋯.eigenvalues
⊢ (1 + sqrtA⁻¹ * B * sqrtA⁻¹).det = ∏ i : n, (1 + μ i)
Tactic:
rw [det_eq_prod_eigenvalues PosSemidef_ABA.1.eigenvectorBasis
  (fun i => 1 + (PosSemidef_ABA.1.eigenvalues i)) _]
State after:
case h
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
μ : n → ℝ := ⋯.eigenvalues
⊢ ↑(∏ i : n, (1 + ⋯.eigenvalues i)) = ∏ i : n, (1 + μ i)

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
μ : n → ℝ := ⋯.eigenvalues
⊢ ∀ (j : n),
    Module.End.HasEigenvector (toLin' (1 + sqrtA⁻¹ * B * sqrtA⁻¹)) (↑((fun i => 1 + ⋯.eigenvalues i) j))
      (⋯.eigenvectorBasis j)

State before:
case h
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
μ : n → ℝ := ⋯.eigenvalues
⊢ ↑(∏ i : n, (1 + ⋯.eigenvalues i)) = ∏ i : n, (1 + μ i)

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
μ : n → ℝ := ⋯.eigenvalues
⊢ ∀ (j : n),
    Module.End.HasEigenvector (toLin' (1 + sqrtA⁻¹ * B * sqrtA⁻¹)) (↑((fun i => 1 + ⋯.eigenvalues i) j))
      (⋯.eigenvectorBasis j)
Tactic:
{ simp }
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
μ : n → ℝ := ⋯.eigenvalues
⊢ ∀ (j : n),
    Module.End.HasEigenvector (toLin' (1 + sqrtA⁻¹ * B * sqrtA⁻¹)) (↑((fun i => 1 + ⋯.eigenvalues i) j))
      (⋯.eigenvectorBasis j)

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
PosSemidef_ABA : (sqrtA⁻¹ * B * sqrtA⁻¹).PosSemidef
μ : n → ℝ := ⋯.eigenvalues
⊢ ∀ (j : n),
    Module.End.HasEigenvector (toLin' (1 + sqrtA⁻¹ * B * sqrtA⁻¹)) (↑((fun i => 1 + ⋯.eigenvalues i) j))
      (⋯.eigenvectorBasis j)
Tactic:
intro i
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
μ : n → ℝ := ⋯.eigenvalues
i : n
⊢ Module.End.HasEigenvector (toLin' (1 + sqrtA⁻¹ * B * sqrtA⁻¹)) (↑((fun i => 1 + ⋯.eigenvalues i) i))
    (⋯.eigenvectorBasis i)

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
PosSemidef_ABA : (sqrtA⁻¹ * B * sqrtA⁻¹).PosSemidef
μ : n → ℝ := ⋯.eigenvalues
i : n
⊢ Module.End.HasEigenvector (toLin' (1 + sqrtA⁻¹ * B * sqrtA⁻¹)) (↑((fun i => 1 + ⋯.eigenvalues i) i))
    (⋯.eigenvectorBasis i)
Tactic:
convert PosSemidef_ABA.1.has_eigenvector_one_add i using 1
State after:
case h.e'_6.h.h.h
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
μ : n → ℝ := ⋯.eigenvalues
i : n
e_2✝ : (n → ℝ) = EuclideanSpace ℝ n
e_3✝ : EuclideanDomain.toCommRing = Real.commRing
he✝¹ : Pi.addCommGroup = WithLp.instAddCommGroup 2 ((i : n) → (fun x => ℝ) i)
he✝ : Pi.Function.module n ℝ ℝ = WithLp.instModule 2 ℝ ((i : n) → (fun x => ℝ) i)
⊢ toLin' (1 + sqrtA⁻¹ * B * sqrtA⁻¹) = 1 + toLin' (sqrtA⁻¹ * B * sqrtA⁻¹)

State before:
case h.e'_6.h.h.h
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
μ : n → ℝ := ⋯.eigenvalues
i : n
e_2✝ : (n → ℝ) = EuclideanSpace ℝ n
e_3✝ : EuclideanDomain.toCommRing = Real.commRing
he✝¹ : Pi.addCommGroup = WithLp.instAddCommGroup 2 ((i : n) → (fun x => ℝ) i)
he✝ : Pi.Function.module n ℝ ℝ = WithLp.instModule 2 ℝ ((i : n) → (fun x => ℝ) i)
⊢ toLin' (1 + sqrtA⁻¹ * B * sqrtA⁻¹) = 1 + toLin' (sqrtA⁻¹ * B * sqrtA⁻¹)
Tactic:
simp only [map_add, toLin'_one, toLin'_mul, add_left_inj]
State after:
case h.e'_6.h.h.h
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
μ : n → ℝ := ⋯.eigenvalues
i : n
e_2✝ : (n → ℝ) = EuclideanSpace ℝ n
e_3✝ : EuclideanDomain.toCommRing = Real.commRing
he✝¹ : Pi.addCommGroup = WithLp.instAddCommGroup 2 ((i : n) → (fun x => ℝ) i)
he✝ : Pi.Function.module n ℝ ℝ = WithLp.instModule 2 ℝ ((i : n) → (fun x => ℝ) i)
⊢ LinearMap.id = 1

State before:
case h.e'_6.h.h.h
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
μ : n → ℝ := ⋯.eigenvalues
i : n
e_2✝ : (n → ℝ) = EuclideanSpace ℝ n
e_3✝ : EuclideanDomain.toCommRing = Real.commRing
he✝¹ : Pi.addCommGroup = WithLp.instAddCommGroup 2 ((i : n) → (fun x => ℝ) i)
he✝ : Pi.Function.module n ℝ ℝ = WithLp.instModule 2 ℝ ((i : n) → (fun x => ℝ) i)
⊢ LinearMap.id = 1
Tactic:
rfl
State after:
no goals

State before:
case h
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
μ : n → ℝ := ⋯.eigenvalues
⊢ ↑(∏ i : n, (1 + ⋯.eigenvalues i)) = ∏ i : n, (1 + μ i)
Tactic:
simp
State after:
no goals

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
PosSemidef_ABA : (sqrtA⁻¹ * B * sqrtA⁻¹).PosSemidef
μ : n → ℝ := ⋯.eigenvalues
⊢ A.det * (1 + sqrtA⁻¹ * B * sqrtA⁻¹).det = (A + B).det
Tactic:
rw [← det_mul, ← det_conj this (A + B)]
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
μ : n → ℝ := ⋯.eigenvalues
⊢ (A * (1 + sqrtA⁻¹ * B * sqrtA⁻¹)).det = (sqrtA * (A + B) * sqrtA⁻¹).det

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
PosSemidef_ABA : (sqrtA⁻¹ * B * sqrtA⁻¹).PosSemidef
μ : n → ℝ := ⋯.eigenvalues
⊢ (A * (1 + sqrtA⁻¹ * B * sqrtA⁻¹)).det = (sqrtA * (A + B) * sqrtA⁻¹).det
Tactic:
apply congr_arg
State after:
case h
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
μ : n → ℝ := ⋯.eigenvalues
⊢ A * (1 + sqrtA⁻¹ * B * sqrtA⁻¹) = sqrtA * (A + B) * sqrtA⁻¹

State before:
case h
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
μ : n → ℝ := ⋯.eigenvalues
⊢ A * (1 + sqrtA⁻¹ * B * sqrtA⁻¹) = sqrtA * (A + B) * sqrtA⁻¹
Tactic:
rw [← hA.posSemidef.sqrt_mul_sqrt]
State after:
case h
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
μ : n → ℝ := ⋯.eigenvalues
⊢ ⋯.sqrt * ⋯.sqrt * (1 + sqrtA⁻¹ * B * sqrtA⁻¹) = sqrtA * (⋯.sqrt * ⋯.sqrt + B) * sqrtA⁻¹

State before:
case h
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
μ : n → ℝ := ⋯.eigenvalues
⊢ ⋯.sqrt * ⋯.sqrt * (1 + sqrtA⁻¹ * B * sqrtA⁻¹) = sqrtA * (⋯.sqrt * ⋯.sqrt + B) * sqrtA⁻¹
Tactic:
change sqrtA * sqrtA * (1 + sqrtA⁻¹ * B * sqrtA⁻¹) = sqrtA * (sqrtA * sqrtA + B) * sqrtA⁻¹
State after:
case h
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
μ : n → ℝ := ⋯.eigenvalues
⊢ sqrtA * sqrtA * (1 + sqrtA⁻¹ * B * sqrtA⁻¹) = sqrtA * (sqrtA * sqrtA + B) * sqrtA⁻¹

State before:
case h
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
μ : n → ℝ := ⋯.eigenvalues
⊢ sqrtA * sqrtA * (1 + sqrtA⁻¹ * B * sqrtA⁻¹) = sqrtA * (sqrtA * sqrtA + B) * sqrtA⁻¹
Tactic:
rw [Matrix.mul_add, Matrix.mul_one, Matrix.mul_add, Matrix.add_mul,
  Matrix.mul_assoc, Matrix.mul_assoc, Matrix.mul_assoc, Matrix.mul_assoc,
  ← Matrix.mul_assoc _ _ (B * _),
  Matrix.mul_nonsing_inv _ isUnit_det_sqrtA, Matrix.one_mul, Matrix.mul_one,
  hA.posSemidef.sqrt_mul_sqrt, Matrix.mul_assoc]
State after:
no goals