Theorem: rcarleson' (Carleson/Theorem1_1/Carleson_on_the_real_line.lean)

State before:
F G : Set ℝ
hF : MeasurableSet F
hG : MeasurableSet G
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ F.indicator 1 x
⊢ ∫⁻ (x : ℝ) in G, T' f x ≤ ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume G ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹
Tactic:
calc ∫⁻ x in G, T' f x
  _ ≤ ∫⁻ x in G, CarlesonOperator' K Θ f x := by
    apply MeasureTheory.lintegral_mono
    apply CarlesonOperatorReal'_le_CarlesonOperator'
  _ ≤ ENNReal.ofReal (C1_2 4 2) * (MeasureTheory.volume G) ^ (2 : ℝ)⁻¹ * (MeasureTheory.volume F) ^ (2 : ℝ)⁻¹ := by
    convert theorem1_2C' K (by simp) h1 h2 hF hG h3 f hf <;> sorry
State after:
no goals

State before:
F G : Set ℝ
hF : MeasurableSet F
hG : MeasurableSet G
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ F.indicator 1 x
⊢ ∫⁻ (x : ℝ) in G, T' f x ≤ ∫⁻ (x : ℝ) in G, CarlesonOperator' K {x | ∃ n, θ n = x} f x
Tactic:
apply MeasureTheory.lintegral_mono
State after:
case hfg
F G : Set ℝ
hF : MeasurableSet F
hG : MeasurableSet G
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ F.indicator 1 x
⊢ (fun a => T' f a) ≤ fun a => CarlesonOperator' K {x | ∃ n, θ n = x} f a

State before:
case hfg
F G : Set ℝ
hF : MeasurableSet F
hG : MeasurableSet G
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ F.indicator 1 x
⊢ (fun a => T' f a) ≤ fun a => CarlesonOperator' K {x | ∃ n, θ n = x} f a
Tactic:
apply CarlesonOperatorReal'_le_CarlesonOperator'
State after:
no goals

State before:
F G : Set ℝ
hF : MeasurableSet F
hG : MeasurableSet G
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ F.indicator 1 x
⊢ ∫⁻ (x : ℝ) in G, CarlesonOperator' K {x | ∃ n, θ n = x} f x ≤
    ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume G ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹
Tactic:
convert theorem1_2C' K (by simp) h1 h2 hF hG h3 f hf <;> sorry
State after:
no goals

State before:
F G : Set ℝ
hF : MeasurableSet F
hG : MeasurableSet G
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ F.indicator 1 x
⊢ 4 ≤ 4
Tactic:
simp
State after:
no goals