add file

.gitignore

@@ -0,0 +1 @@
+/.lake

Main.lean

@@ -0,0 +1,4 @@
+import «Tutorial»
+
+def main : IO Unit :=
+  IO.println s!"Hello World!"

Tutorial.lean

@@ -0,0 +1,3 @@
+-- This module serves as the root of the `Tutorial` library.
+-- Import modules here that should be built as part of the library.
+import «Tutorial».Basic

Tutorial/2-13a.lean

@@ -0,0 +1,123 @@
+import «Tutorial».Basic
+import Mathlib.Data.Matrix.Basic
+import Mathlib.Order.Filter.Basic
+import Mathlib.Topology.Basic
+import Mathlib.Order.Filter.Basic
+
+
+open GateauxDeriv Matrix Topology
+-- 2.13(a)
+
+-- 计算 a^T Xb 的导数，大致思路为容易验证导数 D 应当满足 D . V = a^T V b，取 D = a^T b ，分别验证两个等式即可
+-- 主要困难在于需要用开集的条件规约出tendsTo 内部的 t != 0，
+-- 这里通过用 eventuallyEq_nhdsWithin_of_eqOn 证明引理引导 apply tendsto_congr' 自动匹配解决
+theorem problem_a (a : Fin m → ℝ) (X : Matrix (Fin m) (Fin n) ℝ) (b : Fin n → ℝ)
+  : HasGateauxDerivAt (f_aXb a b) X (vecMulVec a b) := by
+    simp [HasGateauxDerivAt]
+    simp [Matrix.add_mulVec]
+    simp [Matrix.smul_mulVec_assoc]
+    simp [← div_mul_eq_mul_div]
+    intro V
+    have : innerProductofMatrix (vecMulVec a b) V = a ⬝ᵥ mulVec V b := by
+      rw [<- f_aXb]
+      apply Eq.symm
+      apply f_aXb_eq
+    rw [this]
+    have : (fun t => t / t * a ⬝ᵥ mulVec V b) =ᶠ[𝓝[≠] 0] (fun _ => a ⬝ᵥ mulVec V b) := by
+      apply eventuallyEq_nhdsWithin_of_eqOn
+      intro x h
+      simp
+      rw [div_self (h), one_mul]
+    apply (Filter.tendsto_congr' this).mpr
+    apply tendsto_const_nhds
+
+
+/--proof and state-/
+
+theorem problem_a_state (a : Fin m → ℝ) (X : Matrix (Fin m) (Fin n) ℝ) (b : Fin n → ℝ)
+  : HasGateauxDerivAt (f_aXb a b) X (vecMulVec a b) := by
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n ⊢ HasGateauxDerivAt (f_aXb a b) X (vecMulVec a b)-/
+    simp [HasGateauxDerivAt]
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n ⊢ ∀ (V : Matrix (Fin m) (Fin n) ℝ), Filter.Tendsto (fun t => (a ⬝ᵥ mulVec (X + t • V) b - a ⬝ᵥ mulVec X b) / t) (𝓝[≠] 0)
+    (𝓝 (innerProductofMatrix (vecMulVec a b) V))-/
+    simp [Matrix.add_mulVec]
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n ⊢ ∀ (V : Matrix (Fin m) (Fin n) ℝ), Filter.Tendsto (fun t => a ⬝ᵥ mulVec (t • V) b / t) (𝓝[≠] 0) (𝓝 (innerProductofMatrix (vecMulVec a b) V))-/
+    simp [Matrix.smul_mulVec_assoc]
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n ⊢ ∀ (V : Matrix (Fin m) (Fin n) ℝ), Filter.Tendsto (fun t => t * a ⬝ᵥ mulVec V b / t) (𝓝[≠] 0) (𝓝 (innerProductofMatrix (vecMulVec a b) V))-/
+    simp [← div_mul_eq_mul_div]
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n ⊢ ∀ (V : Matrix (Fin m) (Fin n) ℝ), Filter.Tendsto (fun t => t / t * a ⬝ᵥ mulVec V b) (𝓝[≠] 0) (𝓝 (innerProductofMatrix (vecMulVec a b) V))-/
+    intro V
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n V: Matrix (Fin m) (Fin n) ℝ \n ⊢ Filter.Tendsto (fun t => t / t * a ⬝ᵥ mulVec V b) (𝓝[≠] 0) (𝓝 (innerProductofMatrix (vecMulVec a b) V))-/
+    have : innerProductofMatrix (vecMulVec a b) V = a ⬝ᵥ mulVec V b := by
+      rw [<- f_aXb]
+      apply Eq.symm
+      apply f_aXb_eq
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n V: Matrix (Fin m) (Fin n) ℝ \n this: innerProductofMatrix (vecMulVec a b) V = a ⬝ᵥ mulVec V b \n ⊢ Filter.Tendsto (fun t => t / t * a ⬝ᵥ mulVec V b) (𝓝[≠] 0) (𝓝 (innerProductofMatrix (vecMulVec a b) V))-/
+    rw [this]
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n V: Matrix (Fin m) (Fin n) ℝ \n this: innerProductofMatrix (vecMulVec a b) V = a ⬝ᵥ mulVec V b \n ⊢ Filter.Tendsto (fun t => t / t * a ⬝ᵥ mulVec V b) (𝓝[≠] 0) (𝓝 (a ⬝ᵥ mulVec V b))-/
+    have : (fun t => t / t * a ⬝ᵥ mulVec V b) =ᶠ[𝓝[≠] 0] (fun _ => a ⬝ᵥ mulVec V b) := by
+      apply eventuallyEq_nhdsWithin_of_eqOn
+      intro x h
+      simp
+      rw [div_self (h), one_mul]
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n V: Matrix (Fin m) (Fin n) ℝ \n this✝: innerProductofMatrix (vecMulVec a b) V = a ⬝ᵥ mulVec V b \n this: (fun t => t / t * a ⬝ᵥ mulVec V b) =ᶠ[𝓝[≠] 0] fun x => a ⬝ᵥ mulVec V b \n ⊢ Filter.Tendsto (fun t => t / t * a ⬝ᵥ mulVec V b) (𝓝[≠] 0) (𝓝 (a ⬝ᵥ mulVec V b))-/
+    apply (Filter.tendsto_congr' this).mpr
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n V: Matrix (Fin m) (Fin n) ℝ \n this✝: innerProductofMatrix (vecMulVec a b) V = a ⬝ᵥ mulVec V b \n this: (fun t => t / t * a ⬝ᵥ mulVec V b) =ᶠ[𝓝[≠] 0] fun x => a ⬝ᵥ mulVec V b \n ⊢ Filter.Tendsto (fun x => a ⬝ᵥ mulVec V b) (𝓝[≠] 0) (𝓝 (a ⬝ᵥ mulVec V b))-/
+    apply tendsto_const_nhds
+    /-No goals-/
+
+
+/-no tactic-/
+
+theorem problem_a_notactic (a : Fin m → ℝ) (X : Matrix (Fin m) (Fin n) ℝ) (b : Fin n → ℝ)
+  : HasGateauxDerivAt (f_aXb a b) X (vecMulVec a b) := by
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n ⊢ HasGateauxDerivAt (f_aXb a b) X (vecMulVec a b)-/
+
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n ⊢ ∀ (V : Matrix (Fin m) (Fin n) ℝ), Filter.Tendsto (fun t => (a ⬝ᵥ mulVec (X + t • V) b - a ⬝ᵥ mulVec X b) / t) (𝓝[≠] 0)
+    (𝓝 (innerProductofMatrix (vecMulVec a b) V))-/
+
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n ⊢ ∀ (V : Matrix (Fin m) (Fin n) ℝ), Filter.Tendsto (fun t => a ⬝ᵥ mulVec (t • V) b / t) (𝓝[≠] 0) (𝓝 (innerProductofMatrix (vecMulVec a b) V))-/
+
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n ⊢ ∀ (V : Matrix (Fin m) (Fin n) ℝ), Filter.Tendsto (fun t => t * a ⬝ᵥ mulVec V b / t) (𝓝[≠] 0) (𝓝 (innerProductofMatrix (vecMulVec a b) V))-/
+
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n ⊢ ∀ (V : Matrix (Fin m) (Fin n) ℝ), Filter.Tendsto (fun t => t / t * a ⬝ᵥ mulVec V b) (𝓝[≠] 0) (𝓝 (innerProductofMatrix (vecMulVec a b) V))-/
+
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n V: Matrix (Fin m) (Fin n) ℝ \n ⊢ Filter.Tendsto (fun t => t / t * a ⬝ᵥ mulVec V b) (𝓝[≠] 0) (𝓝 (innerProductofMatrix (vecMulVec a b) V))-/
+
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n V: Matrix (Fin m) (Fin n) ℝ \n this: innerProductofMatrix (vecMulVec a b) V = a ⬝ᵥ mulVec V b \n ⊢ Filter.Tendsto (fun t => t / t * a ⬝ᵥ mulVec V b) (𝓝[≠] 0) (𝓝 (innerProductofMatrix (vecMulVec a b) V))-/
+
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n V: Matrix (Fin m) (Fin n) ℝ \n this: innerProductofMatrix (vecMulVec a b) V = a ⬝ᵥ mulVec V b \n ⊢ Filter.Tendsto (fun t => t / t * a ⬝ᵥ mulVec V b) (𝓝[≠] 0) (𝓝 (a ⬝ᵥ mulVec V b))-/
+
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n V: Matrix (Fin m) (Fin n) ℝ \n this✝: innerProductofMatrix (vecMulVec a b) V = a ⬝ᵥ mulVec V b \n this: (fun t => t / t * a ⬝ᵥ mulVec V b) =ᶠ[𝓝[≠] 0] fun x => a ⬝ᵥ mulVec V b \n ⊢ Filter.Tendsto (fun t => t / t * a ⬝ᵥ mulVec V b) (𝓝[≠] 0) (𝓝 (a ⬝ᵥ mulVec V b))-/
+
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n V: Matrix (Fin m) (Fin n) ℝ \n this✝: innerProductofMatrix (vecMulVec a b) V = a ⬝ᵥ mulVec V b \n this: (fun t => t / t * a ⬝ᵥ mulVec V b) =ᶠ[𝓝[≠] 0] fun x => a ⬝ᵥ mulVec V b \n ⊢ Filter.Tendsto (fun x => a ⬝ᵥ mulVec V b) (𝓝[≠] 0) (𝓝 (a ⬝ᵥ mulVec V b))-/
+
+    /-No goals-/
+    sorry
+
+theorem problem_a_1 (a : Fin m → ℝ) (X : Matrix (Fin m) (Fin n) ℝ) (b : Fin n → ℝ)
+  : HasGateauxDerivAt (f_aXb a b) X (vecMulVec a b) := by
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n ⊢ HasGateauxDerivAt (f_aXb a b) X (vecMulVec a b)-/
+    simp [HasGateauxDerivAt]
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n ⊢ ∀ (V : Matrix (Fin m) (Fin n) ℝ), Filter.Tendsto (fun t => (a ⬝ᵥ mulVec (X + t • V) b - a ⬝ᵥ mulVec X b) / t) (𝓝[≠] 0)
+    (𝓝 (innerProductofMatrix (vecMulVec a b) V))-/
+    simp [Matrix.add_mulVec]
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n ⊢ ∀ (V : Matrix (Fin m) (Fin n) ℝ), Filter.Tendsto (fun t => a ⬝ᵥ mulVec (t • V) b / t) (𝓝[≠] 0) (𝓝 (innerProductofMatrix (vecMulVec a b) V))-/
+    simp [Matrix.smul_mulVec_assoc]
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n ⊢ ∀ (V : Matrix (Fin m) (Fin n) ℝ), Filter.Tendsto (fun t => t * a ⬝ᵥ mulVec V b / t) (𝓝[≠] 0) (𝓝 (innerProductofMatrix (vecMulVec a b) V))-/
+    simp [← div_mul_eq_mul_div]
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n ⊢ ∀ (V : Matrix (Fin m) (Fin n) ℝ), Filter.Tendsto (fun t => t / t * a ⬝ᵥ mulVec V b) (𝓝[≠] 0) (𝓝 (innerProductofMatrix (vecMulVec a b) V))-/
+    intro V
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n V: Matrix (Fin m) (Fin n) ℝ \n ⊢ Filter.Tendsto (fun t => t / t * a ⬝ᵥ mulVec V b) (𝓝[≠] 0) (𝓝 (innerProductofMatrix (vecMulVec a b) V))-/
+    have : innerProductofMatrix (vecMulVec a b) V = a ⬝ᵥ mulVec V b := by
+     sorry
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n V: Matrix (Fin m) (Fin n) ℝ \n this: innerProductofMatrix (vecMulVec a b) V = a ⬝ᵥ mulVec V b \n ⊢ Filter.Tendsto (fun t => t / t * a ⬝ᵥ mulVec V b) (𝓝[≠] 0) (𝓝 (innerProductofMatrix (vecMulVec a b) V))-/
+    rw [this]
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n V: Matrix (Fin m) (Fin n) ℝ \n this: innerProductofMatrix (vecMulVec a b) V = a ⬝ᵥ mulVec V b \n ⊢ Filter.Tendsto (fun t => t / t * a ⬝ᵥ mulVec V b) (𝓝[≠] 0) (𝓝 (a ⬝ᵥ mulVec V b))-/
+    have : (fun t => t / t * a ⬝ᵥ mulVec V b) =ᶠ[𝓝[≠] 0] (fun _ => a ⬝ᵥ mulVec V b) := by
+      sorry
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n V: Matrix (Fin m) (Fin n) ℝ \n this✝: innerProductofMatrix (vecMulVec a b) V = a ⬝ᵥ mulVec V b \n this: (fun t => t / t * a ⬝ᵥ mulVec V b) =ᶠ[𝓝[≠] 0] fun x => a ⬝ᵥ mulVec V b \n ⊢ Filter.Tendsto (fun t => t / t * a ⬝ᵥ mulVec V b) (𝓝[≠] 0) (𝓝 (a ⬝ᵥ mulVec V b))-/
+    apply (Filter.tendsto_congr' this).mpr
+    /-m n: ℕ \n a: Fin m → ℝ \n X: Matrix (Fin m) (Fin n) ℝ \n b: Fin n → ℝ \n V: Matrix (Fin m) (Fin n) ℝ \n this✝: innerProductofMatrix (vecMulVec a b) V = a ⬝ᵥ mulVec V b \n this: (fun t => t / t * a ⬝ᵥ mulVec V b) =ᶠ[𝓝[≠] 0] fun x => a ⬝ᵥ mulVec V b \n ⊢ Filter.Tendsto (fun x => a ⬝ᵥ mulVec V b) (𝓝[≠] 0) (𝓝 (a ⬝ᵥ mulVec V b))-/
+    apply tendsto_const_nhds
+    /-No goals-/

Tutorial/2-13b.lean

@@ -0,0 +1,205 @@
+-- package
+import Mathlib.Data.Matrix.Basic
+import Mathlib.Data.Matrix.Notation
+import Mathlib.Data.Matrix.Block
+import Mathlib.Data.Matrix.RowCol
+
+import Mathlib.Data.Matrix.Reflection
+
+import Mathlib.Topology.Basic
+import Mathlib.Topology.Instances.Matrix
+
+import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
+import Mathlib.Data.Nat.Basic
+import Mathlib.Data.Real.Basic
+import Mathlib.LinearAlgebra.Matrix.Trace
+import Mathlib.Algebra.BigOperators.Basic
+import Mathlib.Data.Fin.Tuple.Reflection
+import Mathlib.LinearAlgebra.Matrix.PosDef
+import Mathlib.LinearAlgebra.Matrix.Adjugate
+import Mathlib.LinearAlgebra.FiniteDimensional
+
+-- 环境
+open BigOperators
+open Finset
+open Matrix
+-- 矩阵内积
+def innerProductofMatrix {n m : Nat} (a b : Matrix (Fin n) (Fin m) ℝ) : ℝ :=
+  ∑ i : Fin n, ∑ j : Fin m, (a i j) * (b i j)
+
+-- 定义trace
+-- ⟨a, b⟩ = trace (aᴴ * b)
+@[simp]
+def traceMHDotM (n m : Nat) (a b: Matrix (Fin n) (Fin m) ℝ) : ℝ :=
+  trace (aᵀ   * b)
+
+theorem iProd_eq_traceDot (n m : Nat) (a b : Matrix (Fin n) (Fin m) ℝ) :
+  innerProductofMatrix a b = traceMHDotM n m a b := by
+    rw [innerProductofMatrix, traceMHDotM]
+    rw [← mulᵣ_eq, mulᵣ]
+    rw [trace]
+    simp [dotProduct]
+    exact Finset.sum_comm
+
+variable {m n : ℕ}
+-- 收敛列
+@[simp]
+def ConvergesTo (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N,  ∀ n ≥ N , |s n - a| < ε
+
+-- def ConvergesTo (s : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, (∀ n ≥ N ∧ s n ≠ 0 ),  |s n - a| < ε
+-- 定义Gateaux导数
+@[simp]
+def HasGateauxDerivAt (m n: ℕ) (f : Matrix (Fin m) (Fin n) ℝ → ℝ) (X : Matrix (Fin m) (Fin n) ℝ)
+ (t : ℕ → ℝ)(_ : ∀ ε > 0, ∃ N,  ∀ n ≥ N , |t n - (0:ℝ)| < ε ∧ (t n ≠ 0))
+   : Prop
+   := ∀ V : Matrix (Fin m) (Fin n) ℝ, ∃ G : Matrix (Fin m) (Fin n) ℝ,
+   ConvergesTo (fun n ↦ ((f (X + (t n)•V) - f X)/(t n) - innerProductofMatrix G V)) 0
+-- 定义problem_b的函数
+@[simp]
+def f_XAX (A : Matrix (Fin m) (Fin m) ℝ) : Matrix (Fin m) (Fin n) ℝ → ℝ :=
+  fun X => trace (Xᵀ * A * X)
+
+#check mul_lt_mul_of_pos_right
+section
+variable (t : ℕ → ℝ) (t0 :  ∀ ε > 0, ∃ N,  ∀ n ≥ N , |t n - (0:ℝ)| < ε ∧ (t n ≠ 0))
+-- 主定理证明
+theorem problem_b (m n: ℕ) (A : Matrix (Fin m) (Fin m) ℝ) (X : Matrix (Fin m) (Fin n) ℝ):
+HasGateauxDerivAt m n (f_XAX A) X t t0 := by
+  simp
+  intro V
+  -- 实例化G
+  have h₀ :∀k : ℕ , t k ≠ 0 → ((trace ((Xᵀ +  t k • Vᵀ) * A * (X +  t k • V)) - trace (Xᵀ * A * X)))/(t k) = trace ((A + Aᵀ) * X * Vᵀ) +  (t k) * trace (Vᵀ * A * V) := by
+    intro k hk
+    simp [Matrix.add_mul]
+    simp [Matrix.mul_add]
+    simp [mul_add]
+    simp [add_assoc]
+    simp [← add_assoc]
+    simp [← mul_add]
+    simp [← div_mul_eq_mul_div]
+    have h :  trace (Xᵀ * A * V) = trace (Aᵀ * X * Vᵀ) := by
+      rw [trace_mul_comm]
+      rw [← trace_transpose]
+      rw [Matrix.transpose_mul]
+      rw [Matrix.transpose_mul]
+      simp
+    rw [h]
+
+    have h1 : trace (Vᵀ * A * X) = trace (A * X * Vᵀ) := by
+      rw [Matrix.mul_assoc]
+      rw [trace_mul_comm]
+    rw [h1]
+    rw [div_self]
+    simp
+    rw [add_comm]
+    apply hk
+
+  use (A + Aᵀ) * X
+  intro ε hε
+  -- 利用 t0 假设找N
+  rcases lt_trichotomy (trace (Vᵀ * A * V)) 0 with hl | he | hg
+
+  -- trace (Vᵀ * A * V) < 0的情况
+  · have h₁ : ε / |trace (Vᵀ * A * V)| > 0 := by
+      apply div_pos hε
+      apply abs_pos_of_neg hl
+    rcases t0 (ε/|trace (Vᵀ * A * V)|) h₁ with ⟨N, h₂⟩
+    use N
+    intro n' h₃
+    -- 换掉内积
+    -- 换掉结论前半段
+    rw[h₀ n']
+    -- 换掉结论中的内积
+    · have h₄ : innerProductofMatrix ((A + Aᵀ) * X) V = trace ((A + Aᵀ) * X * Vᵀ) := by
+        rw [iProd_eq_traceDot, traceMHDotM, ← trace_transpose, Matrix.transpose_mul]
+        simp
+        rw [trace_mul_comm]
+
+      rw[h₄]
+      simp
+      rw[abs_mul]
+      -- intro h₅
+      specialize h₂ n' h₃
+      rcases h₂ with ⟨h₂_l, _⟩
+      calc
+        |t n'| * |trace (Vᵀ * A * V)| < (ε / |trace (Vᵀ * A * V)|) * |trace (Vᵀ * A * V)| := by
+          have this : |trace (Vᵀ * A * V)| > 0 := by
+            apply abs_pos_of_neg hl
+          rw[← sub_zero (t n')]
+          apply mul_lt_mul_of_pos_right h₂_l this
+          -- sorry
+        _ = ε :=
+        by
+          ring_nf
+          rw [mul_assoc]
+          field_simp
+          rw [mul_div_assoc]
+          rw [div_self]
+          simp
+          simp [hl]
+          intro s
+          absurd hl
+          rw [s]
+          simp
+    · specialize h₂ n' h₃
+      rcases h₂ with ⟨_, h_r⟩
+      apply h_r
+
+
+  -- trace (Vᵀ * A * V) = 0 的情况
+  · rcases t0 ε hε with ⟨N, h₂⟩
+    use N
+    intro n'
+    intro h1
+    rw[h₀ n']
+    rw [he]
+    simp
+    have h₄ : innerProductofMatrix ((A + Aᵀ) * X) V = trace ((A + Aᵀ) * X * Vᵀ) := by
+      rw [iProd_eq_traceDot, traceMHDotM, ← trace_transpose, Matrix.transpose_mul]
+      simp
+      rw [trace_mul_comm]
+    rw[h₄]
+    simp
+    exact hε
+    · specialize h₂ n' h1
+      rcases h₂ with ⟨_, h_r⟩
+      apply h_r
+
+-- trace (Vᵀ * A * V) > 0
+  · have h₁ : ε / |trace (Vᵀ * A * V)| > 0 := by
+      apply div_pos hε
+      apply abs_pos_of_pos hg
+-- #check abs_pos_of_pos
+    rcases t0 (ε/|trace (Vᵀ * A * V)|) h₁ with ⟨N, h₂⟩
+    use N
+    intro n' h₃
+    -- 换掉内积
+    -- 换掉结论前半段
+    rw[h₀ n']
+    -- 换掉结论中的内积
+    · have h₄ : innerProductofMatrix ((A + Aᵀ) * X) V = trace ((A + Aᵀ) * X * Vᵀ) := by
+        rw [iProd_eq_traceDot, traceMHDotM, ← trace_transpose, Matrix.transpose_mul]
+        simp
+        rw [trace_mul_comm]
+
+      rw[h₄]
+      simp
+      rw[abs_mul]
+      -- intro h₅
+      specialize h₂ n' h₃
+      rcases h₂ with ⟨h₂_l, _⟩
+      calc
+        |t n'| * |trace (Vᵀ * A * V)| < (ε / |trace (Vᵀ * A * V)|) * |trace (Vᵀ * A * V)| := by
+          have this : |trace (Vᵀ * A * V)| > 0 := by
+            apply abs_pos_of_pos hg
+          rw[← sub_zero (t n')]
+          apply mul_lt_mul_of_pos_right h₂_l this
+          -- sorry
+        _ = ε :=
+        by
+          ring_nf
+          rw [mul_assoc]
+          field_simp
+    · specialize h₂ n' h₃
+      rcases h₂ with ⟨_, h_r⟩
+      apply h_r