Zulip Chat Archive
Stream: maths
Topic: Commuting sum sigmas with a sum of sum of sum
Mark Andrew Gerads (Oct 17 2022 at 19:57):
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 (Oct 17 2022 at 20:02):
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 (Oct 17 2022 at 20:22):
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 (Oct 17 2022 at 20:25):
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 (Oct 17 2022 at 21:14):
I think it's pretty clear that finset.sum_comm
should be changed to take explicit arguments...
Last updated: Dec 20 2023 at 11:08 UTC