internlm/Lean-Github huggingface dataset:
Theorem: dirichletKernel_eq
Proof state before:
N : ℕ
x : ℝ
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ cexp (1 / 2 * I * ↑x) * cexp (-1 / 2 * I * ↑x) = 1
Tactic:
rw [← exp_add]
Proof state after:
N : ℕ
x : ℝ
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ cexp (1 / 2 * I * ↑x + -1 / 2 * I * ↑x) = 1
Theorem: dirichletKernel_eq
Proof state before:
N : ℕ
x : ℝ
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ cexp (1 / 2 * I * ↑x + -1 / 2 * I * ↑x) = 1
Tactic:
ring_nf
Proof state after:
N : ℕ
x : ℝ
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ cexp 0 = 1
Theorem: dirichletKernel_eq
Proof state before:
N : ℕ
x : ℝ
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h : cexp (1 / 2 * I * ↑x) = cexp (-1 / 2 * I * ↑x)
⊢ cexp 0 = 1
Tactic:
exact exp_zero
Proof state after:
no goals
Theorem: dirichletKernel_eq
Proof state before:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x)))
Tactic:
rw [mul_div]
Proof state after:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x))
Theorem: dirichletKernel_eq
Proof state before:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (I * ↑N * ↑x) / (1 - cexp (-I * ↑x))
Tactic:
apply eq_div_of_mul_eq
Proof state after:
case e_a.hc
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ 1 - cexp (-I * ↑x) ≠ 0

case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) * (1 - cexp (-I * ↑x)) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (I * ↑N * ↑x)
Theorem: dirichletKernel_eq
Proof state before:
case e_a.hc
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ 1 - cexp (-I * ↑x) ≠ 0

case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) * (1 - cexp (-I * ↑x)) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (I * ↑N * ↑x)
Tactic:
. contrapose! h
  rwa [sub_eq_zero, neg_mul, exp_neg, eq_comm, inv_eq_one] at h
Proof state after:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) * (1 - cexp (-I * ↑x)) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (I * ↑N * ↑x)
Theorem: dirichletKernel_eq
Proof state before:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp ((↑N + 1 / 2) * I * ↑x) * (1 - cexp (-I * ↑x)) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (I * ↑N * ↑x)
Tactic:
ring_nf
Proof state after:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp (↑N * I * ↑x + I * ↑x * (1 / 2)) - cexp (↑N * I * ↑x + I * ↑x * (1 / 2)) * cexp (-(I * ↑x)) =
    cexp (I * ↑x * (1 / 2)) * cexp (↑N * I * ↑x) - cexp (I * ↑x * (-1 / 2)) * cexp (↑N * I * ↑x)
Theorem: dirichletKernel_eq
Proof state before:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp (↑N * I * ↑x + I * ↑x * (1 / 2)) - cexp (↑N * I * ↑x + I * ↑x * (1 / 2)) * cexp (-(I * ↑x)) =
    cexp (I * ↑x * (1 / 2)) * cexp (↑N * I * ↑x) - cexp (I * ↑x * (-1 / 2)) * cexp (↑N * I * ↑x)
Tactic:
rw [← exp_add, ← exp_add, ← exp_add]
Proof state after:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp (↑N * I * ↑x + I * ↑x * (1 / 2)) - cexp (↑N * I * ↑x + I * ↑x * (1 / 2) + -(I * ↑x)) =
    cexp (I * ↑x * (1 / 2) + ↑N * I * ↑x) - cexp (I * ↑x * (-1 / 2) + ↑N * I * ↑x)
Theorem: dirichletKernel_eq
Proof state before:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp (↑N * I * ↑x + I * ↑x * (1 / 2)) - cexp (↑N * I * ↑x + I * ↑x * (1 / 2) + -(I * ↑x)) =
    cexp (I * ↑x * (1 / 2) + ↑N * I * ↑x) - cexp (I * ↑x * (-1 / 2) + ↑N * I * ↑x)
Tactic:
congr 2 <;> ring
Proof state after:
no goals
Theorem: dirichletKernel_eq
Proof state before:
case e_a.hc
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ 1 - cexp (-I * ↑x) ≠ 0
Tactic:
contrapose! h
Proof state after:
case e_a.hc
N : ℕ
x : ℝ
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
h : 1 - cexp (-I * ↑x) = 0
⊢ cexp (I * ↑x) = 1
Theorem: dirichletKernel_eq
Proof state before:
case e_a.hc
N : ℕ
x : ℝ
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
h : 1 - cexp (-I * ↑x) = 0
⊢ cexp (I * ↑x) = 1
Tactic:
rwa [sub_eq_zero, neg_mul, exp_neg, eq_comm, inv_eq_one] at h
Proof state after:
no goals
Theorem: dirichletKernel_eq
Proof state before:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * (cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x)))
Tactic:
rw [mul_div]
Proof state after:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x))
Theorem: dirichletKernel_eq
Proof state before:
case e_a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (-I * ↑N * ↑x) / (1 - cexp (I * ↑x))
Tactic:
apply eq_div_of_mul_eq
Proof state after:
case e_a.hc
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ 1 - cexp (I * ↑x) ≠ 0

case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) * (1 - cexp (I * ↑x)) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (-I * ↑N * ↑x)
Theorem: dirichletKernel_eq
Proof state before:
case e_a.hc
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ 1 - cexp (I * ↑x) ≠ 0

case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) * (1 - cexp (I * ↑x)) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (-I * ↑N * ↑x)
Tactic:
. contrapose! h
  rwa [sub_eq_zero, eq_comm] at h
Proof state after:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) * (1 - cexp (I * ↑x)) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (-I * ↑N * ↑x)
Theorem: dirichletKernel_eq
Proof state before:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N + 1 / 2) * I * ↑x) * (1 - cexp (I * ↑x)) =
    (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * cexp (-I * ↑N * ↑x)
Tactic:
ring_nf
Proof state after:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N * I * ↑x) + I * ↑x * (-1 / 2)) + cexp (-(↑N * I * ↑x) + I * ↑x * (-1 / 2)) * cexp (I * ↑x) =
    cexp (I * ↑x * (1 / 2)) * cexp (-(↑N * I * ↑x)) - cexp (I * ↑x * (-1 / 2)) * cexp (-(↑N * I * ↑x))
Theorem: dirichletKernel_eq
Proof state before:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ -cexp (-(↑N * I * ↑x) + I * ↑x * (-1 / 2)) + cexp (-(↑N * I * ↑x) + I * ↑x * (-1 / 2)) * cexp (I * ↑x) =
    cexp (I * ↑x * (1 / 2)) * cexp (-(↑N * I * ↑x)) - cexp (I * ↑x * (-1 / 2)) * cexp (-(↑N * I * ↑x))
Tactic:
rw [← exp_add, ← exp_add, ← exp_add, neg_add_eq_sub]
Proof state after:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp (-(↑N * I * ↑x) + I * ↑x * (-1 / 2) + I * ↑x) - cexp (-(↑N * I * ↑x) + I * ↑x * (-1 / 2)) =
    cexp (I * ↑x * (1 / 2) + -(↑N * I * ↑x)) - cexp (I * ↑x * (-1 / 2) + -(↑N * I * ↑x))
Theorem: dirichletKernel_eq
Proof state before:
case e_a.a
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ cexp (-(↑N * I * ↑x) + I * ↑x * (-1 / 2) + I * ↑x) - cexp (-(↑N * I * ↑x) + I * ↑x * (-1 / 2)) =
    cexp (I * ↑x * (1 / 2) + -(↑N * I * ↑x)) - cexp (I * ↑x * (-1 / 2) + -(↑N * I * ↑x))
Tactic:
congr 2 <;> ring
Proof state after:
no goals
Theorem: dirichletKernel_eq
Proof state before:
case e_a.hc
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
⊢ 1 - cexp (I * ↑x) ≠ 0
Tactic:
contrapose! h
Proof state after:
case e_a.hc
N : ℕ
x : ℝ
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
h : 1 - cexp (I * ↑x) = 0
⊢ cexp (I * ↑x) = 1
Theorem: dirichletKernel_eq
Proof state before:
case e_a.hc
N : ℕ
x : ℝ
this :
  (cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x)) * dirichletKernel N x =
    cexp ((↑N + 1 / 2) * I * ↑x) - cexp (-(↑N + 1 / 2) * I * ↑x)
h' : cexp (1 / 2 * I * ↑x) - cexp (-1 / 2 * I * ↑x) ≠ 0
h : 1 - cexp (I * ↑x) = 0
⊢ cexp (I * ↑x) = 1
Tactic:
rwa [sub_eq_zero, eq_comm] at h
Proof state after:
no goals
Theorem: dirichletKernel'_eq_zero
Proof state before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) = 1
⊢ dirichletKernel' N x = 0
Tactic:
rw [dirichletKernel', neg_mul, exp_neg, h]
Proof state after:
N : ℕ
x : ℝ
h : cexp (I * ↑x) = 1
⊢ cexp (I * ↑N * ↑x) / (1 - 1⁻¹) + cexp (-I * ↑N * ↑x) / (1 - 1) = 0
Theorem: dirichletKernel'_eq_zero
Proof state before:
N : ℕ
x : ℝ
h : cexp (I * ↑x) = 1
⊢ cexp (I * ↑N * ↑x) / (1 - 1⁻¹) + cexp (-I * ↑N * ↑x) / (1 - 1) = 0
Tactic:
simp
Proof state after:
no goals
Theorem: dirichletKernel_eq_ae
Proof state before:
N : ℕ
⊢ ∀ᵐ (x : ℝ), dirichletKernel N x = dirichletKernel' N x
Tactic:
rw [MeasureTheory.ae_iff]
Proof state after:
N : ℕ
⊢ MeasureTheory.volume {a | ¬dirichletKernel N a = dirichletKernel' N a} = 0
Theorem: dirichletKernel_eq_ae
Proof state before:
N : ℕ
⊢ MeasureTheory.volume {a | ¬dirichletKernel N a = dirichletKernel' N a} = 0
Tactic:
have : {x | ¬dirichletKernel N x = dirichletKernel' N x} = {x | ∃ n : ℤ, x = n * (2 * Real.pi)} := by
  ext x
  simp
  constructor
  . sorry
  . sorry
Proof state after:
N : ℕ
this : {x | ¬dirichletKernel N x = dirichletKernel' N x} = {x | ∃ n, x = ↑n * (2 * Real.pi)}
⊢ MeasureTheory.volume {a | ¬dirichletKernel N a = dirichletKernel' N a} = 0
Theorem: dirichletKernel_eq_ae
Proof state before:
N : ℕ
this : {x | ¬dirichletKernel N x = dirichletKernel' N x} = {x | ∃ n, x = ↑n * (2 * Real.pi)}
⊢ MeasureTheory.volume {a | ¬dirichletKernel N a = dirichletKernel' N a} = 0
Tactic:
rw [this]
Proof state after:
N : ℕ
this : {x | ¬dirichletKernel N x = dirichletKernel' N x} = {x | ∃ n, x = ↑n * (2 * Real.pi)}
⊢ MeasureTheory.volume {x | ∃ n, x = ↑n * (2 * Real.pi)} = 0
Theorem: dirichletKernel_eq_ae
Proof state before:
N : ℕ
this : {x | ¬dirichletKernel N x = dirichletKernel' N x} = {x | ∃ n, x = ↑n * (2 * Real.pi)}
⊢ MeasureTheory.volume {x | ∃ n, x = ↑n * (2 * Real.pi)} = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: dirichletKernel_eq_ae
Proof state before:
N : ℕ
⊢ {x | ¬dirichletKernel N x = dirichletKernel' N x} = {x | ∃ n, x = ↑n * (2 * Real.pi)}
Tactic:
ext x
Proof state after:
case h
N : ℕ
x : ℝ
⊢ x ∈ {x | ¬dirichletKernel N x = dirichletKernel' N x} ↔ x ∈ {x | ∃ n, x = ↑n * (2 * Real.pi)}
Theorem: dirichletKernel_eq_ae
Proof state before:
case h
N : ℕ
x : ℝ
⊢ x ∈ {x | ¬dirichletKernel N x = dirichletKernel' N x} ↔ x ∈ {x | ∃ n, x = ↑n * (2 * Real.pi)}
Tactic:
simp
Proof state after:
case h
N : ℕ
x : ℝ
⊢ ¬dirichletKernel N x = dirichletKernel' N x ↔ ∃ n, x = ↑n * (2 * Real.pi)
Theorem: dirichletKernel_eq_ae
Proof state before:
case h
N : ℕ
x : ℝ
⊢ ¬dirichletKernel N x = dirichletKernel' N x ↔ ∃ n, x = ↑n * (2 * Real.pi)
Tactic:
constructor
Proof state after:
case h.mp
N : ℕ
x : ℝ
⊢ ¬dirichletKernel N x = dirichletKernel' N x → ∃ n, x = ↑n * (2 * Real.pi)

case h.mpr
N : ℕ
x : ℝ
⊢ (∃ n, x = ↑n * (2 * Real.pi)) → ¬dirichletKernel N x = dirichletKernel' N x
Theorem: dirichletKernel_eq_ae
Proof state before:
case h.mp
N : ℕ
x : ℝ
⊢ ¬dirichletKernel N x = dirichletKernel' N x → ∃ n, x = ↑n * (2 * Real.pi)

case h.mpr
N : ℕ
x : ℝ
⊢ (∃ n, x = ↑n * (2 * Real.pi)) → ¬dirichletKernel N x = dirichletKernel' N x
Tactic:
. sorry
Proof state after:
case h.mpr
N : ℕ
x : ℝ
⊢ (∃ n, x = ↑n * (2 * Real.pi)) → ¬dirichletKernel N x = dirichletKernel' N x
Theorem: dirichletKernel_eq_ae
Proof state before:
case h.mpr
N : ℕ
x : ℝ
⊢ (∃ n, x = ↑n * (2 * Real.pi)) → ¬dirichletKernel N x = dirichletKernel' N x
Tactic:
. sorry
Proof state after:
no goals
Theorem: dirichletKernel_eq_ae
Proof state before:
case h.mp
N : ℕ
x : ℝ
⊢ ¬dirichletKernel N x = dirichletKernel' N x → ∃ n, x = ↑n * (2 * Real.pi)
Tactic:
sorry
Proof state after:
no goals
Theorem: dirichletKernel_eq_ae
Proof state before:
case h.mpr
N : ℕ
x : ℝ
⊢ (∃ n, x = ↑n * (2 * Real.pi)) → ¬dirichletKernel N x = dirichletKernel' N x
Tactic:
sorry
Proof state after:
no goals
Theorem: norm_dirichletKernel_le
Proof state before:
N : ℕ
x : ℝ
⊢ ‖dirichletKernel N x‖ ≤ 2 * ↑N + 1
Tactic:
rw [dirichletKernel]
Proof state after:
N : ℕ
x : ℝ
⊢ ‖∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier n) ↑x‖ ≤ 2 * ↑N + 1
Theorem: norm_dirichletKernel_le
Proof state before:
N : ℕ
x : ℝ
⊢ ‖∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier n) ↑x‖ ≤ 2 * ↑N + 1
Tactic:
calc ‖∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier n) ↑x‖
  _ ≤ ∑ n ∈ Icc (-Int.ofNat N) ↑N, ‖(fourier n) ↑x‖ := by
    apply norm_sum_le
  _ ≤ ∑ n ∈ Icc (-Int.ofNat N) ↑N, 1 := by
    apply sum_le_sum
    intro n _
    have : Fact (0 < 2 * Real.pi) := by
      rw [fact_iff]
      exact Real.two_pi_pos
    apply le_trans (ContinuousMap.norm_coe_le_norm (fourier n) x) (fourier_norm n).le
  _ = 2 * N + 1 := by
    rw [sum_const]
    simp only [Int.ofNat_eq_coe, Int.card_Icc, sub_neg_eq_add, nsmul_eq_mul, mul_one]
    norm_cast
    rw [Int.toNat_ofNat]
    ring
Proof state after:
no goals
Theorem: norm_dirichletKernel_le
Proof state before:
N : ℕ
x : ℝ
⊢ ‖∑ n ∈ Icc (-Int.ofNat N) ↑N, (fourier n) ↑x‖ ≤ ∑ n ∈ Icc (-Int.ofNat N) ↑N, ‖(fourier n) ↑x‖
Tactic:
apply norm_sum_le
Proof state after:
no goals
Theorem: norm_dirichletKernel_le
Proof state before:
N : ℕ
x : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, ‖(fourier n) ↑x‖ ≤ ∑ n ∈ Icc (-Int.ofNat N) ↑N, 1
Tactic:
apply sum_le_sum
Proof state after:
case h
N : ℕ
x : ℝ
⊢ ∀ i ∈ Icc (-Int.ofNat N) ↑N, ‖(fourier i) ↑x‖ ≤ 1
Theorem: norm_dirichletKernel_le
Proof state before:
case h
N : ℕ
x : ℝ
⊢ ∀ i ∈ Icc (-Int.ofNat N) ↑N, ‖(fourier i) ↑x‖ ≤ 1
Tactic:
intro n _
Proof state after:
case h
N : ℕ
x : ℝ
n : ℤ
a✝ : n ∈ Icc (-Int.ofNat N) ↑N
⊢ ‖(fourier n) ↑x‖ ≤ 1
Theorem: norm_dirichletKernel_le
Proof state before:
case h
N : ℕ
x : ℝ
n : ℤ
a✝ : n ∈ Icc (-Int.ofNat N) ↑N
⊢ ‖(fourier n) ↑x‖ ≤ 1
Tactic:
have : Fact (0 < 2 * Real.pi) := by
  rw [fact_iff]
  exact Real.two_pi_pos
Proof state after:
case h
N : ℕ
x : ℝ
n : ℤ
a✝ : n ∈ Icc (-Int.ofNat N) ↑N
this : Fact (0 < 2 * Real.pi)
⊢ ‖(fourier n) ↑x‖ ≤ 1
Theorem: norm_dirichletKernel_le
Proof state before:
case h
N : ℕ
x : ℝ
n : ℤ
a✝ : n ∈ Icc (-Int.ofNat N) ↑N
this : Fact (0 < 2 * Real.pi)
⊢ ‖(fourier n) ↑x‖ ≤ 1
Tactic:
apply le_trans (ContinuousMap.norm_coe_le_norm (fourier n) x) (fourier_norm n).le
Proof state after:
no goals
Theorem: norm_dirichletKernel_le
Proof state before:
N : ℕ
x : ℝ
n : ℤ
a✝ : n ∈ Icc (-Int.ofNat N) ↑N
⊢ Fact (0 < 2 * Real.pi)
Tactic:
rw [fact_iff]
Proof state after:
N : ℕ
x : ℝ
n : ℤ
a✝ : n ∈ Icc (-Int.ofNat N) ↑N
⊢ 0 < 2 * Real.pi
Theorem: norm_dirichletKernel_le
Proof state before:
N : ℕ
x : ℝ
n : ℤ
a✝ : n ∈ Icc (-Int.ofNat N) ↑N
⊢ 0 < 2 * Real.pi
Tactic:
exact Real.two_pi_pos
Proof state after:
no goals
Theorem: norm_dirichletKernel_le
Proof state before:
N : ℕ
x : ℝ
⊢ ∑ n ∈ Icc (-Int.ofNat N) ↑N, 1 = 2 * ↑N + 1
Tactic:
rw [sum_const]
Proof state after:
N : ℕ
x : ℝ
⊢ (Icc (-Int.ofNat N) ↑N).card • 1 = 2 * ↑N + 1
Theorem: norm_dirichletKernel_le
Proof state before:
N : ℕ
x : ℝ
⊢ (Icc (-Int.ofNat N) ↑N).card • 1 = 2 * ↑N + 1
Tactic:
simp only [Int.ofNat_eq_coe, Int.card_Icc, sub_neg_eq_add, nsmul_eq_mul, mul_one]
Proof state after:
N : ℕ
x : ℝ
⊢ ↑(↑N + 1 + ↑N).toNat = 2 * ↑N + 1
Theorem: norm_dirichletKernel_le
Proof state before:
N : ℕ
x : ℝ
⊢ ↑(↑N + 1 + ↑N).toNat = 2 * ↑N + 1
Tactic:
norm_cast
Proof state after:
N : ℕ
x : ℝ
⊢ (↑(N + 1 + N)).toNat = 2 * N + 1
Theorem: norm_dirichletKernel_le
Proof state before:
N : ℕ
x : ℝ
⊢ (↑(N + 1 + N)).toNat = 2 * N + 1
Tactic:
rw [Int.toNat_ofNat]
Proof state after:
N : ℕ
x : ℝ
⊢ N + 1 + N = 2 * N + 1
Theorem: norm_dirichletKernel_le
Proof state before:
N : ℕ
x : ℝ
⊢ N + 1 + N = 2 * N + 1
Tactic:
ring
Proof state after:
no goals
Theorem: norm_dirichletKernel'_le
Proof state before:
N : ℕ
x : ℝ
⊢ ‖dirichletKernel' N x‖ ≤ 2 * ↑N + 1
Tactic:
by_cases h : cexp (I * x) ≠ 1
Proof state after:
case pos
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ ‖dirichletKernel' N x‖ ≤ 2 * ↑N + 1

case neg
N : ℕ
x : ℝ
h : ¬cexp (I * ↑x) ≠ 1
⊢ ‖dirichletKernel' N x‖ ≤ 2 * ↑N + 1
Theorem: norm_dirichletKernel'_le
Proof state before:
case pos
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ ‖dirichletKernel' N x‖ ≤ 2 * ↑N + 1

case neg
N : ℕ
x : ℝ
h : ¬cexp (I * ↑x) ≠ 1
⊢ ‖dirichletKernel' N x‖ ≤ 2 * ↑N + 1
Tactic:
. rw [← dirichletKernel_eq]
  apply norm_dirichletKernel_le
  exact h
Proof state after:
case neg
N : ℕ
x : ℝ
h : ¬cexp (I * ↑x) ≠ 1
⊢ ‖dirichletKernel' N x‖ ≤ 2 * ↑N + 1
Theorem: norm_dirichletKernel'_le
Proof state before:
case neg
N : ℕ
x : ℝ
h : ¬cexp (I * ↑x) ≠ 1
⊢ ‖dirichletKernel' N x‖ ≤ 2 * ↑N + 1
Tactic:
. push_neg at h
  rw [dirichletKernel'_eq_zero h, norm_zero]
  linarith
Proof state after:
no goals
Theorem: norm_dirichletKernel'_le
Proof state before:
case pos
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ ‖dirichletKernel' N x‖ ≤ 2 * ↑N + 1
Tactic:
rw [← dirichletKernel_eq]
Proof state after:
case pos
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ ‖dirichletKernel N x‖ ≤ 2 * ↑N + 1

case pos
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ cexp (I * ↑x) ≠ 1
Theorem: norm_dirichletKernel'_le
Proof state before:
case pos
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ ‖dirichletKernel N x‖ ≤ 2 * ↑N + 1

case pos
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ cexp (I * ↑x) ≠ 1
Tactic:
apply norm_dirichletKernel_le
Proof state after:
case pos
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ cexp (I * ↑x) ≠ 1
Theorem: norm_dirichletKernel'_le
Proof state before:
case pos
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ cexp (I * ↑x) ≠ 1
Tactic:
exact h
Proof state after:
no goals
Theorem: norm_dirichletKernel'_le
Proof state before:
case neg
N : ℕ
x : ℝ
h : ¬cexp (I * ↑x) ≠ 1
⊢ ‖dirichletKernel' N x‖ ≤ 2 * ↑N + 1
Tactic:
push_neg at h
Proof state after:
case neg
N : ℕ
x : ℝ
h : cexp (I * ↑x) = 1
⊢ ‖dirichletKernel' N x‖ ≤ 2 * ↑N + 1