[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
⊢ (∀ (i j : n), star (A j i) = A i j) → IsHermitian A
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
⊢ IsHermitian A
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
i j : n
⊢ Aᴴ i j = A i j
[PROOFSTEP]
exact h i j
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : IsHermitian A
⊢ IsHermitian Aᵀ
[PROOFSTEP]
rw [IsHermitian, conjTranspose, transpose_map]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : IsHermitian A
⊢ (Matrix.map Aᵀ star)ᵀ = Aᵀ
[PROOFSTEP]
exact congr_arg Matrix.transpose h
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
⊢ IsHermitian Aᵀ → IsHermitian A
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : IsHermitian Aᵀ
⊢ IsHermitian A
[PROOFSTEP]
rw [← transpose_transpose A]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
h : IsHermitian Aᵀ
⊢ IsHermitian Aᵀᵀ
[PROOFSTEP]
exact IsHermitian.transpose h
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : Star α
inst✝ : Star β
A : Matrix n n α
e : m ≃ n
h : IsHermitian (submatrix A ↑e ↑e)
⊢ IsHermitian A
[PROOFSTEP]
simpa using h.submatrix e.symm
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsHermitian A
hBC : Bᴴ = C
hD : IsHermitian D
⊢ IsHermitian (Matrix.fromBlocks A B C D)
[PROOFSTEP]
have hCB : Cᴴ = B := by rw [← hBC, conjTranspose_conjTranspose]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsHermitian A
hBC : Bᴴ = C
hD : IsHermitian D
⊢ Cᴴ = B
[PROOFSTEP]
rw [← hBC, conjTranspose_conjTranspose]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsHermitian A
hBC : Bᴴ = C
hD : IsHermitian D
hCB : Cᴴ = B
⊢ IsHermitian (Matrix.fromBlocks A B C D)
[PROOFSTEP]
unfold Matrix.IsHermitian
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsHermitian A
hBC : Bᴴ = C
hD : IsHermitian D
hCB : Cᴴ = B
⊢ (Matrix.fromBlocks A B C D)ᴴ = Matrix.fromBlocks A B C D
[PROOFSTEP]
rw [fromBlocks_conjTranspose, hBC, hCB, hA, hD]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝⁴ : NonUnitalSemiring α
inst✝³ : StarRing α
inst✝² : NonUnitalSemiring β
inst✝¹ : StarRing β
inst✝ : Fintype n
A : Matrix m n α
⊢ IsHermitian (A * Aᴴ)
[PROOFSTEP]
rw [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝⁴ : NonUnitalSemiring α
inst✝³ : StarRing α
inst✝² : NonUnitalSemiring β
inst✝¹ : StarRing β
inst✝ : Fintype m
A : Matrix m n α
⊢ IsHermitian (Aᴴ * A)
[PROOFSTEP]
rw [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝⁴ : NonUnitalSemiring α
inst✝³ : StarRing α
inst✝² : NonUnitalSemiring β
inst✝¹ : StarRing β
inst✝ : Fintype m
A : Matrix m m α
B : Matrix m n α
hA : IsHermitian A
⊢ IsHermitian (Bᴴ * A * B)
[PROOFSTEP]
simp only [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose, hA.eq, Matrix.mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝⁴ : NonUnitalSemiring α
inst✝³ : StarRing α
inst✝² : NonUnitalSemiring β
inst✝¹ : StarRing β
inst✝ : Fintype m
A : Matrix m m α
B : Matrix n m α
hA : IsHermitian A
⊢ IsHermitian (B * A * Bᴴ)
[PROOFSTEP]
simp only [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose, hA.eq, Matrix.mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
hA : IsHermitian A
⊢ IsHermitian A⁻¹
[PROOFSTEP]
simp [IsHermitian, conjTranspose_nonsing_inv, hA.eq]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝⁴ : CommRing α
inst✝³ : StarRing α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
inst✝ : Invertible A
h : IsHermitian A⁻¹
⊢ IsHermitian A
[PROOFSTEP]
rw [← inv_inv_of_invertible A]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝⁴ : CommRing α
inst✝³ : StarRing α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
inst✝ : Invertible A
h : IsHermitian A⁻¹
⊢ IsHermitian A⁻¹⁻¹
[PROOFSTEP]
exact IsHermitian.inv h
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
hA : IsHermitian A
⊢ IsHermitian (Matrix.adjugate A)
[PROOFSTEP]
simp [IsHermitian, adjugate_conjTranspose, hA.eq]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝¹ : IsROrC α
inst✝ : IsROrC β
A : Matrix n n α
h : IsHermitian A
i : n
⊢ ↑(↑re (A i i)) = A i i
[PROOFSTEP]
rw [← conj_eq_iff_re, ← star_def, ← conjTranspose_apply, h.eq]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ IsHermitian A ↔ LinearMap.IsSymmetric (↑toEuclideanLin A)
[PROOFSTEP]
rw [LinearMap.IsSymmetric, (PiLp.equiv 2 fun _ : n => α).symm.surjective.forall₂]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ IsHermitian A ↔
    ∀ (x₁ x₂ : n → α),
      inner (↑(↑toEuclideanLin A) (↑(PiLp.equiv 2 fun x => α).symm x₁)) (↑(PiLp.equiv 2 fun x => α).symm x₂) =
        inner (↑(PiLp.equiv 2 fun x => α).symm x₁) (↑(↑toEuclideanLin A) (↑(PiLp.equiv 2 fun x => α).symm x₂))
[PROOFSTEP]
simp only [toEuclideanLin_piLp_equiv_symm, EuclideanSpace.inner_piLp_equiv_symm, toLin'_apply, star_mulVec,
  dotProduct_mulVec]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ IsHermitian A ↔ ∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ IsHermitian A → ∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂
[PROOFSTEP]
rintro (h : Aᴴ = A) x y
[GOAL]
case mp
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : Aᴴ = A
x y : n → α
⊢ vecMul (star x) Aᴴ ⬝ᵥ y = vecMul (star x) A ⬝ᵥ y
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ (∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂) → IsHermitian A
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : ∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂
⊢ IsHermitian A
[PROOFSTEP]
ext i j
[GOAL]
case mpr.a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : ∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂
i j : n
⊢ Aᴴ i j = A i j
[PROOFSTEP]
simpa only [(Pi.single_star i 1).symm, ← star_mulVec, mul_one, dotProduct_single, single_vecMul, star_one,
  one_mul] using h (Pi.single i 1) (Pi.single j 1)
