Theorem: k_measurable (Carleson/Theorem1_1/Hilbert_kernel.lean)

State before:
⊢ Measurable k
Tactic:
apply Measurable.div
State after:
case hf

⊢ Measurable fun a => ↑(max (1 - |a|) 0)

case hg

⊢ Measurable fun a => 1 - (Complex.I * ↑a).exp

State before:
case hg

⊢ Measurable fun a => 1 - (Complex.I * ↑a).exp
Tactic:
. measurability
State after:
no goals

State before:
case hf

⊢ Measurable fun a => ↑(max (1 - |a|) 0)
Tactic:
apply Measurable.comp'
State after:
case hf.hg

⊢ Measurable Complex.ofReal'

case hf.hf

⊢ Measurable fun x => max (1 - |x|) 0

case hf.x

⊢ MeasurableSpace ℝ

State before:
case hf.hg

⊢ Measurable Complex.ofReal'
Tactic:
exact Complex.measurable_ofReal
State after:
no goals

State before:
case hf.hf

⊢ Measurable fun x => max (1 - |x|) 0
Tactic:
exact Measurable.max (measurable_const.sub measurable_norm) measurable_const
State after:
no goals

State before:
case hg

⊢ Measurable fun a => 1 - (Complex.I * ↑a).exp
Tactic:
measurability
State after:
no goals