I encountered a summation problem in Lean4

Stream: mathlib4

[Planck Anderson]

A finite summation expression equals 0. I used apply Finset.sum_eq_zero, and after using split_ifs, I found that when x = a, the expression equals -1; when x = b, it equals 1; and in all other cases, it equals 0. I don't know how to exclude these two cases and compute them separately.

[Yaël Dillies]

Can you provide a #mwe ?

[Planck Anderson]

The goal is :(you know I am dealing with some matrix multiplication as I am formalizeing gaussian elimination.)

⊢ (∑ x,
    (if a = x then 1 else if True ∧ x = i then -M.R a j / M.R i j else 0) *
      if x = i then 1 else if x > i ∧ True then M.R x j / M.R i j else 0) =
  0

After I apply Finset.sum_eq_zero, it become like this

⊢ ∀ x ∈ Finset.univ,
  ((if a = x then 1 else if True ∧ x = i then -M.R a j / M.R i j else 0) *
      if x = i then 1 else if x > i ∧ True then M.R x j / M.R i j else 0) =
    0

After

    intro p hp
    simp
    split_ifs
    · exfalso
      expose_names;rw [← h_1, h_2] at h_ai; exact (lt_irrefl p) h_ai

I found some contradiction

p : Fin n
hp : p ∈ Finset.univ
h✝¹ : p = i
h✝ : ¬a = p
⊢ -M.R a j / M.R i j = 0

and

p : Fin n
hp : p ∈ Finset.univ
h✝² : ¬p = i
h✝¹ : i < p
h✝ : a = p
⊢ M.R p j / M.R i j = 0

[Yaël Dillies]

Thanks! But this is not a #mwe: If you click on this button, then you willl see that your code block is broken and that I can't see the same infoview as you do

[Planck Anderson]

lemma Gaussian.gaussian_elimination_row_eq_left_mul (i : Fin n) (j : Fin m) (h : M.R i j ≠ 0) :
    ∃ (P : GL (Fin n) K), P.1 • M = M.gaussian_elimination_step_row i j := by
  have id_eqzero (a b : Fin n) (h: a ≠ b): (1 : Matrix (Fin n) (Fin n) K) a b = 0 := by simp [h]
  have id_eqone (a b : Fin n) (h: a = b): (1 : Matrix (Fin n) (Fin n) K) a b = 1 := by sorry
  have h_mul (A : Matrix (Fin n) (Fin n) K) (B : Matrix (Fin n) (Fin n) K) (C : Matrix (Fin n) (Fin n) K) (i : Fin n) (j : Fin n): (A * B) i j  - (C * B) i j = ((A - C) * B) i j := by sorry
  have h_mul'(A : Fin n → K) (B : Fin n → K) (j : Fin n): A j  - B j = (A - B) j := by sorry
  let P_mat : Matrix (Fin n) (Fin n) K := fun k l =>
    if k = l then 1
    else if k > i ∧ l = i then -(M.R k j) / (M.R i j)
    else 0
  let P_inv : Matrix (Fin n) (Fin n) K := fun k l =>
    if k = l then 1
    else if k > i ∧ l = i then (M.R k j) / (M.R i j)
    else 0
  have h_inv1 : P_mat * P_inv = 1 := by
    ext a b
    simp only [P_mat, P_inv, Matrix.mul_apply]
    by_cases h_ab : a = b
    rw [h_ab]
    rw [← Finset.sum_add_sum_compl {b}]
    simp
    apply Finset.sum_eq_zero
    intro p hp
    have : p ≠ b := by simpa using hp
    simp [this]
    intro hp1 hp2
    split_ifs
    · exfalso
      (expose_names; exact this (id (Eq.symm h_1)))
    · exfalso
      expose_names
      obtain ⟨h_21, h_22⟩ := h_2
      rw [hp2] at h_21
      exact (lt_self_iff_false i).mp h_21
    rfl
    by_cases h_ai : a > i
    by_cases h_bi : b = i
    simp only [h_ai, h_bi, id_eqzero _ _ h_ab]

    apply Finset.sum_eq_zero
    intro p hp
    simp
    split_ifs
    · exfalso
      expose_names;rw [← h_1, h_2] at h_ai; exact (lt_irrefl p) h_ai
    · sorry
    · sorry
    · rfl
    rfl
    simp only [h_ai, h_bi, id_eqzero _ _ h_ab]
    apply Finset.sum_eq_zero
    intro p hp
    simp
    intro p'
    split_ifs
    · exfalso
      expose_names;exact h_ab (h_1.trans p')
    · exfalso
      expose_names;exact h_bi ((Eq.symm p').trans h_2)
    rfl
    simp only [h_ai, id_eqzero _ _ h_ab]
    apply Finset.sum_eq_zero
    intro p hp
    simp
    split_ifs
    · exfalso
      expose_names;exact h_ab (h_2.trans h_1)
    · rfl
    · exfalso
      expose_names;obtain ⟨h_21, h_22⟩ := h_2;rw [← h_3] at h_21;exact h_ai h_21
    rfl
    rfl

[Planck Anderson]

I am so sorry

[Yaël Dillies]

You're still missing imports :slight_smile:

[Planck Anderson]

it will be some cruddy code

[Kenny Lau]

@Planck Anderson well, you took a wrong turn in your proof and obtained an unprovable goal

[Kenny Lau]

so go back where you came from

[Kenny Lau]

and use sum_subset instead

[Planck Anderson]

thanks a lot!

[Planck Anderson]

@Kenny Lau yeah but it seems sum_subset does not work
image.png

[Planck Anderson]

（someone deleted this）

[Planck Anderson]

@Yaël Dillies there will be a lot of matrix multiplications here, I feel so sad to deal with a lot of summation... :melting_face:

[Ruben Van de Velde]

You shouldn't use Lean.Grind.* lemmas directly, I don't think

[Dexin Zhang]

docs#Finset.sum_erase_add can separate one element from a sum

[Planck Anderson]

I have solved this problem. use Finset.sum_eq_add_sum_diff_singleton to exclude the two special situations

[Planck Anderson]

anyway, thanks for your guys help, love you guys, I like lean community and it is really warm, you guys are really approachable and glad to help others.

[Planck Anderson]

Now I am here, sad to deal with some matrix multiplication, especially some matrix are not determinate.

import Mathlib

#check Matrix

variable {α : Type*}
open Matrix Equiv Nat List

section Basic

variable {n m} (M : Matrix (Fin n) (Fin m) α)

def swap_rows  (i j : Fin n) : Matrix (Fin n) (Fin m) α :=
    M.submatrix (swap i j : Perm (Fin n)) id



def swap_cols  (i j : Fin m) : Matrix (Fin n) (Fin m) α :=
   (swap_rows M.transpose i j).transpose

def gaussian_update [Add α] [Mul α] [Sub α]
    (i k : Fin n) (a b : α) : (Fin m) → α :=
  if k ≤ i then M k else a • M k - b • M i

def gaussian_update_row [Add α] [Mul α] [Sub α]
  (i : Fin n) (j : Fin m):
  Matrix (Fin n) (Fin m) α :=
  fun k => gaussian_update M i k (M i j) (M k j)

end Basic
@[ext]
structure Gaussian (n m α) [Ring α] where
  P : Matrix (Fin n) (Fin n) α
  R : Matrix (Fin n) (Fin m) α
  Q : Matrix (Fin m) (Fin m) α
  M : Matrix (Fin n) (Fin m) α
  hm : P * M * Q = R
  -- P M Q = [I_r, 0;
            -- 0, 0]
instance {n m α} [Ring α] : SMul (Matrix (Fin n) (Fin n) α) (Gaussian n m α) where
  smul := fun P B => (⟨P * B.P, P * B.R, B.Q, B.M, by simp [B.hm, Matrix.mul_assoc];⟩ : Gaussian n m α)

instance {n m α} [Ring α] : SMul (Matrix (Fin m) (Fin m) α) (Gaussian n m α) where
  smul := fun Q B => (⟨B.P, B.R * Q, B.Q * Q, B.M, by rw [← B.hm]; simp [Matrix.mul_assoc];⟩ : Gaussian n m α)

section Gauss
variable {n m} [Ring α] (M : Gaussian n m α) [NeZero n] [NeZero m]

def find_pivot_col [LinearOrder α] (M : Fin n → α) (i : Fin n): Fin n :=
  (argmax (abs ∘ M) ((finRange n).rtake (n - i))).getD 0

def Gaussian.gaussian_elimination_step_row (i : Fin n) (j : Fin m)
    : Gaussian n m α where
  P := fun k => gaussian_update M.P i k (M.R i j) (M.R k j)
  R := gaussian_update_row M.R i j
  Q := M.Q
  M := M.M
  hm := by
    funext k
    simp only [gaussian_update, gaussian_update_row, Matrix.mul_apply_eq_vecMul,
      Matrix.vecMul_vecMul, ← M.hm]
    split_ifs with h_le
    simp
    simp [sub_vecMul, Matrix.vecMul_smul, Matrix.vecMul_smul]
end Gauss

section PrimaryTransformation
variable {m n : ℕ} {i : Fin n} {j : Fin m} {K : Type*}  [CommRing K] (M : Gaussian n m K)

#check (⟨1,1,by simp, by simp⟩: GL (Fin n) K)

@[simp]
def row_trans_matrix (M : Gaussian n m K) (i : Fin n) (j : Fin m) : Matrix (Fin n) (Fin n) K :=
  fun k l =>
    if k = l then 1
    else if k > i ∧ l = i then -(M.R k j)
    else 0

@[simp]
def row_trans_matrix_inv (M : Gaussian n m K) (i : Fin n) (j : Fin m) : Matrix (Fin n) (Fin n) K :=
  fun k l =>
    if k = l then 1
    else if k > i ∧ l = i then (M.R k j)
    else 0

lemma id_eqzero (a b : Fin n) (h: a ≠ b): (1 : Matrix (Fin n) (Fin n) K) a b = 0 := by simp [h]
lemma id_eqone (a b : Fin n) (h: a = b): (1 : Matrix (Fin n) (Fin n) K) a b = 1 := by rw[← h]; exact one_apply_eq a

lemma row_trans_matrix_mul_inv_eq_one (M : Gaussian n m K) (i : Fin n) (j : Fin m) :
  row_trans_matrix M i j * row_trans_matrix_inv M i j = 1 := by
    ext a b
    simp only [row_trans_matrix, row_trans_matrix_inv, Matrix.mul_apply]
    by_cases h_ab : a = b
    rw [h_ab]
    rw [← Finset.sum_add_sum_compl {b}]
    simp
    apply Finset.sum_eq_zero
    intro p hp
    have : p ≠ b := by simpa using hp
    simp [this]
    intro hp1 hp2
    split_ifs
    · exfalso
      (expose_names;exact this (id (Eq.symm h)))
    · exfalso
      expose_names
      rw [hp2] at h
      exact h (Eq.symm h_1.2)
    ring
    by_cases h_ai : a > i
    by_cases h_bi : b = i
    simp only [h_ai, id_eqzero _ _ h_ab]
    have h_be0: b ∈ Finset.univ := by exact Finset.mem_univ b
    rw [Finset.sum_eq_add_sum_diff_singleton (Finset.mem_univ a)]
    have h_be: b ∈ Finset.univ \ {a} := by rw [Finset.mem_sdiff];constructor;exact h_be0;exact Finset.notMem_singleton.mpr fun a_1 => h_ab (id (Eq.symm a_1))
    rw [Finset.sum_eq_add_sum_diff_singleton h_be]
    have h_be1: i < a ∧ b = i := by constructor;apply h_ai;exact h_bi
    have h_be3: ¬ a = i := by exact Fin.ne_of_gt h_ai
    simp only [h_ab, h_be1, h_bi, h_be3]
    simp
    apply Finset.sum_eq_zero
    intro p hp
    split_ifs
    · exfalso;expose_names;rw [h_1, h] at h_be3;exact h_be3 rfl
    · exfalso;expose_names
      have hineq1 : p ≠ i := by rw [Finset.mem_sdiff] at hp;obtain ⟨h_1, h_2⟩ := hp;exact ne_of_not_mem_cons h_2
      apply hineq1 h
    · exfalso;expose_names
      have hineq2 : p ≠ a := by rw [Finset.mem_sdiff] at hp;obtain ⟨h_1, h_2⟩ := hp;rw [Finset.mem_sdiff] at h_1;obtain ⟨h_3, h_4⟩ := h_1;exact ne_of_not_mem_cons h_4
      apply hineq2 (Eq.symm h_2)
    · ring
    ring
    simp only [h_ai, h_bi, id_eqzero _ _ h_ab]
    apply Finset.sum_eq_zero
    intro p hp
    simp
    intro p'
    split_ifs
    · exfalso
      expose_names;rw [h, p'] at h_ab;exact h_ab rfl
    · exfalso
      expose_names;rw [h_1] at p';apply absurd (Eq.symm p') h_bi
    ring
    simp only [h_ai, id_eqzero _ _ h_ab]
    apply Finset.sum_eq_zero
    intro p hp
    simp
    split_ifs
    · exfalso
      expose_names;rw [← h_1] at h;exact h_ab h
    · rfl
    · exfalso
      expose_names;obtain ⟨h_21, h_22⟩ := h_2;exact h_ai h_1.1
    ring
    ring

lemma row_trans_matrix_inv_mul_eq_one (M : Gaussian n m K) (i : Fin n) (j : Fin m) :
  row_trans_matrix_inv M i j * row_trans_matrix M i j = 1 := by
    ext a b
    simp only [row_trans_matrix_inv, row_trans_matrix, Matrix.mul_apply]
    by_cases h_ab : a = b
    rw [h_ab]
    rw [← Finset.sum_add_sum_compl {b}]
    simp
    apply Finset.sum_eq_zero
    intro p hp
    have : p ≠ b := by simpa using hp
    simp [this]
    intro hp1 hp2
    split_ifs
    · exfalso
      (expose_names;exact this (id (Eq.symm h)))
    · exfalso
      expose_names
      rw [hp2] at h
      exact h (Eq.symm h_1.2)
    ring
    by_cases h_ai : a > i
    by_cases h_bi : b = i
    simp only [h_ai, id_eqzero _ _ h_ab]
    have h_be0: b ∈ Finset.univ := by exact Finset.mem_univ b
    rw [Finset.sum_eq_add_sum_diff_singleton (Finset.mem_univ a)]
    have h_be: b ∈ Finset.univ \ {a} := by rw [Finset.mem_sdiff];constructor;exact h_be0;exact Finset.notMem_singleton.mpr fun a_1 => h_ab (id (Eq.symm a_1))
    rw [Finset.sum_eq_add_sum_diff_singleton h_be]
    have h_be1: i < a ∧ b = i := by constructor;apply h_ai;exact h_bi
    have h_be3: ¬ a = i := by exact Fin.ne_of_gt h_ai
    simp only [h_ab, h_be1, h_bi, h_be3]
    simp
    apply Finset.sum_eq_zero
    intro p hp
    split_ifs
    · exfalso;expose_names;rw [h_1, h] at h_be3;exact h_be3 rfl
    · exfalso;expose_names
      have hineq1 : p ≠ i := by rw [Finset.mem_sdiff] at hp;obtain ⟨h_1, h_2⟩ := hp;exact ne_of_not_mem_cons h_2
      apply hineq1 h
    · exfalso;expose_names
      have hineq2 : p ≠ a := by rw [Finset.mem_sdiff] at hp;obtain ⟨h_1, h_2⟩ := hp;rw [Finset.mem_sdiff] at h_1;obtain ⟨h_3, h_4⟩ := h_1;exact ne_of_not_mem_cons h_4
      apply hineq2 (Eq.symm h_2)
    · ring
    ring
    simp only [h_ai, h_bi, id_eqzero _ _ h_ab]
    apply Finset.sum_eq_zero
    intro p hp
    simp
    intro p'
    split_ifs
    · exfalso
      expose_names;rw [h, p'] at h_ab;exact h_ab rfl
    · exfalso
      expose_names;rw [h_1] at p';apply absurd (Eq.symm p') h_bi
    ring
    simp only [h_ai, id_eqzero _ _ h_ab]
    apply Finset.sum_eq_zero
    intro p hp
    simp
    split_ifs
    · exfalso
      expose_names;rw [← h_1] at h;exact h_ab h
    · rfl
    · exfalso
      expose_names;obtain ⟨h_21, h_22⟩ := h_2;exact h_ai h_1.1
    ring
    ring  --证明过程完全一模一样，不知道怎么简化

lemma Gaussian.gaussian_elimination_row_eq_left_mul :
    ∃ (P : GL (Fin n) K), P.1 • M = M.gaussian_elimination_step_row i j := by
  have h_mul₁ (A : Matrix (Fin n) (Fin n) K) (B : Matrix (Fin n) (Fin n) K) (C : Matrix (Fin n) (Fin n) K) (i : Fin n) (j : Fin n): (A * B) i j  - (C * B) i j = ((A - C) * B) i j := by simp only [Matrix.mul_apply];rw [← Finset.sum_sub_distrib]; congr; funext k; simp [sub_mul]
  have h_mul₂ (A : Matrix (Fin n) (Fin n) K) (B : Matrix (Fin n) (Fin m) K) (C : Matrix (Fin n) (Fin n) K) (i : Fin n) (j : Fin m): (A * B) i j  - (C * B) i j = ((A - C) * B) i j := by simp only [Matrix.mul_apply];rw [← Finset.sum_sub_distrib]; congr; funext k; simp [sub_mul]
  let P_mat := row_trans_matrix M i j
  let P_inv := row_trans_matrix_inv M i j
  let P : GL (Fin n) K := ⟨P_mat, P_inv, row_trans_matrix_mul_inv_eq_one M i j, row_trans_matrix_inv_mul_eq_one M i j⟩
  use P
  have h₁: P.1 • M = ⟨P.1 * M.P, P.1 * M.R, M.Q, M.M, by simp [M.hm, Matrix.mul_assoc];⟩ := by
    exact rfl
  have h₂: M.gaussian_elimination_step_row i j = ⟨fun k => gaussian_update M.P i k (M.R i j) (M.R k j), fun k => gaussian_update M.R i k (M.R i j) (M.R k j), M.Q, M.M, by
    funext k
    simp only [gaussian_update, gaussian_update_row, Matrix.mul_apply_eq_vecMul,
      Matrix.vecMul_vecMul, ← M.hm]
    split_ifs with h_le
    simp
    simp [sub_vecMul, Matrix.vecMul_smul, Matrix.vecMul_smul];⟩ := by rfl
  rw [h₁, h₂]
  congr
  · ext
    simp only [Gaussian.gaussian_elimination_step_row, gaussian_update, P, P_mat, row_trans_matrix]
    rw [← sub_eq_zero]
    nth_rewrite 2 [← Matrix.one_mul M.P]
    split_ifs with h_ki
    rw [h_mul₁]
    simp only [Matrix.mul_apply]
    apply Finset.sum_eq_zero
    intro p hp
    simp
    split_ifs
    expose_names;simp only [id_eqone _ _ h];ring
    exfalso;expose_names;apply lt_irrefl i_1;exact (lt_of_le_of_lt h_ki h_1.1)
    expose_names;simp only [id_eqzero _ _ h];ring
    rw [Pi.sub_apply]
    sorry
  ext
  simp only [Gaussian.gaussian_elimination_step_row, gaussian_update, P, P_mat]
  rw [← sub_eq_zero]
  nth_rewrite 3 [← Matrix.one_mul M.R]
  split_ifs with h_ki
  nth_rewrite 2 [← Matrix.one_mul M.R]
  rw [h_mul₂]
  simp only [Matrix.mul_apply]
  apply Finset.sum_eq_zero
  intro p hp
  simp
  split_ifs
  expose_names;simp only [id_eqone _ _ h];ring  --i=p
  exfalso;expose_names;apply lt_irrefl i_1;exact (lt_of_le_of_lt h_ki h_1.1)
  expose_names;simp only [id_eqzero _ _ h];ring
  simp
  sorry

end PrimaryTransformation