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

State before:
f : ℝ → ℂ
N : ℕ
⊢ Function.Periodic (partialFourierSum f N) (2 * Real.pi)
Tactic:
rw [Function.Periodic]
State after:
f : ℝ → ℂ
N : ℕ
⊢ ∀ (x : ℝ), partialFourierSum f N (x + 2 * Real.pi) = partialFourierSum f N x

State before:
f : ℝ → ℂ
N : ℕ
⊢ ∀ (x : ℝ), partialFourierSum f N (x + 2 * Real.pi) = partialFourierSum f N x
Tactic:
intro x
State after:
f : ℝ → ℂ
N : ℕ
x : ℝ
⊢ partialFourierSum f N (x + 2 * Real.pi) = partialFourierSum f N x

State before:
f : ℝ → ℂ
N : ℕ
x : ℝ
⊢ partialFourierSum f N (x + 2 * Real.pi) = partialFourierSum f N x
Tactic:
rw [partialFourierSum, partialFourierSum]
State after:
f : ℝ → ℂ
N : ℕ
x : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑(x + 2 * Real.pi) =
    ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x

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

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

State before:
case e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑(x + 2 * Real.pi) =
    fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x
Tactic:
congr 1
State after:
case e_f.h.e_a
f : ℝ → ℂ
N : ℕ
x : ℝ
n : ℤ
⊢ (fourier n) ↑(x + 2 * Real.pi) = (fourier n) ↑x

State before:
case e_f.h.e_a
f : ℝ → ℂ
N : ℕ
x : ℝ
n : ℤ
⊢ (fourier n) ↑(x + 2 * Real.pi) = (fourier n) ↑x
Tactic:
exact fourier_periodic x
State after:
no goals