internlm/Lean-Github huggingface dataset:
Theorem: Matrix.PosDef_inv_iff_PosDef
Proof state before:
m : Type ?u.50670
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.50682
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
⊢ M⁻¹.PosDef ↔ M.PosDef
Tactic:
constructor
Proof state after:
case mp
m : Type ?u.50670
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.50682
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
⊢ M⁻¹.PosDef → M.PosDef

case mpr
m : Type ?u.50670
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.50682
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
⊢ M.PosDef → M⁻¹.PosDef
Theorem: Matrix.PosDef_inv_iff_PosDef
Proof state before:
case mp
m : Type ?u.50670
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.50682
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
⊢ M⁻¹.PosDef → M.PosDef

case mpr
m : Type ?u.50670
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.50682
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
⊢ M.PosDef → M⁻¹.PosDef
Tactic:
{ intros hM
  rw [← Matrix.nonsing_inv_nonsing_inv M (isUnit_det_of_PosDef_inv hM)]
  apply hM.nonsingular_inv }
Proof state after:
case mpr
m : Type ?u.50670
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.50682
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
⊢ M.PosDef → M⁻¹.PosDef
Theorem: Matrix.PosDef_inv_iff_PosDef
Proof state before:
case mpr
m : Type ?u.50670
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.50682
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
⊢ M.PosDef → M⁻¹.PosDef
Tactic:
{ intros hM
  exact hM.nonsingular_inv }
Proof state after:
no goals
Theorem: Matrix.PosDef_inv_iff_PosDef
Proof state before:
case mp
m : Type ?u.50670
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.50682
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
⊢ M⁻¹.PosDef → M.PosDef
Tactic:
intros hM
Proof state after:
case mp
m : Type ?u.50670
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.50682
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M⁻¹.PosDef
⊢ M.PosDef
Theorem: Matrix.PosDef_inv_iff_PosDef
Proof state before:
case mp
m : Type ?u.50670
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.50682
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M⁻¹.PosDef
⊢ M.PosDef
Tactic:
rw [← Matrix.nonsing_inv_nonsing_inv M (isUnit_det_of_PosDef_inv hM)]
Proof state after:
case mp
m : Type ?u.50670
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.50682
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M⁻¹.PosDef
⊢ M⁻¹⁻¹.PosDef
Theorem: Matrix.PosDef_inv_iff_PosDef
Proof state before:
case mp
m : Type ?u.50670
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.50682
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M⁻¹.PosDef
⊢ M⁻¹⁻¹.PosDef
Tactic:
apply hM.nonsingular_inv
Proof state after:
no goals
Theorem: Matrix.PosDef_inv_iff_PosDef
Proof state before:
case mpr
m : Type ?u.50670
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.50682
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
⊢ M.PosDef → M⁻¹.PosDef
Tactic:
intros hM
Proof state after:
case mpr
m : Type ?u.50670
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.50682
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosDef
⊢ M⁻¹.PosDef
Theorem: Matrix.PosDef_inv_iff_PosDef
Proof state before:
case mpr
m : Type ?u.50670
n : Type u_1
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
𝕜 : Type ?u.50682
inst✝⁵ : NormedField 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : StarRing 𝕜
inst✝² : StarOrderedRing 𝕜
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosDef
⊢ M⁻¹.PosDef
Tactic:
exact hM.nonsingular_inv
Proof state after:
no goals
Theorem: Matrix.PosSemiDef.IsSymm
Proof 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
Proof 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
Theorem: Matrix.PosSemiDef.IsSymm
Proof 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
Proof 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
Theorem: Matrix.PosSemiDef.IsSymm
Proof 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
Proof 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
Theorem: Matrix.PosSemiDef.IsSymm
Proof 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
Proof 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
Theorem: Matrix.PosSemiDef.IsSymm
Proof 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
Proof 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
Theorem: Matrix.PosSemiDef.IsSymm
Proof 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)
Proof 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
Theorem: Matrix.PosSemiDef.IsSymm
Proof 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
Proof 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
Theorem: Matrix.PosSemiDef.IsSymm
Proof 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
Proof 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
Theorem: Matrix.PosSemiDef.IsSymm
Proof 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
Proof 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
Theorem: Matrix.PosSemiDef.IsSymm
Proof 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
Proof 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
Theorem: Matrix.PosSemiDef.IsSymm
Proof 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]
Proof state after:
no goals
Theorem: Matrix.PosSemiDef.IsSymm
Proof 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
Proof state after:
no goals
Theorem: Matrix.PosSemiDef.IsSymm
Proof 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
Proof state after:
no goals
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
⊢ match t.rotateSoCone x with
  | (v, w, x) => v.rotatedSoCone w x
Tactic:
simp [rotatedSoCone, rotateSoCone]
Proof state after:
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
⊢ ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ (t + x 0) / √2 * ((t - x 0) / √2) * 2 ∧ 0 ≤ (t + x 0) / √2 ∧ 0 ≤ (t - x 0) / √2
Theorem: Real.rotateSoCone_rotatedSoCone
Proof state before:
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
⊢ ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ (t + x 0) / √2 * ((t - x 0) / √2) * 2 ∧ 0 ≤ (t + x 0) / √2 ∧ 0 ≤ (t - x 0) / √2
Tactic:
have habsx0t : |x 0| ≤ t := by
  rw [soCone, Fin.sum_univ_succ] at h
  have hS : 0 ≤ ∑ i : Fin n, x (Fin.succ i) ^ 2 :=
    Finset.sum_nonneg (fun i _ => (rpow_two (x i.succ)).symm ▸ sq_nonneg (x i.succ))
  exact abs_le_of_sqrt_sq_add_nonneg_le hS h
Proof state after:
n✝ : Type ?u.2341
m : Type ?u.2338
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
t : ℝ
x : Fin n.succ → ℝ
h : t.soCone x
habsx0t : |x 0| ≤ t
⊢ ∑ x_1 : Fin n, x x_1.succ ^ 2 ≤ (t + x 0) / √2 * ((t - x 0) / √2) * 2 ∧ 0 ≤ (t + x 0) / √2 ∧ 0 ≤ (t - x 0) / √2