Commuting sum sigmas with a sum of sum of sum

Stream: maths

[Mark Andrew Gerads]

image.png
I have a triple sum I need to rearrange:

∑ (x : ℕ) in
  range n,
  ∑ (x_1 : ℕ) in
    range n,
    ∑ (x_2 : ℕ) in
      range n,
      ruesDiff n ↑x_1 z₀ * ruesDiff n ↑x_2 z₁ * exp (2 * ↑real.pi * (↑x / ↑n) * I) ^ (-↑x_1 + -↑x_2)

needs to become

∑ (x_1 : ℕ) in
  range n,
  ∑ (x_2 : ℕ) in
    range n,
    ∑ (x : ℕ) in
      range n,
      ruesDiff n ↑x_1 z₀ * ruesDiff n ↑x_2 z₁ * exp (2 * ↑real.pi * (↑x / ↑n) * I) ^ (-↑x_1 + -↑x_2)

docs#finset.sum_comm seems to be the key, yet I do not know how to use it to rewrite only the part needed to be rewritten.
Here is my #MWE, where I am working on ruesArgumentSumRule:

import analysis.special_functions.trigonometric.basic
import analysis.special_functions.exponential
import analysis.special_functions.complex.log
import algebra.group_with_zero.defs
import algebra.big_operators.basic

open classical complex asymptotics real normed_space
open_locale classical big_operators nat

-- rues is the Root of Unity Exponential Sum function
-- inspired by the relationship between exp and cosh
noncomputable
def rues (n:ℕ) (z:ℂ) : ℂ :=
  tsum (λ (k:ℕ), z ^ (n*k) / (n*k).factorial)

def ruesDiff (n : ℕ) (m : ℤ) : ℂ → ℂ := sorry

lemma rouNot0 (n:ℕ) (h₀:0<n) (rou:ℂ) (h₁:rou ^ n = 1) : rou ≠ 0 := sorry

lemma ruesDiffRotationallySymmetric (n:ℕ) (h₀:0<n) (m:ℤ) (z rou:ℂ) (h₁:rou ^ n = 1) : ruesDiff n m (z * rou) = rou ^ -m * ruesDiff n m z :=
  sorry

open finset

lemma ruesNEqExpSum (n:ℕ) (h:0<n) (z:ℂ) :
    rues n z = (∑ m in range n, exp (z * exp (2 * real.pi * (m / n) * I)))/n := sorry

lemma expSumOfRuesDiff (k:ℕ) (h:0<k) (z:ℂ) : exp z = ∑ k₀ in range k, ruesDiff k k₀ z:= sorry

lemma ruesArgumentSumRule (n:ℕ) (h:0<n) (z₀ z₁:ℂ) :
        rues n (z₀ + z₁) = ∑ k in range n, (ruesDiff n k z₀ * ruesDiff n (n - k) z₁) :=
begin
  rw ruesNEqExpSum n h _,
  have h0 : ∀ (m : ℕ), (z₀ + z₁) * exp (2 * ↑real.pi * (↑m / ↑n) * I) =
    z₀ * exp (2 * ↑real.pi * (↑m / ↑n) * I) +
    z₁ * exp (2 * ↑real.pi * (↑m / ↑n) * I),
  {
    intros m,
    ring_nf,
  },
  simp_rw h0,
  clear h0,
  simp_rw complex.exp_add,
  have h1 : ∀ (x : ℕ), exp (z₀ * exp (2 * ↑real.pi * (↑x / ↑n) * I)) =
    ∑ (k₀ : ℕ) in range n, ruesDiff n ↑k₀ (z₀ * exp (2 * ↑real.pi * (↑x / ↑n) * I)),
  {
    intros x,
    exact expSumOfRuesDiff n h (z₀ * complex.exp ((2:ℂ) * (real.pi:ℂ) * ((x:ℂ) / (n:ℂ)) * I)),
  },
  simp_rw h1,
  clear h1,
  have h2 : ∀ (x : ℕ), exp (z₁ * exp (2 * ↑real.pi * (↑x / ↑n) * I)) =
    ∑ (k₀ : ℕ) in range n, ruesDiff n ↑k₀ (z₁ * exp (2 * ↑real.pi * (↑x / ↑n) * I)),
  {
    intros x,
    exact expSumOfRuesDiff n h (z₁ * complex.exp ((2:ℂ) * (real.pi:ℂ) * ((x:ℂ) / (n:ℂ)) * I)),
  },
  simp_rw h2,
  clear h2,
  have h3 : ∀ (x:ℕ), exp (2 * ↑real.pi * (↑x / ↑n) * I) ^ n = 1,
  {
    intros x,
    rw (complex.exp_nat_mul _ n).symm,
    rw complex.exp_eq_one_iff,
    use (x:ℤ),
    have h4 : 0 ≠ n,
    exact ne_of_lt h,
    have h5 : (n:ℂ) ≠ 0,
    exact_mod_cast h4.symm,
    field_simp,
    ring_nf,
  },
  have h6 : ∀ (k₀ x : ℕ) (z : ℂ), ruesDiff n ↑k₀ (z * exp (2 * ↑real.pi * (↑x / ↑n) * I)) =
    exp (2 * ↑real.pi * (↑x / ↑n) * I) ^ -↑k₀ * ruesDiff n ↑k₀ z,
  {
    intros k₀ x z,
    exact ruesDiffRotationallySymmetric n h k₀ z (exp (2 * ↑real.pi * (↑x / ↑n) * I)) (h3 x),
  },
  simp_rw h6 _ _ _,
  clear h6,
  simp_rw [finset.sum_mul, finset.mul_sum],
  have h7 : ∀ (x x_1 x_2 : ℕ), exp (2 * ↑real.pi * ((x:ℂ) / (n:ℂ)) * I) ^ -(x_1:ℤ) * ruesDiff n x_1 z₀ *
  (exp (2 * ↑real.pi * ((x:ℂ) / (n:ℂ)) * I) ^ -(x_2:ℤ) * ruesDiff n x_2 z₁) =
  ruesDiff n x_1 z₀ * ruesDiff n x_2 z₁ * (exp (2 * ↑real.pi * ((x:ℂ) / (n:ℂ)) * I) ^ -(x_1:ℤ) *
  exp (2 * ↑real.pi * ((x:ℂ) / (n:ℂ)) * I) ^ -(x_2:ℤ)),
  {
    intros x x_1 x_2,
    ring_nf,
  },
  simp_rw h7,
  clear h7,
  have h8 : ∀ (x x_1 x_2 : ℕ), exp (2 * ↑real.pi * ((x:ℂ) / (n:ℂ)) * I) ^ -(x_1:ℤ) * exp (2 * ↑real.pi * ((x:ℂ) / (n:ℂ)) * I) ^ -(x_2:ℤ) =
  exp (2 * ↑real.pi * ((x:ℂ) / (n:ℂ)) * I) ^ (-(x_1:ℤ) + -(x_2:ℤ)),
  {
    intros x x_1 x_2,
    have h9 : exp (2 * ↑real.pi * ((x:ℂ) / (n:ℂ)) * I) ≠ 0,
    {
      exact rouNot0 n h (exp (2 * ↑real.pi * (↑x / ↑n) * I)) (h3 x),
    },
    exact (zpow_add₀ h9 (-(x_1:ℤ)) (-(x_2:ℤ))).symm,
  },
  simp_rw h8,
  clear h8,
  -- simp_rw finset.sum_comm, -- seems to be stuck in an infinite loop? Taking way to long.
  sorry,
end

[Mark Andrew Gerads]

I was thinking this would be easy if I had a command like simp_rw_nth with would act like simp_rw, except it only rewrites the nth rewritable term.

[Kevin Buzzard]

This proof takes a really long time to compile. Lean likes you much better if you refactor out as much as you can -- many small lemmas is much much better than one big theorem. For example it's quite bad style to do things like proving h3 in the middle of your proof -- this is just an independent result which could be factored out, you shouldn't be proving it in the middle of some other proof just because you realised you needed it in the middle of the other proof.

[Kevin Buzzard]

To do the targetted rewrite you can do simp_rw @finset.sum_comm _ _ _ _ _ _ (λ g a, ...) (sorry, need to go, the art is to fill in the ...)

[Eric Wieser]

I think it's pretty clear that finset.sum_comm should be changed to take explicit arguments...