tsum stretcher, adding zeroes to sums like this

Stream: Is there code for X?

[Mark Gerads]

import all

lemma needZeroCoeff (f:ℕ→ℂ) (n:ℕ) (h:n>0) : ∑' (k : ℕ), f (n * k) = ∑' (k : ℕ), ite (n ∣ k) (f k) 0 :=
begin
  sorry,
end

One part of my proof needs plenty of zero coefficients, yet it needs to be shown equivalent to the nice version without zero coefficients.

[Damiano Testa]

This works:

import analysis.complex.basic

/-  A more general version. -/
lemma tsum_mul_ite {α} [topological_space α] [t2_space α] [add_comm_monoid α]
  (f : ℕ → α) {n : ℕ} (h : 0 < n) :
  ∑' (k : ℕ), f (n * k) = ∑' (k : ℕ), ite (n ∣ k) (f k) 0 :=
begin
  rw [(show ∑' (c : ℕ), f (n * c) = ∑' (a : set.range ((*) n)), f ↑a, from
    (equiv.of_injective ((*) n) (nat.mul_right_injective h)).tsum_eq (λ a, f a.val)), tsum_subtype],
  exact tsum_congr (λ a, by simp [set.indicator, has_dvd.dvd, eq_comm]),
end

lemma needZeroCoeff (f:ℕ→ℂ) (n:ℕ) (h : n>0) : ∑' (k : ℕ), f (n * k) = ∑' (k : ℕ), ite (n ∣ k) (f k) 0 :=
tsum_mul_ite _ h

[Mark Gerads]

That should have finished off my proof of ruesDiffM0EqRues, a required step to proving ruesNEqExpSum, but Lean is not accepting this, probably because I have (↑n ∣ ↑k) instead of (n ∣ k). How can this be rewritten to match?

import all

open classical complex real normed_space
open_locale classical big_operators nat

lemma expTsumForm (z:ℂ) : exp z = tsum (λ (k:ℕ), z ^ k / k.factorial):=
begin
  rw [exp_eq_exp_ℂ, exp_eq_tsum_div],
end

-- 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)

-- The zero coefficients are needed for proof of ruesNEqExpSum
-- m=0 is same as rues, ruesDiff is the mth derivative of rues
noncomputable
def ruesDiff (n:ℕ) (m:ℤ) (z:ℂ) : ℂ :=
  tsum (λ (k:ℕ), if ((k:ℤ)+m)%n=0 then z ^ k / k.factorial else 0)

lemma tsum_mul_ite {α} [topological_space α] [t2_space α] [add_comm_monoid α]
  (f : ℕ → α) {n : ℕ} (h : 0 < n) :
  ∑' (k : ℕ), f (n * k) = ∑' (k : ℕ), ite (n ∣ k) (f k) 0 :=
begin
  rw [(show ∑' (c : ℕ), f (n * c) = ∑' (a : set.range ((*) n)), f ↑a, from
    (equiv.of_injective ((*) n) (nat.mul_right_injective h)).tsum_eq (λ a, f a.val)), tsum_subtype],
  exact tsum_congr (λ a, by simp [set.indicator, has_dvd.dvd, eq_comm]),
end

lemma needZeroCoeff (f:ℕ→ℂ) (n:ℕ) (h : n>0) : ∑' (k : ℕ), f (n * k) = ∑' (k : ℕ), ite (n ∣ k) (f k) 0 :=
tsum_mul_ite _ h

lemma ruesDiffM0EqRues (n:ℕ) (h:n>0) (z:ℂ) : rues n z = ruesDiff n 0 z :=
begin
  rw [rues, ruesDiff],
  simp,
  sorry,
end

open finset

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

lemma rues1EqExp (z:ℂ) : rues 1 z = exp z :=
begin
  rw [expTsumForm z, rues],
  simp,
end

lemma rues2EqCosh (z:ℂ) : rues 2 z = cosh z :=
begin
  rw [complex.cosh, ruesNEqExpSum],
  rw finset.sum,
  simp only [range_coe, multiset.range_succ, multiset.range_zero, nat.cast_bit0, nat.cast_one, multiset.map_cons, mul_one,
    nat.cast_zero, mul_zero, zero_mul, zero_div, complex.exp_zero, multiset.map_zero, multiset.sum_cons,
    multiset.sum_zero, add_zero],
  have h : 2 * I * ↑real.pi / 2 = ↑real.pi * I,
  ring,
  rw h,
  simp only [exp_pi_mul_I, mul_neg, mul_one],
  ring,
  norm_num,
end

lemma rues4EqCoshCosh (z:ℂ) : rues 4 z = cosh (z/(1+I)) * cosh (z/(1-I)) :=
begin
  rw [complex.cosh, complex.cosh, ruesNEqExpSum],
  rw finset.sum,
  simp,
  sorry,
  norm_num,
end

Also, tsum_mul_ite should probably be added to mathlib.

[Mark Gerads]

I am aware int.coe_nat_dvd.symm is what I need, but I haven't been able to get it working so far.

[Kevin Buzzard]

My machine cannot handle the import all. Can you repost with more reasonable imports?

[Kevin Buzzard]

Sorry i take that back, my mathlib is borked. I think I'm a victim of some earlier problem.

[Kevin Buzzard]

lemma ruesDiffM0EqRues_first_try (n:ℕ) (h:n>0) (z:ℂ) : rues n z = ruesDiff n 0 z :=
begin
  rw [rues, ruesDiff],
  simp, -- nontermal simps are bad; squeeze it to see the names of what you're using, you might learn something
  -- Let's isolate the problem
  convert needZeroCoeff (λ n, z ^ n / n!) n h,
  ext1, -- cancel lambdas
  congr' 1, -- cancel ITEs
  apply propext, -- make equality of propositions into an iff
  -- the problem is now isolated. Now let's solve it
  exact int.coe_nat_dvd, -- library_search found it (and might have found it quicker had
  -- you not done `import all` but I'm not sure)
end

-- second go now we know the name of the lemma
lemma ruesDiffM0EqRues (n:ℕ) (h:n>0) (z:ℂ) : rues n z = ruesDiff n 0 z :=
begin
  simp only [rues, ruesDiff, add_zero, euclidean_domain.mod_eq_zero,
    int.coe_nat_dvd, needZeroCoeff (λ n, z ^ n / n!) n h],
end

[Mark Gerads]

Thanks. I suppose it would be nice if there was something like 'squeeze imports' that would change 'import all' to specific imports for sharing minimal working examples. I do wonder how much 'import all' impacts usability though; it seems fine to me.

[Alex J. Best]

There are some import squeezing tools, but unfortunately they are not yet in mathlib, so are a bit harder to utilize

[Damiano Testa]

What I manually do is

• comment out an import and see what lemma no longer exists;
• put the import back, peek at the definition of the broken lemma;
• add the import of this new file;
• repeat.

The number of iterations of the above process is usually fairly small.