Problem with rw

Stream: new members

[Julia Ramos Alves]

Dear all, I have a problem with the following code:

import analysis.fourier
import measure_theory.integral.interval_integral
import data.real.basic
import analysis.special_functions.integrals

lemma split_tsum (f : ℤ → ℂ) (hf : summable f): ∑' x, f x =
  f 0 + (∑' (x : ℕ), f (x+1)) + (∑' (x : ℕ), f (-x-1)) :=
begin
  sorry,
end

noncomputable
def fourier_coeff (f : ℝ → ℂ) (n : ℤ) : ℂ :=
(2 * real.pi)⁻¹ * ∫ x in -real.pi .. real.pi, (f x) * complex.exp (-complex.I * n * x)

lemma lhs (x: ℝ)(f : ℝ → ℂ)(hf: f x = x)(n : ℤ)(g: ℤ → ℂ)
(hg: g n = (complex.abs (fourier_coeff f n))^2):
1/2 * ∑' (n : ℤ), g n = ∑' (n:ℕ) , 1 / ((n+1)^2) :=
begin
  rw split_tsum,
  rw hg,
end

And I think it's because the rw tactic is trying to replace only for the occurrence of n and not of any integer. Am I correct? And, in any case, how do I fix this issue?

[Kevin Buzzard]

Yes that sounds right: your lemma right now says that n is some integer and that g(n)=|fhat(n)|^2. If that's not what you want to say then the fix it to say what you want to say. What do you want to say? Here's a suggestion but I don't know if it's what you want.

lemma lhs (x: ℝ)(f : ℝ → ℂ)(hf: f x = x) (g: ℤ → ℂ)
(hg: ∀ n, g n = (complex.abs (fourier_coeff f n))^2):
1/2 * ∑' (n : ℤ), g n = ∑' (n:ℕ) , 1 / ((n+1)^2) :=
begin
  rw split_tsum,
  rw hg,
end

[Julia Ramos Alves]

That suggestion actually fits my intention perfectly, thank you.