Theorem: dirichlet_Hilbert_eq (Carleson/Theorem1_1/Control_Approximation_Effect.lean)

State before:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) * dirichletKernel' N (x - y) =
    cexp (I * (-↑N * ↑x)) * K x y * cexp (I * ↑N * ↑y) +
      (starRingEnd ℂ) (cexp (I * (-↑N * ↑x)) * K x y * cexp (I * ↑N * ↑y))
Tactic:
rw [dirichletKernel', K, k]
State after:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * ↑(x - y)) / (1 - cexp (-I * ↑(x - y))) + cexp (-I * ↑N * ↑(x - y)) / (1 - cexp (I * ↑(x - y)))) =
    cexp (I * (-↑N * ↑x)) * (↑(max (1 - |x - y|) 0) / (1 - cexp (I * ↑(x - y)))) * cexp (I * ↑N * ↑y) +
      (starRingEnd ℂ)
        (cexp (I * (-↑N * ↑x)) * (↑(max (1 - |x - y|) 0) / (1 - cexp (I * ↑(x - y)))) * cexp (I * ↑N * ↑y))

State before:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * ↑(x - y)) / (1 - cexp (-I * ↑(x - y))) + cexp (-I * ↑N * ↑(x - y)) / (1 - cexp (I * ↑(x - y)))) =
    cexp (I * (-↑N * ↑x)) * (↑(max (1 - |x - y|) 0) / (1 - cexp (I * ↑(x - y)))) * cexp (I * ↑N * ↑y) +
      (starRingEnd ℂ)
        (cexp (I * (-↑N * ↑x)) * (↑(max (1 - |x - y|) 0) / (1 - cexp (I * ↑(x - y)))) * cexp (I * ↑N * ↑y))
Tactic:
rw [map_mul, map_mul, map_div₀, conj_ofReal, map_sub, ←exp_conj, ←exp_conj, ←exp_conj,
  map_mul, map_mul, map_mul, map_mul, map_mul, conj_ofReal, conj_ofReal, conj_ofReal]
State after:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * ↑(x - y)) / (1 - cexp (-I * ↑(x - y))) + cexp (-I * ↑N * ↑(x - y)) / (1 - cexp (I * ↑(x - y)))) =
    cexp (I * (-↑N * ↑x)) * (↑(max (1 - |x - y|) 0) / (1 - cexp (I * ↑(x - y)))) * cexp (I * ↑N * ↑y) +
      cexp ((starRingEnd ℂ) I * ((starRingEnd ℂ) (-↑N) * ↑x)) *
          (↑(max (1 - |x - y|) 0) / ((starRingEnd ℂ) 1 - cexp ((starRingEnd ℂ) I * ↑(x - y)))) *
        cexp ((starRingEnd ℂ) I * (starRingEnd ℂ) ↑N * ↑y)

State before:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * ↑(x - y)) / (1 - cexp (-I * ↑(x - y))) + cexp (-I * ↑N * ↑(x - y)) / (1 - cexp (I * ↑(x - y)))) =
    cexp (I * (-↑N * ↑x)) * (↑(max (1 - |x - y|) 0) / (1 - cexp (I * ↑(x - y)))) * cexp (I * ↑N * ↑y) +
      cexp ((starRingEnd ℂ) I * ((starRingEnd ℂ) (-↑N) * ↑x)) *
          (↑(max (1 - |x - y|) 0) / ((starRingEnd ℂ) 1 - cexp ((starRingEnd ℂ) I * ↑(x - y)))) *
        cexp ((starRingEnd ℂ) I * (starRingEnd ℂ) ↑N * ↑y)
Tactic:
simp
State after:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * (↑x - ↑y)) / (1 - cexp (-(I * (↑x - ↑y)))) +
        cexp (-(I * ↑N * (↑x - ↑y))) / (1 - cexp (I * (↑x - ↑y)))) =
    cexp (-(I * (↑N * ↑x))) * (↑(max (1 - |x - y|) 0) / (1 - cexp (I * (↑x - ↑y)))) * cexp (I * ↑N * ↑y) +
      cexp (I * (↑N * ↑x)) * (↑(max (1 - |x - y|) 0) / (1 - cexp (-(I * (↑x - ↑y))))) * cexp (-(I * ↑N * ↑y))

State before:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * (↑x - ↑y)) / (1 - cexp (-(I * (↑x - ↑y)))) +
        cexp (-(I * ↑N * (↑x - ↑y))) / (1 - cexp (I * (↑x - ↑y)))) =
    cexp (-(I * (↑N * ↑x))) * (↑(max (1 - |x - y|) 0) / (1 - cexp (I * (↑x - ↑y)))) * cexp (I * ↑N * ↑y) +
      cexp (I * (↑N * ↑x)) * (↑(max (1 - |x - y|) 0) / (1 - cexp (-(I * (↑x - ↑y))))) * cexp (-(I * ↑N * ↑y))
Tactic:
field_simp
State after:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * (↑x - ↑y)) / (1 - cexp (-(I * (↑x - ↑y)))) +
        cexp (-(I * ↑N * (↑x - ↑y))) / (1 - cexp (I * (↑x - ↑y)))) =
    cexp (-(I * (↑N * ↑x))) * ↑(max (1 - |x - y|) 0) * cexp (I * ↑N * ↑y) / (1 - cexp (I * (↑x - ↑y))) +
      cexp (I * (↑N * ↑x)) * ↑(max (1 - |x - y|) 0) * cexp (-(I * ↑N * ↑y)) / (1 - cexp (-(I * (↑x - ↑y))))

State before:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * (↑x - ↑y)) / (1 - cexp (-(I * (↑x - ↑y)))) +
        cexp (-(I * ↑N * (↑x - ↑y))) / (1 - cexp (I * (↑x - ↑y)))) =
    cexp (-(I * (↑N * ↑x))) * ↑(max (1 - |x - y|) 0) * cexp (I * ↑N * ↑y) / (1 - cexp (I * (↑x - ↑y))) +
      cexp (I * (↑N * ↑x)) * ↑(max (1 - |x - y|) 0) * cexp (-(I * ↑N * ↑y)) / (1 - cexp (-(I * (↑x - ↑y))))
Tactic:
symm
State after:
N : ℕ
x y : ℝ
⊢ cexp (-(I * (↑N * ↑x))) * ↑(max (1 - |x - y|) 0) * cexp (I * ↑N * ↑y) / (1 - cexp (I * (↑x - ↑y))) +
      cexp (I * (↑N * ↑x)) * ↑(max (1 - |x - y|) 0) * cexp (-(I * ↑N * ↑y)) / (1 - cexp (-(I * (↑x - ↑y)))) =
    ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * (↑x - ↑y)) / (1 - cexp (-(I * (↑x - ↑y)))) +
        cexp (-(I * ↑N * (↑x - ↑y))) / (1 - cexp (I * (↑x - ↑y))))

State before:
N : ℕ
x y : ℝ
⊢ cexp (-(I * (↑N * ↑x))) * ↑(max (1 - |x - y|) 0) * cexp (I * ↑N * ↑y) / (1 - cexp (I * (↑x - ↑y))) +
      cexp (I * (↑N * ↑x)) * ↑(max (1 - |x - y|) 0) * cexp (-(I * ↑N * ↑y)) / (1 - cexp (-(I * (↑x - ↑y)))) =
    ↑(max (1 - |x - y|) 0) *
      (cexp (I * ↑N * (↑x - ↑y)) / (1 - cexp (-(I * (↑x - ↑y)))) +
        cexp (-(I * ↑N * (↑x - ↑y))) / (1 - cexp (I * (↑x - ↑y))))
Tactic:
rw [mul_comm, ←mul_assoc, ←exp_add, mul_comm, add_comm, mul_comm, ←mul_assoc, ←exp_add, mul_comm, mul_add, mul_div_assoc, mul_div_assoc]
State after:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) * (cexp (-(I * ↑N * ↑y) + I * (↑N * ↑x)) / (1 - cexp (-(I * (↑x - ↑y))))) +
      ↑(max (1 - |x - y|) 0) * (cexp (I * ↑N * ↑y + -(I * (↑N * ↑x))) / (1 - cexp (I * (↑x - ↑y)))) =
    ↑(max (1 - |x - y|) 0) * (cexp (I * ↑N * (↑x - ↑y)) / (1 - cexp (-(I * (↑x - ↑y))))) +
      ↑(max (1 - |x - y|) 0) * (cexp (-(I * ↑N * (↑x - ↑y))) / (1 - cexp (I * (↑x - ↑y))))

State before:
N : ℕ
x y : ℝ
⊢ ↑(max (1 - |x - y|) 0) * (cexp (-(I * ↑N * ↑y) + I * (↑N * ↑x)) / (1 - cexp (-(I * (↑x - ↑y))))) +
      ↑(max (1 - |x - y|) 0) * (cexp (I * ↑N * ↑y + -(I * (↑N * ↑x))) / (1 - cexp (I * (↑x - ↑y)))) =
    ↑(max (1 - |x - y|) 0) * (cexp (I * ↑N * (↑x - ↑y)) / (1 - cexp (-(I * (↑x - ↑y))))) +
      ↑(max (1 - |x - y|) 0) * (cexp (-(I * ↑N * (↑x - ↑y))) / (1 - cexp (I * (↑x - ↑y))))
Tactic:
congr <;> ring
State after:
no goals