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

State before:
f : ℝ → ℂ
a : ℂ
N : ℕ
⊢ partialFourierSum (fun x => a * f x) N = fun x => a * partialFourierSum f N x
Tactic:
ext x
State after:
case h
f : ℝ → ℂ
a : ℂ
N : ℕ
x : ℝ
⊢ partialFourierSum (fun x => a * f x) N x = a * partialFourierSum f N x

State before:
case h
f : ℝ → ℂ
a : ℂ
N : ℕ
x : ℝ
⊢ partialFourierSum (fun x => a * f x) N x = a * partialFourierSum f N x
Tactic:
rw [partialFourierSum, partialFourierSum, mul_sum]
State after:
case h
f : ℝ → ℂ
a : ℂ
N : ℕ
x : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos (fun x => a * f x) n * (fourier n) ↑x =
    ∑ i ∈ Icc (-Int.ofNat N) ↑N, a * (fourierCoeffOn Real.two_pi_pos f i * (fourier i) ↑x)

State before:
case h
f : ℝ → ℂ
a : ℂ
N : ℕ
x : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos (fun x => a * f x) n * (fourier n) ↑x =
    ∑ i ∈ Icc (-Int.ofNat N) ↑N, a * (fourierCoeffOn Real.two_pi_pos f i * (fourier i) ↑x)
Tactic:
congr
State after:
case h.e_f
f : ℝ → ℂ
a : ℂ
N : ℕ
x : ℝ
⊢ (fun n => fourierCoeffOn Real.two_pi_pos (fun x => a * f x) n * (fourier n) ↑x) = fun i =>
    a * (fourierCoeffOn Real.two_pi_pos f i * (fourier i) ↑x)

State before:
case h.e_f
f : ℝ → ℂ
a : ℂ
N : ℕ
x : ℝ
⊢ (fun n => fourierCoeffOn Real.two_pi_pos (fun x => a * f x) n * (fourier n) ↑x) = fun i =>
    a * (fourierCoeffOn Real.two_pi_pos f i * (fourier i) ↑x)
Tactic:
ext n
State after:
case h.e_f.h
f : ℝ → ℂ
a : ℂ
N : ℕ
x : ℝ
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos (fun x => a * f x) n * (fourier n) ↑x =
    a * (fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x)

State before:
case h.e_f.h
f : ℝ → ℂ
a : ℂ
N : ℕ
x : ℝ
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos (fun x => a * f x) n * (fourier n) ↑x =
    a * (fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x)
Tactic:
rw [fourierCoeffOn_mul, mul_assoc]
State after:
no goals