Theorem: rcarleson_exceptional_set_estimate (Carleson/Theorem1_1/Control_Approximation_Effect.lean)

State before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ε * MeasureTheory.volume E ≤
    ENNReal.ofReal (δ * C1_2 4 2) * MeasureTheory.volume F ^ 2⁻¹ * MeasureTheory.volume E ^ 2⁻¹
Tactic:
calc ε * MeasureTheory.volume E
  _ = ∫⁻ _ in E, ε := by
    symm
    apply MeasureTheory.set_lintegral_const
  _ ≤ ∫⁻ x in E, T' f x := by
    apply MeasureTheory.set_lintegral_mono' measurableSetE hE
  _ = ENNReal.ofReal δ * ∫⁻ x in E, T' (fun x ↦ (1 / δ) * f x) x := by
    rw [← MeasureTheory.lintegral_const_mul']
    congr
    ext x
    rw [CarlesonOperatorReal'_mul δpos]
    congr
    exact ENNReal.ofReal_ne_top
  _ ≤ ENNReal.ofReal δ * (ENNReal.ofReal (C1_2 4 2) * (MeasureTheory.volume E) ^ (2 : ℝ)⁻¹ * (MeasureTheory.volume F) ^ (2 : ℝ)⁻¹) := by
    gcongr
    apply rcarleson' measurableSetF measurableSetE
    intro x
    simp
    rw [_root_.abs_of_nonneg δpos.le, inv_mul_le_iff δpos]
    exact hf x
  _ = ENNReal.ofReal (δ * C1_2 4 2) * (MeasureTheory.volume F) ^ (2 : ℝ)⁻¹ * (MeasureTheory.volume E) ^ (2 : ℝ)⁻¹ := by
    rw [ENNReal.ofReal_mul δpos.le]
    ring
State after:
no goals

State before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ε * MeasureTheory.volume E = ∫⁻ (x : ℝ) in E, ε
Tactic:
symm
State after:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∫⁻ (x : ℝ) in E, ε = ε * MeasureTheory.volume E

State before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∫⁻ (x : ℝ) in E, ε = ε * MeasureTheory.volume E
Tactic:
apply MeasureTheory.set_lintegral_const
State after:
no goals

State before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∫⁻ (x : ℝ) in E, ε ≤ ∫⁻ (x : ℝ) in E, T' f x
Tactic:
apply MeasureTheory.set_lintegral_mono' measurableSetE hE
State after:
no goals

State before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∫⁻ (x : ℝ) in E, T' f x = ENNReal.ofReal δ * ∫⁻ (x : ℝ) in E, T' (fun x => 1 / ↑δ * f x) x
Tactic:
rw [← MeasureTheory.lintegral_const_mul']
State after:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∫⁻ (x : ℝ) in E, T' f x = ∫⁻ (a : ℝ) in E, ENNReal.ofReal δ * T' (fun x => 1 / ↑δ * f x) a

case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤

State before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∫⁻ (x : ℝ) in E, T' f x = ∫⁻ (a : ℝ) in E, ENNReal.ofReal δ * T' (fun x => 1 / ↑δ * f x) a

case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤
Tactic:
congr
State after:
case e_f
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ (fun x => T' f x) = fun a => ENNReal.ofReal δ * T' (fun x => 1 / ↑δ * f x) a

case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤

State before:
case e_f
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ (fun x => T' f x) = fun a => ENNReal.ofReal δ * T' (fun x => 1 / ↑δ * f x) a

case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤
Tactic:
ext x
State after:
case e_f.h
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ T' f x = ENNReal.ofReal δ * T' (fun x => 1 / ↑δ * f x) x

case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤

State before:
case e_f.h
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ T' f x = ENNReal.ofReal δ * T' (fun x => 1 / ↑δ * f x) x

case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤
Tactic:
rw [CarlesonOperatorReal'_mul δpos]
State after:
case e_f.h
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ ↑δ.toNNReal * T' (fun x => 1 / ↑δ * f x) x = ENNReal.ofReal δ * T' (fun x => 1 / ↑δ * f x) x

case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤

State before:
case e_f.h
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ ↑δ.toNNReal * T' (fun x => 1 / ↑δ * f x) x = ENNReal.ofReal δ * T' (fun x => 1 / ↑δ * f x) x

case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤
Tactic:
congr
State after:
case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤

State before:
case hr
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ ≠ ⊤
Tactic:
exact ENNReal.ofReal_ne_top
State after:
no goals

State before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ * ∫⁻ (x : ℝ) in E, T' (fun x => 1 / ↑δ * f x) x ≤
    ENNReal.ofReal δ * (ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume E ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹)
Tactic:
gcongr
State after:
case bc
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∫⁻ (x : ℝ) in E, T' (fun x => 1 / ↑δ * f x) x ≤
    ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume E ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹

State before:
case bc
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∫⁻ (x : ℝ) in E, T' (fun x => 1 / ↑δ * f x) x ≤
    ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume E ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹
Tactic:
apply rcarleson' measurableSetF measurableSetE
State after:
case bc.hf
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∀ (x : ℝ), ‖1 / ↑δ * f x‖ ≤ F.indicator 1 x

State before:
case bc.hf
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ∀ (x : ℝ), ‖1 / ↑δ * f x‖ ≤ F.indicator 1 x
Tactic:
intro x
State after:
case bc.hf
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ ‖1 / ↑δ * f x‖ ≤ F.indicator 1 x

State before:
case bc.hf
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ ‖1 / ↑δ * f x‖ ≤ F.indicator 1 x
Tactic:
simp
State after:
case bc.hf
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ |δ|⁻¹ * Complex.abs (f x) ≤ F.indicator 1 x

State before:
case bc.hf
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ |δ|⁻¹ * Complex.abs (f x) ≤ F.indicator 1 x
Tactic:
rw [_root_.abs_of_nonneg δpos.le, inv_mul_le_iff δpos]
State after:
case bc.hf
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ Complex.abs (f x) ≤ δ * F.indicator 1 x

State before:
case bc.hf
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
x : ℝ
⊢ Complex.abs (f x) ≤ δ * F.indicator 1 x
Tactic:
exact hf x
State after:
no goals

State before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ * (ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume E ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹) =
    ENNReal.ofReal (δ * C1_2 4 2) * MeasureTheory.volume F ^ 2⁻¹ * MeasureTheory.volume E ^ 2⁻¹
Tactic:
rw [ENNReal.ofReal_mul δpos.le]
State after:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ * (ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume E ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹) =
    ENNReal.ofReal δ * ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume F ^ 2⁻¹ * MeasureTheory.volume E ^ 2⁻¹

State before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
F : Set ℝ
measurableSetF : MeasurableSet F
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * F.indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal δ * (ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume E ^ 2⁻¹ * MeasureTheory.volume F ^ 2⁻¹) =
    ENNReal.ofReal δ * ENNReal.ofReal (C1_2 4 2) * MeasureTheory.volume F ^ 2⁻¹ * MeasureTheory.volume E ^ 2⁻¹
Tactic:
ring
State after:
no goals