internlm/Lean-Github huggingface dataset:
Theorem: norm_dirichletKernel'_le
Proof state before:
case neg
N : ℕ
x : ℝ
h : cexp (I * ↑x) = 1
⊢ ‖dirichletKernel' N x‖ ≤ 2 * ↑N + 1
Tactic:
rw [dirichletKernel'_eq_zero h, norm_zero]
Proof state after:
case neg
N : ℕ
x : ℝ
h : cexp (I * ↑x) = 1
⊢ 0 ≤ 2 * ↑N + 1
Theorem: norm_dirichletKernel'_le
Proof state before:
case neg
N : ℕ
x : ℝ
h : cexp (I * ↑x) = 1
⊢ 0 ≤ 2 * ↑N + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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]
Proof state after:
no goals
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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]
Proof state after:
no goals
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof 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)
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof 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)
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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]
Proof state after:
no goals
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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]
Proof 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)
⊢ ℤ → ℝ
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof state after:
no goals
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof 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
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof 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
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof 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
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof state after:
no goals
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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]
Proof 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)
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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 _
Proof 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)
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof 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)
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof state after:
no goals
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof 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
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof 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
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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]
Proof 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)
⊢ ℝ → ℤ → ℝ
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof 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)
⊢ ℝ → ℤ → ℝ
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof 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)
⊢ ℝ → ℤ → ℝ
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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]
Proof 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)
⊢ ℝ → ℤ → ℝ
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof state after:
no goals
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof 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)
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof 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)
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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]
Proof 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)
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof 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)
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof 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)
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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]
Proof 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))
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof 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)
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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
Proof 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)
Theorem: partialFourierSum_eq_conv_dirichletKernel
Proof 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]
Proof state after:
no goals
Theorem: partialFourierSum_eq_conv_dirichletKernel'
Proof 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
Proof 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)
Theorem: partialFourierSum_eq_conv_dirichletKernel'
Proof 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]
Proof 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)