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:
have : (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel' N (x - y) = (1 / (2 * Real.pi)) * ∫ (y : ℝ) in (0 : ℝ)..(2 * Real.pi), f y * dirichletKernel N (x - y) := by
  congr 1
  apply intervalIntegral.integral_congr_ae
  apply MeasureTheory.ae_imp_of_ae_restrict
  apply MeasureTheory.ae_restrict_of_ae
  sorry
State after:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
this :
  1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel' N (x - y) =
    1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel N (x - y)
⊢ partialFourierSum f N x = 1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel' N (x - y)

State before:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
this :
  1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel' N (x - y) =
    1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel N (x - y)
⊢ partialFourierSum f N x = 1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel' N (x - y)
Tactic:
rw [this]
State after:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
this :
  1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel' N (x - y) =
    1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel N (x - y)
⊢ partialFourierSum f N x = 1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel N (x - y)

State before:
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
this :
  1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel' N (x - y) =
    1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel N (x - y)
⊢ partialFourierSum f N x = 1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel N (x - y)
Tactic:
exact partialFourierSum_eq_conv_dirichletKernel h
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 * dirichletKernel' N (x - y) =
    1 / (2 * ↑Real.pi) * ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel N (x - y)
Tactic:
congr 1
State after:
case e_a
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel' N (x - y) =
    ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel N (x - y)

State before:
case e_a
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel' N (x - y) =
    ∫ (y : ℝ) in 0 ..2 * Real.pi, f y * dirichletKernel N (x - y)
Tactic:
apply intervalIntegral.integral_congr_ae
State after:
case e_a.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∀ᵐ (x_1 : ℝ), x_1 ∈ Ι 0 (2 * Real.pi) → f x_1 * dirichletKernel' N (x - x_1) = f x_1 * dirichletKernel N (x - x_1)

State before:
case e_a.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∀ᵐ (x_1 : ℝ), x_1 ∈ Ι 0 (2 * Real.pi) → f x_1 * dirichletKernel' N (x - x_1) = f x_1 * dirichletKernel N (x - x_1)
Tactic:
apply MeasureTheory.ae_imp_of_ae_restrict
State after:
case e_a.h.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∀ᵐ (x_1 : ℝ) ∂MeasureTheory.volume.restrict (Ι 0 (2 * Real.pi)),
    f x_1 * dirichletKernel' N (x - x_1) = f x_1 * dirichletKernel N (x - x_1)

State before:
case e_a.h.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∀ᵐ (x_1 : ℝ) ∂MeasureTheory.volume.restrict (Ι 0 (2 * Real.pi)),
    f x_1 * dirichletKernel' N (x - x_1) = f x_1 * dirichletKernel N (x - x_1)
Tactic:
apply MeasureTheory.ae_restrict_of_ae
State after:
case e_a.h.h.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∀ᵐ (x_1 : ℝ), f x_1 * dirichletKernel' N (x - x_1) = f x_1 * dirichletKernel N (x - x_1)

State before:
case e_a.h.h.h
f : ℝ → ℂ
N : ℕ
x : ℝ
h : IntervalIntegrable f MeasureTheory.volume 0 (2 * Real.pi)
⊢ ∀ᵐ (x_1 : ℝ), f x_1 * dirichletKernel' N (x - x_1) = f x_1 * dirichletKernel N (x - x_1)
Tactic:
sorry
State after:
no goals