Theorem: norm_dirichletKernel'_le (Carleson/Theorem1_1/Dirichlet_kernel.lean)

State before:
N : ℕ
x : ℝ
⊢ ‖dirichletKernel' N x‖ ≤ 2 * ↑N + 1
Tactic:
by_cases h : cexp (I * x) ≠ 1
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

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
State after:
case neg
N : ℕ
x : ℝ
h : ¬cexp (I * ↑x) ≠ 1
⊢ ‖dirichletKernel' N x‖ ≤ 2 * ↑N + 1

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
State after:
no goals

State before:
case pos
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ ‖dirichletKernel' N x‖ ≤ 2 * ↑N + 1
Tactic:
rw [← dirichletKernel_eq]
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

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
State after:
case pos
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ cexp (I * ↑x) ≠ 1

State before:
case pos
N : ℕ
x : ℝ
h : cexp (I * ↑x) ≠ 1
⊢ cexp (I * ↑x) ≠ 1
Tactic:
exact h
State after:
no goals

State before:
case neg
N : ℕ
x : ℝ
h : ¬cexp (I * ↑x) ≠ 1
⊢ ‖dirichletKernel' N x‖ ≤ 2 * ↑N + 1
Tactic:
push_neg at h
State after:
case neg
N : ℕ
x : ℝ
h : cexp (I * ↑x) = 1
⊢ ‖dirichletKernel' N x‖ ≤ 2 * ↑N + 1

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]
State after:
case neg
N : ℕ
x : ℝ
h : cexp (I * ↑x) = 1
⊢ 0 ≤ 2 * ↑N + 1

State before:
case neg
N : ℕ
x : ℝ
h : cexp (I * ↑x) = 1
⊢ 0 ≤ 2 * ↑N + 1
Tactic:
linarith
State after:
no goals