From 5fd6d0e101a1fbb611088be37a5932846c4b9e42 Mon Sep 17 00:00:00 2001 From: Sirui Lu Date: Sun, 21 Jun 2026 05:37:51 +0200 Subject: [PATCH] refactor(algebra): use Fintype sum zero criterion --- TNLean/Algebra/MatrixAux.lean | 4 ++-- TNLean/Algebra/PerronFrobenius/RankOne.lean | 4 ++-- TNLean/Channel/FixedPoint/Cesaro.lean | 5 +++-- TNLean/Channel/Irreducible/Growth/OneStep.lean | 4 ++-- TNLean/Channel/Semigroup/LiouvillianKernel.lean | 4 ++-- TNLean/MPS/Irreducible/FixedPointProjection.lean | 4 ++-- TNLean/QPF/PosDef.lean | 5 +++-- 7 files changed, 16 insertions(+), 14 deletions(-) diff --git a/TNLean/Algebra/MatrixAux.lean b/TNLean/Algebra/MatrixAux.lean index 819230d9a2..88988fc85b 100644 --- a/TNLean/Algebra/MatrixAux.lean +++ b/TNLean/Algebra/MatrixAux.lean @@ -92,8 +92,8 @@ theorem eq_zero_of_sum_mul_conjTranspose_eq_zero rw [← Complex.re_sum, ← Matrix.trace_sum, h] simp have htrace_re : ((B i * (B i)ᴴ).trace).re = 0 := - Finset.sum_eq_zero_iff_of_nonneg (fun j _ => htrace_nonneg j) - |>.mp htrace_sum i (Finset.mem_univ i) + congrFun (Fintype.sum_eq_zero_iff_of_nonneg (fun j => htrace_nonneg j) |>.mp + htrace_sum) i have htrace_zero : (B i * (B i)ᴴ).trace = 0 := Complex.ext htrace_re (Complex.le_def.mp (Matrix.posSemidef_self_mul_conjTranspose (B i)).trace_nonneg).2.symm diff --git a/TNLean/Algebra/PerronFrobenius/RankOne.lean b/TNLean/Algebra/PerronFrobenius/RankOne.lean index 7ada88c59d..3a2eb3d81f 100644 --- a/TNLean/Algebra/PerronFrobenius/RankOne.lean +++ b/TNLean/Algebra/PerronFrobenius/RankOne.lean @@ -86,8 +86,8 @@ private lemma exists_eq_one_of_sum_eq_one_sum_sq_eq_one_nonneg _ = 0 := by rw [h_sum, h_sq]; norm_num have hterm_zero : ∀ i, lam i * (1 - lam i) = 0 := by intro i - exact (Finset.sum_eq_zero_iff_of_nonneg - (fun j _ => hterm_nonneg j)).mp hsum_term i (Finset.mem_univ i) + exact congrFun (Fintype.sum_eq_zero_iff_of_nonneg + (fun j => hterm_nonneg j) |>.mp hsum_term) i have hex : ∃ i, lam i = 1 := by by_contra hno have hall_zero : ∀ i, lam i = 0 := by diff --git a/TNLean/Channel/FixedPoint/Cesaro.lean b/TNLean/Channel/FixedPoint/Cesaro.lean index 82301e5ebe..3bee6fe506 100644 --- a/TNLean/Channel/FixedPoint/Cesaro.lean +++ b/TNLean/Channel/FixedPoint/Cesaro.lean @@ -106,8 +106,9 @@ private theorem psd_orthogonal_difference_eq_zero have hre_sum : ∑ j, (star (e j) ⬝ᵥ Y.mulVec (e j)).re = 0 := by have h1 := map_sum Complex.reAddGroupHom (fun j => star (e j) ⬝ᵥ Y.mulVec (e j)) Finset.univ rw [← hY_tr_sum, hY_tr] at h1; exact h1.symm - have hre_zero := (Finset.sum_eq_zero_iff_of_nonneg (fun j _ => hre_nonneg j)).mp hre_sum - intro j; exact Complex.ext (hre_zero j (Finset.mem_univ _)) (him j) + have hre_zero := congrFun + (Fintype.sum_eq_zero_iff_of_nonneg (fun j => hre_nonneg j) |>.mp hre_sum) + intro j; exact Complex.ext (hre_zero j) (him j) -- Y.mulVec(e_j) = 0 via dotProduct_mulVec_zero_iff for (A+Y) or (B+Y) have hY_mulVec_zero : ∀ j, Y.mulVec (e j) = 0 := by intro j; rcases he_ker j with hA_ker | hB_ker diff --git a/TNLean/Channel/Irreducible/Growth/OneStep.lean b/TNLean/Channel/Irreducible/Growth/OneStep.lean index 120b0cd762..05d3860196 100644 --- a/TNLean/Channel/Irreducible/Growth/OneStep.lean +++ b/TNLean/Channel/Irreducible/Growth/OneStep.lean @@ -88,8 +88,8 @@ theorem posDef_of_ker_subset_irreducible_cp star ((K j')ᴴ *ᵥ v) ⬝ᵥ (A *ᵥ ((K j')ᴴ *ᵥ v))).re = 0 := by rw [← hsum]; simp [hqf_EA] rwa [Complex.re_sum] at this - have hre := (Finset.sum_eq_zero_iff_of_nonneg - (fun j' _ => hA_psd.re_dotProduct_nonneg _)).mp h_sum_re j (Finset.mem_univ _) + have hre := congrFun (Fintype.sum_eq_zero_iff_of_nonneg + (fun j' => hA_psd.re_dotProduct_nonneg _) |>.mp h_sum_re) j exact Complex.ext hre (hA_psd.isHermitian.im_star_dotProduct_mulVec_self _) exact (hA_psd.dotProduct_mulVec_zero_iff _).mp (h_each i) -- Step 2: Construct support projection Q = U * diag(sgn(λ)) * U† diff --git a/TNLean/Channel/Semigroup/LiouvillianKernel.lean b/TNLean/Channel/Semigroup/LiouvillianKernel.lean index 2f5c66fec4..5375ae3450 100644 --- a/TNLean/Channel/Semigroup/LiouvillianKernel.lean +++ b/TNLean/Channel/Semigroup/LiouvillianKernel.lean @@ -384,8 +384,8 @@ private theorem each_commutator_eq_zero_of_sum_eq_zero have h_tr_re : ((A * F.L j - F.L j * A)ᴴ * (A * F.L j - F.L j * A)).trace.re = 0 := le_antisymm - (by linarith [Finset.sum_eq_zero_iff_of_nonneg (fun k _ => h_each_nonneg k) - |>.mp h_tr_sum_re j (Finset.mem_univ j)]) + (le_of_eq <| congrFun (Fintype.sum_eq_zero_iff_of_nonneg + (fun k => h_each_nonneg k) |>.mp h_tr_sum_re) j) (h_each_nonneg j) have h_tr_zero : ((A * F.L j - F.L j * A)ᴴ * (A * F.L j - F.L j * A)).trace = 0 := diff --git a/TNLean/MPS/Irreducible/FixedPointProjection.lean b/TNLean/MPS/Irreducible/FixedPointProjection.lean index 94996a8f3e..300f8d7a42 100644 --- a/TNLean/MPS/Irreducible/FixedPointProjection.lean +++ b/TNLean/MPS/Irreducible/FixedPointProjection.lean @@ -266,8 +266,8 @@ private lemma ker_invariant_under_adjoint rw [← map_sum, ← hsum, hqf] exact Complex.zero_re have hre := - (Finset.sum_eq_zero_iff_of_nonneg (fun j _ => hρ_psd.re_dotProduct_nonneg _)).mp - h_sum_zero i (Finset.mem_univ _) + congrFun (Fintype.sum_eq_zero_iff_of_nonneg + (fun j => hρ_psd.re_dotProduct_nonneg _) |>.mp h_sum_zero) i exact Complex.ext hre (hρ_psd.isHermitian.im_star_dotProduct_mulVec_self _) intro i exact (hρ_psd.dotProduct_mulVec_zero_iff _).mp (h_each_zero i) diff --git a/TNLean/QPF/PosDef.lean b/TNLean/QPF/PosDef.lean index 1c649bd853..ddc021afaf 100644 --- a/TNLean/QPF/PosDef.lean +++ b/TNLean/QPF/PosDef.lean @@ -79,8 +79,9 @@ private lemma ker_invariant_under_adjoint have h_sum_zero : ∑ j, RCLike.re (star ((A j)ᴴ *ᵥ x) ⬝ᵥ (ρ *ᵥ ((A j)ᴴ *ᵥ x))) = 0 := by rw [← map_sum, ← hsum, hqf]; simp - have hre := (Finset.sum_eq_zero_iff_of_nonneg (fun j _ => hρ_psd.re_dotProduct_nonneg _)).mp - h_sum_zero i (Finset.mem_univ _) + have hre := congrFun + (Fintype.sum_eq_zero_iff_of_nonneg (fun j => hρ_psd.re_dotProduct_nonneg _) |>.mp + h_sum_zero) i exact Complex.ext hre (hρ_psd.isHermitian.im_star_dotProduct_mulVec_self _) intro i exact (hρ_psd.dotProduct_mulVec_zero_iff _).mp (h_each_zero i)