Theorem: dirichletKernel'_measurable (Carleson/Theorem1_1/Dirichlet_kernel.lean)

State before:
N : ℕ
⊢ Measurable (dirichletKernel' N)
Tactic:
apply Measurable.add
State after:
case hf
N : ℕ
⊢ Measurable fun a => cexp (I * ↑N * ↑a) / (1 - cexp (-I * ↑a))

case hg
N : ℕ
⊢ Measurable fun a => cexp (-I * ↑N * ↑a) / (1 - cexp (I * ↑a))

State before:
case hf
N : ℕ
⊢ Measurable fun a => cexp (I * ↑N * ↑a) / (1 - cexp (-I * ↑a))

case hg
N : ℕ
⊢ Measurable fun a => cexp (-I * ↑N * ↑a) / (1 - cexp (I * ↑a))
Tactic:
. apply Measurable.div <;> measurability
State after:
case hg
N : ℕ
⊢ Measurable fun a => cexp (-I * ↑N * ↑a) / (1 - cexp (I * ↑a))

State before:
case hg
N : ℕ
⊢ Measurable fun a => cexp (-I * ↑N * ↑a) / (1 - cexp (I * ↑a))
Tactic:
. apply Measurable.div <;> measurability
State after:
no goals

State before:
case hf
N : ℕ
⊢ Measurable fun a => cexp (I * ↑N * ↑a) / (1 - cexp (-I * ↑a))
Tactic:
apply Measurable.div <;> measurability
State after:
no goals

State before:
case hg
N : ℕ
⊢ Measurable fun a => cexp (-I * ↑N * ↑a) / (1 - cexp (I * ↑a))
Tactic:
apply Measurable.div <;> measurability
State after:
no goals