A sum of a sum equal to a sum

Stream: mathlib4

[Mark Andrew Gerads]

Please help, and thanks for the help in advance.

import Mathlib

opaque RuesDiff : ℕ → ℤ → ℂ → ℂ -- defined elsewhere

lemma RuesDiffMPeriodic (n : ℕ+) (m k : ℤ) : RuesDiff n m = RuesDiff n (m + k * n) := by
  sorry -- proved elsewhere but needed to prove DesiredLemma

lemma DesiredLemma (n : ℕ+) (m : ℤ) (z₀ z₁ : ℂ) : (∑ i : Fin ↑n, ∑ i_1 : Fin ↑n, if ↑↑n ∣ m - ↑↑i - ↑↑i_1 then RuesDiff n (↑↑i) z₀ * RuesDiff n (↑↑i_1) z₁ * ↑↑n else 0) / ↑↑n =
  ∑ k : Fin ↑n, RuesDiff n (↑↑k) z₀ * RuesDiff n (m - ↑↑k) z₁ := by
  sorry -- needed to complete lemma RuesDiffArgumentSumRule at https://github.com/Nazgand/NazgandLean4/blob/master/NazgandLean4/RootOfUnityExponentialSum.lean

For reference, here is some Lean 3 code that does almost the same thing. I got stuck trying to translate the code at the part with the change command, where Fin is somehow replaced with ZMod.

-- Help received from https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Diagonal.20sum.20simplification.20request.2E
lemma diagonalSumSimp (n : ℕ) (h : 0 < n) (z₀ z₁: ℂ) :
  (∑ k in range n, ∑ l in range n,
    if (n : ℤ) ∣ -k - l then (ruesDiff n k z₀ * ruesDiff n l z₁) else 0) =
  ∑ k in range n, (ruesDiff n (n - k) z₁ * ruesDiff n k z₀) :=
begin
  rcases nat.exists_eq_succ_of_ne_zero h.ne' with ⟨n, rfl⟩,
  have h₀ : ∀ k l : fin (n + 1), (↑(n + 1) : ℤ) ∣ -(k : ℕ) -(l : ℕ) ↔ l = -k,
  { change ∀ k l : zmod (n + 1), (↑(n + 1) : ℤ) ∣ -(k.val : ℕ) -(l.val : ℕ) ↔ l = -k,
    intros k l,
    rw [← zmod.int_coe_zmod_eq_zero_iff_dvd, ← neg_add', int.cast_neg, neg_eq_zero,
      eq_neg_iff_add_eq_zero, add_comm l],
    push_cast [zmod.nat_cast_zmod_val] },
  simp only [sum_range, h₀, sum_ite_eq', mem_univ, if_true],
  refine sum_congr rfl (λ k _, _),
  rw [mul_comm],
  congr' 1,
  rcases eq_or_ne k 0 with rfl | hk,
  { simpa using ruesDiffMPeriodic2 (n + 1) 0 1 z₁ },
  { simp only [fin.coe_neg, nat.add],
    rw [nat.mod_eq_of_lt, nat.cast_sub],
    exacts [k.2.le, tsub_lt_self n.succ_pos (pos_iff_ne_zero.2 $ mt (fin.coe_eq_coe k 0).1 hk)] }
end

[Yaël Dillies]

(This belongs in #Is there code for X? or #mathlib4, not in #lean4)

[Mark Andrew Gerads]

Well, I doubt there is code for it, seeing as RuesDiff was defined by me in a personal project. Also, I wasn't planning to contribute it to Mathlib4 because I thought it was too esoteric. Perhaps I should move it to the #maths channel? Looks like I don't have permission to move messages.

[Yaël Dillies]

No, "X" in your "Is-there-code-for-X" question should be taken as "the lemma above with RuesDiff replaced by a general periodic function"

[Yaël Dillies]

It does not belong in #maths

[Mark Andrew Gerads]

I suppose if this were in Mathlib, it would need to be generalized so that complex numbers should be replaced with a AddCommMonoid type.

[Mark Andrew Gerads]

I thought of using suffices instead of change, but I still do not see how to use ZMod n lemmas with Fin n or replace Fin n with ZMod n.

lemma DesiredLemma (n : ℕ+) (m : ℤ) (z₀ z₁ : ℂ) : (∑ i : Fin ↑n, ∑ i_1 : Fin ↑n, if ↑↑n ∣ m - ↑↑i - ↑↑i_1 then RuesDiff n (↑↑i) z₀ * RuesDiff n (↑↑i_1) z₁ * ↑↑n else 0) / ↑↑n =
  ∑ k : Fin ↑n, RuesDiff n (↑↑k) z₀ * RuesDiff n (m - ↑↑k) z₁ := by
  have h₃ : ∀ (i i_1 : Fin n), ↑↑n ∣ m - ↑↑i - ↑↑i_1 ↔ i_1 = (m : Fin n) - i := by
    suffices h₄ : ∀ (i i_1 : ZMod n), ↑↑n ∣ m - (i.val : ℤ) - (i_1.val : ℤ) ↔ i_1 = (m : ZMod n) - i
    · intros i i_1
      -- neither norm_cast or mod_cast work
      sorry
    · sorry
  sorry

[Notification Bot]

This topic was moved here from #lean4 > A sum of a sum equal to a sum by Mario Carneiro.