Theorem: partialFourierSum_eq_conv_dirichletKernel (Carleson/Theorem1_1/Dirichlet_kernel.lean)

State before:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ partialFourierSum f N x = 1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel N (x - y)
Tactic:
calc partialFourierSum f N x
  _ = ∑ n in Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x := by
    rw [partialFourierSum]
  _ = ∑ n in Icc (-Int.ofNat N) ↑N, (1 / (2 * Real.pi - 0)) • ((∫ (y : ℝ) in (0 : ℝ)..2 * Real.pi, (fourier (-n) ↑y • f y)) * (fourier n) ↑x) := by
    congr 1
    ext n
    rw [fourierCoeffOn_eq_integral, smul_mul_assoc]
  _ = (1 / (2 * Real.pi)) * ∑ n in Icc (-Int.ofNat N) ↑N, ((∫ (y : ℝ) in (0 : ℝ)..2 * Real.pi, (fourier (-n) ↑y • f y)) * (fourier n) ↑x) := by
    rw [← smul_sum, real_smul, sub_zero]
    norm_cast
  _ = (1 / (2 * Real.pi)) * ∑ n in Icc (-Int.ofNat N) ↑N, ((∫ (y : ℝ) in (0 : ℝ)..2 * Real.pi, (fourier (-n) ↑y • f y) * (fourier n) ↑x)) := by
    congr
    ext n
    symm
    apply intervalIntegral.integral_mul_const
  _ = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), ∑ n in Icc (-Int.ofNat N) ↑N, (fourier (-n)) y • f y * (fourier n) x := by
    rw [← intervalIntegral.integral_finset_sum]
    intro n _
    apply IntervalIntegrable.mul_const
    apply IntervalIntegrable.continuousOn_mul h fourier_uniformContinuous.continuous.continuousOn
  _ = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * ∑ n in Icc (-Int.ofNat N) ↑N, (fourier (-n)) y * (fourier n) x := by
    congr
    ext y
    rw [mul_sum]
    congr
    ext n
    rw [smul_eq_mul]
    ring
  _ = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel N (x - y) := by
    congr
    ext y
    rw [dirichletKernel]
    congr
    ext n
    rw [fourier_coe_apply, fourier_coe_apply, fourier_coe_apply, ←exp_add]
    congr
    field_simp
    rw [mul_sub, sub_eq_neg_add]
State after:
no goals

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

State before:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x =
    ∑ n ∈ Icc (-Int.ofNat N) ↑N,
      (1 / (2 * Real.pi - 0)) • ((∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y) * (fourier n) ↑x)
Tactic:
congr 1
State after:
case e_f
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ (fun n => fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x) = fun n =>
    (1 / (2 * Real.pi - 0)) • ((∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y) * (fourier n) ↑x)

State before:
case e_f
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ (fun n => fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x) = fun n =>
    (1 / (2 * Real.pi - 0)) • ((∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y) * (fourier n) ↑x)
Tactic:
ext n
State after:
case e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x =
    (1 / (2 * Real.pi - 0)) • ((∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y) * (fourier n) ↑x)

State before:
case e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
n : ℤ
⊢ fourierCoeffOn Real.two_pi_pos f n * (fourier n) ↑x =
    (1 / (2 * Real.pi - 0)) • ((∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y) * (fourier n) ↑x)
Tactic:
rw [fourierCoeffOn_eq_integral, smul_mul_assoc]
State after:
no goals

State before:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N,
      (1 / (2 * Real.pi - 0)) • ((∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y) * (fourier n) ↑x) =
    1 / (2 * ↑Real.pi) *
      ∑ n ∈ Icc (-Int.ofNat N) ↑N, (∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y) * (fourier n) ↑x
Tactic:
rw [← smul_sum, real_smul, sub_zero]
State after:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ↑(1 / (2 * Real.pi)) *
      ∑ x_1 ∈ Icc (-Int.ofNat N) ↑N, (∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-x_1)) ↑y • f y) * (fourier x_1) ↑x =
    1 / (2 * ↑Real.pi) *
      ∑ n ∈ Icc (-Int.ofNat N) ↑N, (∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y) * (fourier n) ↑x

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℤ → ℝ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℤ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℤ → ℝ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℤ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℤ → ℝ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℤ → ℝ

State before:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ↑(1 / (2 * Real.pi)) *
      ∑ x_1 ∈ Icc (-Int.ofNat N) ↑N, (∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-x_1)) ↑y • f y) * (fourier x_1) ↑x =
    1 / (2 * ↑Real.pi) *
      ∑ n ∈ Icc (-Int.ofNat N) ↑N, (∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y) * (fourier n) ↑x

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℤ → ℝ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℤ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℤ → ℝ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℤ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℤ → ℝ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℤ → ℝ
Tactic:
norm_cast
State after:
no goals

State before:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ 1 / (2 * ↑Real.pi) *
      ∑ n ∈ Icc (-Int.ofNat N) ↑N, (∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y) * (fourier n) ↑x =
    1 / (2 * ↑Real.pi) *
      ∑ n ∈ Icc (-Int.ofNat N) ↑N, ∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y * (fourier n) ↑x
Tactic:
congr
State after:
case e_a.e_f
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ (fun n => (∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y) * (fourier n) ↑x) = fun n =>
    ∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y * (fourier n) ↑x

State before:
case e_a.e_f
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ (fun n => (∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y) * (fourier n) ↑x) = fun n =>
    ∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y * (fourier n) ↑x
Tactic:
ext n
State after:
case e_a.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
n : ℤ
⊢ (∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y) * (fourier n) ↑x =
    ∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y * (fourier n) ↑x

State before:
case e_a.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
n : ℤ
⊢ (∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y) * (fourier n) ↑x =
    ∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y * (fourier n) ↑x
Tactic:
symm
State after:
case e_a.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
n : ℤ
⊢ ∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y * (fourier n) ↑x =
    (∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y) * (fourier n) ↑x

State before:
case e_a.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
n : ℤ
⊢ ∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y * (fourier n) ↑x =
    (∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y) * (fourier n) ↑x
Tactic:
apply intervalIntegral.integral_mul_const
State after:
no goals

State before:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ 1 / (2 * ↑Real.pi) *
      ∑ n ∈ Icc (-Int.ofNat N) ↑N, ∫ (y : ℝ) in 0 ..2 * Real.pi, (fourier (-n)) ↑y • f y * (fourier n) ↑x =
    1 / (2 * ↑Real.pi) *
      ∫ (y : ℝ) in 0 ..2 * Real.pi, ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y • f y * (fourier n) ↑x
Tactic:
rw [← intervalIntegral.integral_finset_sum]
State after:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∀ i ∈ Icc (-Int.ofNat N) ↑N,
    IntervalIntegrable (fun y => (fourier (-i)) ↑y • f y * (fourier i) ↑x) MeasureTheory.volume 0 (2 * Real.pi)

State before:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∀ i ∈ Icc (-Int.ofNat N) ↑N,
    IntervalIntegrable (fun y => (fourier (-i)) ↑y • f y * (fourier i) ↑x) MeasureTheory.volume 0 (2 * Real.pi)
Tactic:
intro n _
State after:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
n : ℤ
a✝ : n ∈ Icc (-Int.ofNat N) ↑N
⊢ IntervalIntegrable (fun y => (fourier (-n)) ↑y • f y * (fourier n) ↑x) MeasureTheory.volume 0 (2 * Real.pi)

State before:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
n : ℤ
a✝ : n ∈ Icc (-Int.ofNat N) ↑N
⊢ IntervalIntegrable (fun y => (fourier (-n)) ↑y • f y * (fourier n) ↑x) MeasureTheory.volume 0 (2 * Real.pi)
Tactic:
apply IntervalIntegrable.mul_const
State after:
case hf
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
n : ℤ
a✝ : n ∈ Icc (-Int.ofNat N) ↑N
⊢ IntervalIntegrable (fun x => (fourier (-n)) ↑x • f x) MeasureTheory.volume 0 (2 * Real.pi)

State before:
case hf
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
n : ℤ
a✝ : n ∈ Icc (-Int.ofNat N) ↑N
⊢ IntervalIntegrable (fun x => (fourier (-n)) ↑x • f x) MeasureTheory.volume 0 (2 * Real.pi)
Tactic:
apply IntervalIntegrable.continuousOn_mul h fourier_uniformContinuous.continuous.continuousOn
State after:
no goals

State before:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ 1 / (2 * ↑Real.pi) *
      ∫ (y : ℝ) in 0 ..2 * Real.pi, ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y • f y * (fourier n) ↑x =
    1 / (2 * ↑Real.pi) *
      ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y * (fourier n) ↑x
Tactic:
congr
State after:
case e_a.e_f
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ (fun y => ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y • f y * (fourier n) ↑x) = fun y =>
    f y * ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y * (fourier n) ↑x

State before:
case e_a.e_f
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ (fun y => ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y • f y * (fourier n) ↑x) = fun y =>
    f y * ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y * (fourier n) ↑x
Tactic:
ext y
State after:
case e_a.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y • f y * (fourier n) ↑x =
    f y * ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y * (fourier n) ↑x

State before:
case e_a.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y • f y * (fourier n) ↑x =
    f y * ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y * (fourier n) ↑x
Tactic:
rw [mul_sum]
State after:
case e_a.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y • f y * (fourier n) ↑x =
    ∑ i ∈ Icc (-Int.ofNat N) ↑N, f y * ((fourier (-i)) ↑y * (fourier i) ↑x)

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ

State before:
case e_a.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y • f y * (fourier n) ↑x =
    ∑ i ∈ Icc (-Int.ofNat N) ↑N, f y * ((fourier (-i)) ↑y * (fourier i) ↑x)

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ
Tactic:
congr
State after:
case e_a.e_f.h.e_f
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
⊢ (fun n => (fourier (-n)) ↑y • f y * (fourier n) ↑x) = fun i => f y * ((fourier (-i)) ↑y * (fourier i) ↑x)

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ

State before:
case e_a.e_f.h.e_f
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
⊢ (fun n => (fourier (-n)) ↑y • f y * (fourier n) ↑x) = fun i => f y * ((fourier (-i)) ↑y * (fourier i) ↑x)

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ
Tactic:
ext n
State after:
case e_a.e_f.h.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
n : ℤ
⊢ (fourier (-n)) ↑y • f y * (fourier n) ↑x = f y * ((fourier (-n)) ↑y * (fourier n) ↑x)

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ

State before:
case e_a.e_f.h.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
n : ℤ
⊢ (fourier (-n)) ↑y • f y * (fourier n) ↑x = f y * ((fourier (-n)) ↑y * (fourier n) ↑x)

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ
Tactic:
rw [smul_eq_mul]
State after:
case e_a.e_f.h.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
n : ℤ
⊢ (fourier (-n)) ↑y * f y * (fourier n) ↑x = f y * ((fourier (-n)) ↑y * (fourier n) ↑x)

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ

State before:
case e_a.e_f.h.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
n : ℤ
⊢ (fourier (-n)) ↑y * f y * (fourier n) ↑x = f y * ((fourier (-n)) ↑y * (fourier n) ↑x)

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ

f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ℝ → ℤ → ℝ
Tactic:
ring
State after:
no goals

State before:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ 1 / (2 * ↑Real.pi) *
      ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y * (fourier n) ↑x =
    1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel N (x - y)
Tactic:
congr
State after:
case e_a.e_f
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ (fun y => f y * ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y * (fourier n) ↑x) = fun y =>
    f y * dirichletKernel N (x - y)

State before:
case e_a.e_f
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ (fun y => f y * ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y * (fourier n) ↑x) = fun y =>
    f y * dirichletKernel N (x - y)
Tactic:
ext y
State after:
case e_a.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
⊢ f y * ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y * (fourier n) ↑x = f y * dirichletKernel N (x - y)

State before:
case e_a.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
⊢ f y * ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y * (fourier n) ↑x = f y * dirichletKernel N (x - y)
Tactic:
rw [dirichletKernel]
State after:
case e_a.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
⊢ f y * ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y * (fourier n) ↑x =
    f y * ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier n) ↑(x - y)

State before:
case e_a.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
⊢ f y * ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier (-n)) ↑y * (fourier n) ↑x =
    f y * ∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier n) ↑(x - y)
Tactic:
congr
State after:
case e_a.e_f.h.e_a.e_f
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
⊢ (fun n => (fourier (-n)) ↑y * (fourier n) ↑x) = fun n => (fourier n) ↑(x - y)

State before:
case e_a.e_f.h.e_a.e_f
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
⊢ (fun n => (fourier (-n)) ↑y * (fourier n) ↑x) = fun n => (fourier n) ↑(x - y)
Tactic:
ext n
State after:
case e_a.e_f.h.e_a.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
n : ℤ
⊢ (fourier (-n)) ↑y * (fourier n) ↑x = (fourier n) ↑(x - y)

State before:
case e_a.e_f.h.e_a.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
n : ℤ
⊢ (fourier (-n)) ↑y * (fourier n) ↑x = (fourier n) ↑(x - y)
Tactic:
rw [fourier_coe_apply, fourier_coe_apply, fourier_coe_apply, ←exp_add]
State after:
case e_a.e_f.h.e_a.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
n : ℤ
⊢ cexp (2 * ↑Real.pi * I * ↑(-n) * ↑y / ↑(2 * Real.pi) + 2 * ↑Real.pi * I * ↑n * ↑x / ↑(2 * Real.pi)) =
    cexp (2 * ↑Real.pi * I * ↑n * ↑(x - y) / ↑(2 * Real.pi))

State before:
case e_a.e_f.h.e_a.e_f.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
n : ℤ
⊢ cexp (2 * ↑Real.pi * I * ↑(-n) * ↑y / ↑(2 * Real.pi) + 2 * ↑Real.pi * I * ↑n * ↑x / ↑(2 * Real.pi)) =
    cexp (2 * ↑Real.pi * I * ↑n * ↑(x - y) / ↑(2 * Real.pi))
Tactic:
congr
State after:
case e_a.e_f.h.e_a.e_f.h.e_z
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
n : ℤ
⊢ 2 * ↑Real.pi * I * ↑(-n) * ↑y / ↑(2 * Real.pi) + 2 * ↑Real.pi * I * ↑n * ↑x / ↑(2 * Real.pi) =
    2 * ↑Real.pi * I * ↑n * ↑(x - y) / ↑(2 * Real.pi)

State before:
case e_a.e_f.h.e_a.e_f.h.e_z
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
n : ℤ
⊢ 2 * ↑Real.pi * I * ↑(-n) * ↑y / ↑(2 * Real.pi) + 2 * ↑Real.pi * I * ↑n * ↑x / ↑(2 * Real.pi) =
    2 * ↑Real.pi * I * ↑n * ↑(x - y) / ↑(2 * Real.pi)
Tactic:
field_simp
State after:
case e_a.e_f.h.e_a.e_f.h.e_z
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
n : ℤ
⊢ (-(2 * ↑Real.pi * I * ↑n * ↑y) + 2 * ↑Real.pi * I * ↑n * ↑x) / (2 * ↑Real.pi) =
    2 * ↑Real.pi * I * ↑n * (↑x - ↑y) / (2 * ↑Real.pi)

State before:
case e_a.e_f.h.e_a.e_f.h.e_z
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
y : ℝ
n : ℤ
⊢ (-(2 * ↑Real.pi * I * ↑n * ↑y) + 2 * ↑Real.pi * I * ↑n * ↑x) / (2 * ↑Real.pi) =
    2 * ↑Real.pi * I * ↑n * (↑x - ↑y) / (2 * ↑Real.pi)
Tactic:
rw [mul_sub, sub_eq_neg_add]
State after:
no goals