Theorem: partialFourierSum_sub (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 only [Pi.sub_apply]
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 x - 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 x - partialFourierSum g N x
Tactic:
rw [partialFourierSum, partialFourierSum, partialFourierSum, ←sum_sub_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 : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos (f - g) n * (fourier n) ↑x =
    ∑ x_1 ∈ Icc (-Int.ofNat N) ↑N,
      (fourierCoeffOn Real.two_pi_pos f x_1 * (fourier x_1) ↑x -
        fourierCoeffOn Real.two_pi_pos g x_1 * (fourier x_1) ↑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 : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos (f - g) n * (fourier n) ↑x =
    ∑ x_1 ∈ Icc (-Int.ofNat N) ↑N,
      (fourierCoeffOn Real.two_pi_pos f x_1 * (fourier x_1) ↑x -
        fourierCoeffOn Real.two_pi_pos g x_1 * (fourier x_1) ↑x)
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 n => fourierCoeffOn Real.two_pi_pos (f - g) n * (fourier n) ↑x) = fun x_1 =>
    fourierCoeffOn Real.two_pi_pos f x_1 * (fourier x_1) ↑x - fourierCoeffOn Real.two_pi_pos g x_1 * (fourier x_1) ↑x

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 n => fourierCoeffOn Real.two_pi_pos (f - g) n * (fourier n) ↑x) = fun x_1 =>
    fourierCoeffOn Real.two_pi_pos f x_1 * (fourier x_1) ↑x - fourierCoeffOn Real.two_pi_pos g x_1 * (fourier x_1) ↑x
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 * (fourier n) ↑x =
    fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x - fourierCoeffOn Real.two_pi_pos g n * (fourier n) ↑x

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 * (fourier n) ↑x =
    fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x - fourierCoeffOn Real.two_pi_pos g n * (fourier n) ↑x
Tactic:
rw [fourierCoeffOn_sub hf hg, sub_mul]
State after:
no goals