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

State before:
ε : ℝ
εpos : 0 < ε
⊢ Real.pi < C_control_approximation_effect ε
Tactic:
rw [C_control_approximation_effect]
State after:
ε : ℝ
εpos : 0 < ε
⊢ Real.pi < C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹ + Real.pi

State before:
ε : ℝ
εpos : 0 < ε
⊢ Real.pi < C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹ + Real.pi
Tactic:
apply lt_add_of_pos_of_le _ (by rfl)
State after:
ε : ℝ
εpos : 0 < ε
⊢ 0 < C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹

State before:
ε : ℝ
εpos : 0 < ε
⊢ 0 < C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹
Tactic:
apply mul_pos (C1_2_pos (by norm_num))
State after:
ε : ℝ
εpos : 0 < ε
⊢ 0 < (8 / (Real.pi * ε)) ^ 2⁻¹

State before:
ε : ℝ
εpos : 0 < ε
⊢ 0 < (8 / (Real.pi * ε)) ^ 2⁻¹
Tactic:
apply Real.rpow_pos_of_pos
State after:
case hx
ε : ℝ
εpos : 0 < ε
⊢ 0 < 8 / (Real.pi * ε)

State before:
case hx
ε : ℝ
εpos : 0 < ε
⊢ 0 < 8 / (Real.pi * ε)
Tactic:
apply div_pos (by norm_num)
State after:
case hx
ε : ℝ
εpos : 0 < ε
⊢ 0 < Real.pi * ε

State before:
case hx
ε : ℝ
εpos : 0 < ε
⊢ 0 < Real.pi * ε
Tactic:
apply mul_pos Real.pi_pos εpos
State after:
no goals

State before:
ε : ℝ
εpos : 0 < ε
⊢ Real.pi ≤ Real.pi
Tactic:
rfl
State after:
no goals

State before:
ε : ℝ
εpos : 0 < ε
⊢ 1 < 2
Tactic:
norm_num
State after:
no goals

State before:
ε : ℝ
εpos : 0 < ε
⊢ 0 < 8
Tactic:
norm_num
State after:
no goals