Theorem: Matrix.PosSemiDef.IsSymm (CvxLean/Lib/Math/LinearAlgebra/Matrix/PosDef.lean)

State before:
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
⊢ A.IsSymm
Tactic:
let h_A_IsHermitian := hA.1
State after:
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian : A.IsHermitian := hA.left
⊢ A.IsSymm

State before:
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian : A.IsHermitian := hA.left
⊢ A.IsSymm
Tactic:
rw [Matrix.isHermitian_iff_isSymmetric] at h_A_IsHermitian
State after:
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian : (toEuclideanLin A).IsSymmetric
⊢ A.IsSymm

State before:
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian : (toEuclideanLin A).IsSymmetric
⊢ A.IsSymm
Tactic:
simp [LinearMap.IsSymmetric, toEuclideanLin] at h_A_IsHermitian
State after:
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian :
  ∀ (x y : EuclideanSpace ℝ (Fin n)),
    (Finset.univ.sum fun x_1 => A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) x) x_1 * y x_1) =
      Finset.univ.sum fun x_1 => x x_1 * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) y) x_1
⊢ A.IsSymm

State before:
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian :
  ∀ (x y : EuclideanSpace ℝ (Fin n)),
    (Finset.univ.sum fun x_1 => A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) x) x_1 * y x_1) =
      Finset.univ.sum fun x_1 => x x_1 * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) y) x_1
⊢ A.IsSymm
Tactic:
apply IsSymm.ext
State after:
case a
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian :
  ∀ (x y : EuclideanSpace ℝ (Fin n)),
    (Finset.univ.sum fun x_1 => A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) x) x_1 * y x_1) =
      Finset.univ.sum fun x_1 => x x_1 * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) y) x_1
⊢ ∀ (i j : Fin n), A j i = A i j

State before:
case a
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian :
  ∀ (x y : EuclideanSpace ℝ (Fin n)),
    (Finset.univ.sum fun x_1 => A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) x) x_1 * y x_1) =
      Finset.univ.sum fun x_1 => x x_1 * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) y) x_1
⊢ ∀ (i j : Fin n), A j i = A i j
Tactic:
intros i j
State after:
case a
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian :
  ∀ (x y : EuclideanSpace ℝ (Fin n)),
    (Finset.univ.sum fun x_1 => A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) x) x_1 * y x_1) =
      Finset.univ.sum fun x_1 => x x_1 * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) y) x_1
i j : Fin n
⊢ A j i = A i j

State before:
case a
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian :
  ∀ (x y : EuclideanSpace ℝ (Fin n)),
    (Finset.univ.sum fun x_1 => A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) x) x_1 * y x_1) =
      Finset.univ.sum fun x_1 => x x_1 * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) y) x_1
i j : Fin n
⊢ A j i = A i j
Tactic:
have hAij := h_A_IsHermitian (fun k => if k = i then 1 else 0) (fun k => if k = j then 1 else 0)
State after:
case a
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian :
  ∀ (x y : EuclideanSpace ℝ (Fin n)),
    (Finset.univ.sum fun x_1 => A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) x) x_1 * y x_1) =
      Finset.univ.sum fun x_1 => x x_1 * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) y) x_1
i j : Fin n
hAij :
  (Finset.univ.sum fun x =>
      A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) fun k => if k = i then 1 else 0) x * if x = j then 1 else 0) =
    Finset.univ.sum fun x =>
      (if x = i then 1 else 0) * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) fun k => if k = j then 1 else 0) x
⊢ A j i = A i j

State before:
case a
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian :
  ∀ (x y : EuclideanSpace ℝ (Fin n)),
    (Finset.univ.sum fun x_1 => A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) x) x_1 * y x_1) =
      Finset.univ.sum fun x_1 => x x_1 * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) y) x_1
i j : Fin n
hAij :
  (Finset.univ.sum fun x =>
      A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) fun k => if k = i then 1 else 0) x * if x = j then 1 else 0) =
    Finset.univ.sum fun x =>
      (if x = i then 1 else 0) * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) fun k => if k = j then 1 else 0) x
⊢ A j i = A i j
Tactic:
have hi : (Finset.sum Finset.univ fun x => A j x * (Equiv.refl (WithLp 2 (Fin n → ℝ)))
  (fun k => if k = i then 1 else 0) x) = A j i := by simp
State after:
case a
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian :
  ∀ (x y : EuclideanSpace ℝ (Fin n)),
    (Finset.univ.sum fun x_1 => A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) x) x_1 * y x_1) =
      Finset.univ.sum fun x_1 => x x_1 * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) y) x_1
i j : Fin n
hAij :
  (Finset.univ.sum fun x =>
      A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) fun k => if k = i then 1 else 0) x * if x = j then 1 else 0) =
    Finset.univ.sum fun x =>
      (if x = i then 1 else 0) * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) fun k => if k = j then 1 else 0) x
hi : (Finset.univ.sum fun x => A j x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = i then 1 else 0) x) = A j i
⊢ A j i = A i j

State before:
case a
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian :
  ∀ (x y : EuclideanSpace ℝ (Fin n)),
    (Finset.univ.sum fun x_1 => A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) x) x_1 * y x_1) =
      Finset.univ.sum fun x_1 => x x_1 * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) y) x_1
i j : Fin n
hAij :
  (Finset.univ.sum fun x =>
      A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) fun k => if k = i then 1 else 0) x * if x = j then 1 else 0) =
    Finset.univ.sum fun x =>
      (if x = i then 1 else 0) * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) fun k => if k = j then 1 else 0) x
hi : (Finset.univ.sum fun x => A j x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = i then 1 else 0) x) = A j i
⊢ A j i = A i j
Tactic:
have hj : (Finset.sum Finset.univ fun x => A i x * (Equiv.refl (WithLp 2 (Fin n → ℝ)))
  (fun k => if k = j then 1 else 0) x) = A i j := by simp
State after:
case a
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian :
  ∀ (x y : EuclideanSpace ℝ (Fin n)),
    (Finset.univ.sum fun x_1 => A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) x) x_1 * y x_1) =
      Finset.univ.sum fun x_1 => x x_1 * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) y) x_1
i j : Fin n
hAij :
  (Finset.univ.sum fun x =>
      A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) fun k => if k = i then 1 else 0) x * if x = j then 1 else 0) =
    Finset.univ.sum fun x =>
      (if x = i then 1 else 0) * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) fun k => if k = j then 1 else 0) x
hi : (Finset.univ.sum fun x => A j x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = i then 1 else 0) x) = A j i
hj : (Finset.univ.sum fun x => A i x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = j then 1 else 0) x) = A i j
⊢ A j i = A i j

State before:
case a
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian :
  ∀ (x y : EuclideanSpace ℝ (Fin n)),
    (Finset.univ.sum fun x_1 => A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) x) x_1 * y x_1) =
      Finset.univ.sum fun x_1 => x x_1 * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) y) x_1
i j : Fin n
hAij :
  (Finset.univ.sum fun x =>
      A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) fun k => if k = i then 1 else 0) x * if x = j then 1 else 0) =
    Finset.univ.sum fun x =>
      (if x = i then 1 else 0) * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) fun k => if k = j then 1 else 0) x
hi : (Finset.univ.sum fun x => A j x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = i then 1 else 0) x) = A j i
hj : (Finset.univ.sum fun x => A i x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = j then 1 else 0) x) = A i j
⊢ A j i = A i j
Tactic:
simp [WithLp.equiv, mulVec, dotProduct] at hAij
State after:
case a
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian :
  ∀ (x y : EuclideanSpace ℝ (Fin n)),
    (Finset.univ.sum fun x_1 => A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) x) x_1 * y x_1) =
      Finset.univ.sum fun x_1 => x x_1 * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) y) x_1
i j : Fin n
hi : (Finset.univ.sum fun x => A j x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = i then 1 else 0) x) = A j i
hj : (Finset.univ.sum fun x => A i x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = j then 1 else 0) x) = A i j
hAij :
  (Finset.univ.sum fun x => A j x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = i then 1 else 0) x) =
    Finset.univ.sum fun x => A i x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = j then 1 else 0) x
⊢ A j i = A i j

State before:
case a
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian :
  ∀ (x y : EuclideanSpace ℝ (Fin n)),
    (Finset.univ.sum fun x_1 => A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) x) x_1 * y x_1) =
      Finset.univ.sum fun x_1 => x x_1 * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) y) x_1
i j : Fin n
hi : (Finset.univ.sum fun x => A j x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = i then 1 else 0) x) = A j i
hj : (Finset.univ.sum fun x => A i x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = j then 1 else 0) x) = A i j
hAij :
  (Finset.univ.sum fun x => A j x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = i then 1 else 0) x) =
    Finset.univ.sum fun x => A i x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = j then 1 else 0) x
⊢ A j i = A i j
Tactic:
erw [hi, hj] at hAij
State after:
case a
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian :
  ∀ (x y : EuclideanSpace ℝ (Fin n)),
    (Finset.univ.sum fun x_1 => A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) x) x_1 * y x_1) =
      Finset.univ.sum fun x_1 => x x_1 * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) y) x_1
i j : Fin n
hi : (Finset.univ.sum fun x => A j x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = i then 1 else 0) x) = A j i
hj : (Finset.univ.sum fun x => A i x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = j then 1 else 0) x) = A i j
hAij : A j i = A i j
⊢ A j i = A i j

State before:
case a
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian :
  ∀ (x y : EuclideanSpace ℝ (Fin n)),
    (Finset.univ.sum fun x_1 => A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) x) x_1 * y x_1) =
      Finset.univ.sum fun x_1 => x x_1 * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) y) x_1
i j : Fin n
hi : (Finset.univ.sum fun x => A j x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = i then 1 else 0) x) = A j i
hj : (Finset.univ.sum fun x => A i x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = j then 1 else 0) x) = A i j
hAij : A j i = A i j
⊢ A j i = A i j
Tactic:
rw [hAij]
State after:
no goals

State before:
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian :
  ∀ (x y : EuclideanSpace ℝ (Fin n)),
    (Finset.univ.sum fun x_1 => A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) x) x_1 * y x_1) =
      Finset.univ.sum fun x_1 => x x_1 * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) y) x_1
i j : Fin n
hAij :
  (Finset.univ.sum fun x =>
      A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) fun k => if k = i then 1 else 0) x * if x = j then 1 else 0) =
    Finset.univ.sum fun x =>
      (if x = i then 1 else 0) * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) fun k => if k = j then 1 else 0) x
⊢ (Finset.univ.sum fun x => A j x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = i then 1 else 0) x) = A j i
Tactic:
simp
State after:
no goals

State before:
m : Type ?u.51903
n✝ : Type ?u.51906
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n✝
𝕜 : Type ?u.51915
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : StarRing 𝕜
inst✝¹ : StarOrderedRing 𝕜
inst✝ : RCLike 𝕜
n : ℕ
A : Matrix (Fin n) (Fin n) ℝ
hA : A.PosSemidef
h_A_IsHermitian :
  ∀ (x y : EuclideanSpace ℝ (Fin n)),
    (Finset.univ.sum fun x_1 => A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) x) x_1 * y x_1) =
      Finset.univ.sum fun x_1 => x x_1 * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) y) x_1
i j : Fin n
hAij :
  (Finset.univ.sum fun x =>
      A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) fun k => if k = i then 1 else 0) x * if x = j then 1 else 0) =
    Finset.univ.sum fun x =>
      (if x = i then 1 else 0) * A.mulVec ((WithLp.equiv 2 (Fin n → ℝ)) fun k => if k = j then 1 else 0) x
hi : (Finset.univ.sum fun x => A j x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = i then 1 else 0) x) = A j i
⊢ (Finset.univ.sum fun x => A i x * (Equiv.refl (WithLp 2 (Fin n → ℝ))) (fun k => if k = j then 1 else 0) x) = A i j
Tactic:
simp
State after:
no goals