Theorem: partialFourierSum_add (Carleson/Theorem1_1/Basic.lean)

State before:
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
⊢ partialFourierSum (f + g) N = partialFourierSum f N + partialFourierSum g N
Tactic:
ext x
State after:
case h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ partialFourierSum (f + g) N x = (partialFourierSum f N + partialFourierSum g N) x

State before:
case h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ partialFourierSum (f + g) N x = (partialFourierSum f N + partialFourierSum g N) x
Tactic:
simp [partialFourierSum, partialFourierSum, partialFourierSum, ← sum_add_distrib]
State after:
case h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ ∑ x_1 ∈ Icc (-↑N) ↑N,
      fourierCoeffOn Real.two_pi_pos (f + g) x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp =
    ∑ x_1 ∈ Icc (-↑N) ↑N,
      (fourierCoeffOn Real.two_pi_pos f x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp +
        fourierCoeffOn Real.two_pi_pos g x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp)

State before:
case h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ ∑ x_1 ∈ Icc (-↑N) ↑N,
      fourierCoeffOn Real.two_pi_pos (f + g) x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp =
    ∑ x_1 ∈ Icc (-↑N) ↑N,
      (fourierCoeffOn Real.two_pi_pos f x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp +
        fourierCoeffOn Real.two_pi_pos g x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp)
Tactic:
congr
State after:
case h.e_f
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ (fun x_1 =>
      fourierCoeffOn Real.two_pi_pos (f + g) x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp) =
    fun x_1 =>
    fourierCoeffOn Real.two_pi_pos f x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp +
      fourierCoeffOn Real.two_pi_pos g x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp

State before:
case h.e_f
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
⊢ (fun x_1 =>
      fourierCoeffOn Real.two_pi_pos (f + g) x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp) =
    fun x_1 =>
    fourierCoeffOn Real.two_pi_pos f x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp +
      fourierCoeffOn Real.two_pi_pos g x_1 * (2 * ↑Real.pi * Complex.I * ↑x_1 * ↑x / (2 * ↑Real.pi)).exp
Tactic:
ext n
State after:
case h.e_f.h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos (f + g) n * (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp =
    fourierCoeffOn Real.two_pi_pos f n * (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp +
      fourierCoeffOn Real.two_pi_pos g n * (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp

State before:
case h.e_f.h
f g : ℝ → ℂ
N : ℕ
hf : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
hg : IntervalIntegrable g MeasureTheory.volume 0 (2 * Real.pi)
x : ℝ
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos (f + g) n * (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp =
    fourierCoeffOn Real.two_pi_pos f n * (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp +
      fourierCoeffOn Real.two_pi_pos g n * (2 * ↑Real.pi * Complex.I * ↑n * ↑x / (2 * ↑Real.pi)).exp
Tactic:
rw [fourierCoeffOn_add hf hg, add_mul]
State after:
no goals