Splitting a complex summable tsum into real and imaginary

Stream: Is there code for X?

[Mark Gerads]

Is imagPartsOfSumEqSumOfImagParts in the library somewhere? I would like proof so I can get closer to proving ruesRealToReal. If you have insight into the other 2 sorries, that would also be nice.

import all

open classical complex real topological_space

open_locale topological_space big_operators


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

lemma ruesSummable (n:ℕ) (z:ℂ) : summable (λ (k:ℕ), z ^ (n*k) / (n*k).factorial):=
begin
  rw [summable],
  sorry,
end

lemma imagPartsOfSumEqSumOfImagParts (f:ℕ→ℂ) (hf:summable f):
      im (∑' (k : ℕ), f k) = (∑' (k : ℕ), im (f k)):=
begin
  sorry,
end

lemma ruesRealToReal (n:ℕ) (h:n>0) (x:ℝ) : (rues n x).im = 0 :=
begin
  rw [rues, imagPartsOfSumEqSumOfImagParts],
  {
    suffices h : ∑' (k : ℕ), im (↑x ^ (n * k) / ↑(n * k)!) = ∑' (k : ℕ), 0,
    simp only [tsum_zero, h],
    congr' 1,
    ext1,
    sorry,
  },
  exact ruesSummable n x,
end

[Ruben Van de Velde]

Is it true? What if the real part diverges and the imaginary part converges to something nonzero?

[Eric Wieser]

docs#continuous_linear_map.map_tsum?

[Eric Wieser]

Combined with docs#complex.im_clm

[Mark Gerads]

@Ruben Van de Velde If that were the case, then the sum does not converge in ℂ. I have (f:ℕ→ℂ) (hf:summable f).

[Eric Wieser]

Then the above should work

[Mark Gerads]

I'm trying.

[Mark Gerads]

I got it.

lemma imagPartsOfSumEqSumOfImagParts (f:ℕ→ℂ) (hf:summable f):
      im (∑' (k : ℕ), f k) = (∑' (k : ℕ), im (f k)):=
begin
  let h:= continuous_linear_map.map_tsum complex.im_clm hf,
  continuity,
end

[Eric Wieser]

I suspect you can remove everything from the begin to the := (inclusive), and everything after the first cons

[Eric Wieser]

You might want to look at #naming too; while it wouldn't have helped you here, following the rules for naming can often lead to finding an existing lemma.

[Eric Wieser]

That would be called complex.im_tsum I think