Sum of sum of ite simplifies to sum

Stream: maths

[Mark Andrew Gerads]

import all
-- import RootOfUnityExponentialSum

open classical complex asymptotics real normed_space finset
open_locale classical big_operators nat

-----------
-- This section is properly defined without any sorry elsewhere.

def ruesDiff : ℕ → ℤ → ℂ → ℂ := sorry

lemma ruesDiffMPeriodic2 (n : ℕ) (m k : ℤ) (z : ℂ) : ruesDiff n m z = ruesDiff n (m + k * n) z := sorry

-----------
-- The following needs help.


lemma ruesDiffArgumentSumRule4 (n : ℕ) (h : 0 < n) (m : ℤ) (z₀ z₁ : ℂ) :
        ∑ (x : ℕ) in range n, ∑ (x_1 : ℕ) in range n, ite ((n : ℤ) ∣ ↑m - ↑x - ↑x_1) (ruesDiff n ↑x z₀ * ruesDiff n ↑x_1 z₁) 0 =
  ∑ (k : ℕ) in range n, ruesDiff n (m + ↑k) z₀ * ruesDiff n (↑n - ↑k) z₁ :=
begin
  sorry,
end

-- The following is example code for the case m=0. I do not understand it well enough to generalize it.
-- Help received from https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Diagonal.20sum.20simplification.20request.2E
lemma diagonalSumSimp2 (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

[Yury G. Kudryashov]

Let me repeat my question: why don't you use docs#pnat for n and zmod n for k in ruesDiff n k z?

[Yury G. Kudryashov]

Then you write your "divisibility" conditions as equalities in zmod n

[Mark Andrew Gerads]

I think you are right that using pnat would be better, and probably right about zmod being better. I just built my project in an inefficient way, using a very small subset of mathlib because that's all I know thus far.

[Yury G. Kudryashov]

What's your math background?

[Mark Andrew Gerads]

I studied 2.5 years undergrad, double majoring in Mathematics and Computer Science, before I dropped out of college. Math has been a relatively consistent hobby for me. I'm going back to college but will focus on Computer Science this time.

[Mark Andrew Gerads]

I just tried converting all the appropriate nat variables to pnat variables, but it is surprisingly difficult to change everything without breaking proofs. I plan to eventually be coding in Lean4, at which point I plan to rewrite my RootOfUnityExponentialSum project with PNat variables.