Theorem: CarlesonOperatorRat'_measurable (Carleson/Theorem1_1/CarlesonOperatorReal.lean)

State before:
f : ℝ → ℂ
hf : Measurable f
⊢ Measurable (CarlesonOperatorRat' K f)
Tactic:
apply measurable_iSup
State after:
case hf
f : ℝ → ℂ
hf : Measurable f
⊢ ∀ (i : ℤ),
    Measurable fun b =>
      ⨆ r, ⨆ (_ : 0 < r), ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑i * ↑y).exp‖₊

State before:
case hf
f : ℝ → ℂ
hf : Measurable f
⊢ ∀ (i : ℤ),
    Measurable fun b =>
      ⨆ r, ⨆ (_ : 0 < r), ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑i * ↑y).exp‖₊
Tactic:
intro n
State after:
case hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
⊢ Measurable fun b =>
    ⨆ r, ⨆ (_ : 0 < r), ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊

State before:
case hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
⊢ Measurable fun b =>
    ⨆ r, ⨆ (_ : 0 < r), ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
apply measurable_iSup
State after:
case hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
⊢ ∀ (i : ℚ),
    Measurable fun b =>
      ⨆ (_ : 0 < i), ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑i) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊

State before:
case hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
⊢ ∀ (i : ℚ),
    Measurable fun b =>
      ⨆ (_ : 0 < i), ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑i) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
intro r
State after:
case hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
⊢ Measurable fun b =>
    ⨆ (_ : 0 < r), ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊

State before:
case hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
⊢ Measurable fun b =>
    ⨆ (_ : 0 < r), ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
apply measurable_iSup
State after:
case hf.hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
⊢ 0 < r → Measurable fun b => ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊

State before:
case hf.hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
⊢ 0 < r → Measurable fun b => ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
intro hr
State after:
case hf.hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
hr : 0 < r
⊢ Measurable fun b => ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊

State before:
case hf.hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
hr : 0 < r
⊢ Measurable fun b => ↑‖∫ (y : ℝ) in {y | dist b y ∈ Set.Ioo (↑r) 1}, f y * K b y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
apply Measurable.coe_nnreal_ennreal
State after:
case hf.hf.hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
hr : 0 < r
⊢ Measurable fun x => ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo (↑r) 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊

State before:
case hf.hf.hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
hr : 0 < r
⊢ Measurable fun x => ‖∫ (y : ℝ) in {y | dist x y ∈ Set.Ioo (↑r) 1}, f y * K x y * (Complex.I * ↑n * ↑y).exp‖₊
Tactic:
apply Measurable.nnnorm
State after:
case hf.hf.hf.hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
hr : 0 < r
⊢ Measurable fun a => ∫ (y : ℝ) in {y | dist a y ∈ Set.Ioo (↑r) 1}, f y * K a y * (Complex.I * ↑n * ↑y).exp

State before:
case hf.hf.hf.hf.hf
f : ℝ → ℂ
hf : Measurable f
n : ℤ
r : ℚ
hr : 0 < r
⊢ Measurable fun a => ∫ (y : ℝ) in {y | dist a y ∈ Set.Ioo (↑r) 1}, f y * K a y * (Complex.I * ↑n * ↑y).exp
Tactic:
sorry
State after:
no goals