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

State before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ε * MeasureTheory.volume E ≤ ENNReal.ofReal (δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹) * MeasureTheory.volume E ^ 2⁻¹
Tactic:
rw [ENNReal.ofReal_mul (by apply mul_nonneg δpos.le; rw [C1_2]; norm_num), ← ENNReal.ofReal_rpow_of_pos (by linarith [Real.pi_pos])]
State after:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ε * MeasureTheory.volume E ≤
    ENNReal.ofReal (δ * C1_2 4 2) * ENNReal.ofReal (4 * Real.pi) ^ 2⁻¹ * MeasureTheory.volume E ^ 2⁻¹

State before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ε * MeasureTheory.volume E ≤
    ENNReal.ofReal (δ * C1_2 4 2) * ENNReal.ofReal (4 * Real.pi) ^ 2⁻¹ * MeasureTheory.volume E ^ 2⁻¹
Tactic:
convert rcarleson_exceptional_set_estimate δpos measurableSet_Icc hf measurableSetE hE
State after:
case h.e'_4.h.e'_5.h.e'_6.h.e'_5
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal (4 * Real.pi) = MeasureTheory.volume (Set.Icc (-Real.pi) (3 * Real.pi))

State before:
case h.e'_4.h.e'_5.h.e'_6.h.e'_5
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal (4 * Real.pi) = MeasureTheory.volume (Set.Icc (-Real.pi) (3 * Real.pi))
Tactic:
rw [Real.volume_Icc]
State after:
case h.e'_4.h.e'_5.h.e'_6.h.e'_5
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal (4 * Real.pi) = ENNReal.ofReal (3 * Real.pi - -Real.pi)

State before:
case h.e'_4.h.e'_5.h.e'_6.h.e'_5
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ ENNReal.ofReal (4 * Real.pi) = ENNReal.ofReal (3 * Real.pi - -Real.pi)
Tactic:
ring_nf
State after:
no goals

State before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ 0 ≤ δ * C1_2 4 2
Tactic:
apply mul_nonneg δpos.le
State after:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ 0 ≤ C1_2 4 2

State before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ 0 ≤ C1_2 4 2
Tactic:
rw [C1_2]
State after:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ 0 ≤ 2 ^ (450 * 4 ^ 3) / (2 - 1) ^ 5

State before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ 0 ≤ 2 ^ (450 * 4 ^ 3) / (2 - 1) ^ 5
Tactic:
norm_num
State after:
no goals

State before:
δ : ℝ
δpos : 0 < δ
f : ℝ → ℂ
hf : ∀ (x : ℝ), ‖f x‖ ≤ δ * (Set.Icc (-Real.pi) (3 * Real.pi)).indicator 1 x
E : Set ℝ
measurableSetE : MeasurableSet E
ε : ENNReal
hE : ∀ x ∈ E, ε ≤ T' f x
⊢ 0 < 4 * Real.pi
Tactic:
linarith [Real.pi_pos]
State after:
no goals