Theorem: UpperBnd_aux6 (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2 ∧
    ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ) ∧ ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
Tactic:
have bnd := UpperBnd_aux5 t_ge hσ.2
State after:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2 ∧
    ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ) ∧ ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)

State before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2 ∧
    ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ) ∧ ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
Tactic:
have bnd' : (|t| / ⌊|t|⌋₊) ^ σ ≤ 2 * |t| := by linarith
State after:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2 ∧
    ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ) ∧ ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)

State before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2 ∧
    ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ) ∧ ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
Tactic:
split_ands
State after:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2

case refine_2.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ)

case refine_2.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)

State before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
⊢ (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
Tactic:
linarith
State after:
no goals

State before:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2
Tactic:
apply (div_le_iff <| norm_pos_iff.mpr <| sub_ne_zero_of_ne neOne.symm).mpr
State after:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) ≤ |t| ^ (1 - σ) * 2 * ‖1 - (↑σ + ↑t * I)‖

State before:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) ≤ |t| ^ (1 - σ) * 2 * ‖1 - (↑σ + ↑t * I)‖
Tactic:
conv => rw [mul_assoc]; rhs; rw [mul_comm]
State after:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) ≤ 2 * ‖1 - (↑σ + ↑t * I)‖ * |t| ^ (1 - σ)

State before:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) ≤ 2 * ‖1 - (↑σ + ↑t * I)‖ * |t| ^ (1 - σ)
Tactic:
apply (div_le_iff <| Real.rpow_pos_of_pos (by linarith) _).mp
State after:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) / |t| ^ (1 - σ) ≤ 2 * ‖1 - (↑σ + ↑t * I)‖

State before:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (1 - σ) / |t| ^ (1 - σ) ≤ 2 * ‖1 - (↑σ + ↑t * I)‖
Tactic:
rw [div_rpow_eq_rpow_div_neg (by positivity) (by positivity), neg_sub]
State after:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ (|t| / ↑⌊|t|⌋₊) ^ (σ - 1) ≤ 2 * ‖1 - (↑σ + ↑t * I)‖

State before:
case refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ (|t| / ↑⌊|t|⌋₊) ^ (σ - 1) ≤ 2 * ‖1 - (↑σ + ↑t * I)‖
Tactic:
refine le_trans₄ ?_ bnd' ?_
State after:
case refine_1.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ (|t| / ↑⌊|t|⌋₊) ^ (σ - 1) ≤ (|t| / ↑⌊|t|⌋₊) ^ σ

case refine_1.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 2 * |t| ≤ 2 * ‖1 - (↑σ + ↑t * I)‖

State before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 0 < |t|
Tactic:
linarith
State after:
no goals

State before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 0 ≤ ↑⌊|t|⌋₊
Tactic:
positivity
State after:
no goals

State before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 0 ≤ |t|
Tactic:
positivity
State after:
no goals

State before:
case refine_1.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ (|t| / ↑⌊|t|⌋₊) ^ (σ - 1) ≤ (|t| / ↑⌊|t|⌋₊) ^ σ
Tactic:
exact Real.rpow_le_rpow_of_exponent_le (one_le_div (by positivity) |>.mpr N_le_t) (by simp)
State after:
no goals

State before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 0 < ↑⌊|t|⌋₊
Tactic:
positivity
State after:
no goals

State before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ σ - 1 ≤ σ
Tactic:
simp
State after:
no goals

State before:
case refine_1.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 2 * |t| ≤ 2 * ‖1 - (↑σ + ↑t * I)‖
Tactic:
apply (mul_le_mul_left (by norm_num)).mpr
State after:
case refine_1.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ |t| ≤ ‖1 - (↑σ + ↑t * I)‖

State before:
case refine_1.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ |t| ≤ ‖1 - (↑σ + ↑t * I)‖
Tactic:
simpa using abs_im_le_abs (1 - (σ + t * I))
State after:
no goals

State before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
case refine_2.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ)
Tactic:
apply div_le_iff (by norm_num) |>.mpr
State after:
case refine_2.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) ≤ |t| ^ (1 - σ) * 2

State before:
case refine_2.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) ≤ |t| ^ (1 - σ) * 2
Tactic:
rw [Real.rpow_sub (by linarith), Real.rpow_one, div_mul_eq_mul_div, mul_comm]
State after:
case refine_2.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) ≤ 2 * |t| / |t| ^ σ

State before:
case refine_2.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) ≤ 2 * |t| / |t| ^ σ
Tactic:
apply div_le_iff (by positivity) |>.mp
State after:
case refine_2.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / (|t| ^ σ)⁻¹ ≤ 2 * |t|

State before:
case refine_2.refine_1
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / (|t| ^ σ)⁻¹ ≤ 2 * |t|
Tactic:
convert bnd' using 1
State after:
case h.e'_3
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / (|t| ^ σ)⁻¹ = (|t| / ↑⌊|t|⌋₊) ^ σ

State before:
case h.e'_3
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / (|t| ^ σ)⁻¹ = (|t| / ↑⌊|t|⌋₊) ^ σ
Tactic:
rw [← Real.rpow_neg (by linarith), div_rpow_neg_eq_rpow_div (by positivity) (by positivity)]
State after:
no goals

State before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 0 < (|t| ^ σ)⁻¹
Tactic:
positivity
State after:
no goals

State before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 0 ≤ |t|
Tactic:
linarith
State after:
no goals

State before:
case refine_2.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
Tactic:
apply div_le_iff (by linarith [hσ.1]) |>.mpr
State after:
case refine_2.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) ≤ 8 * |t| ^ (-σ) * σ

State before:
case refine_2.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) ≤ 8 * |t| ^ (-σ) * σ
Tactic:
rw [mul_assoc, mul_comm, mul_assoc]
State after:
case refine_2.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) ≤ |t| ^ (-σ) * (σ * 8)

State before:
case refine_2.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) ≤ |t| ^ (-σ) * (σ * 8)
Tactic:
apply div_le_iff' (by positivity) |>.mp
State after:
case refine_2.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / |t| ^ (-σ) ≤ σ * 8

State before:
case refine_2.refine_2
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / |t| ^ (-σ) ≤ σ * 8
Tactic:
apply le_trans ?_ (by linarith [hσ.1] : 4 ≤ σ * 8)
State after:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / |t| ^ (-σ) ≤ 4

State before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / |t| ^ (-σ) ≤ 4
Tactic:
convert bnd using 1
State after:
case h.e'_3
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / |t| ^ (-σ) = (|t| / ↑⌊|t|⌋₊) ^ σ

State before:
case h.e'_3
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ ↑⌊|t|⌋₊ ^ (-σ) / |t| ^ (-σ) = (|t| / ↑⌊|t|⌋₊) ^ σ
Tactic:
exact div_rpow_neg_eq_rpow_div (by positivity) (by positivity)
State after:
no goals

State before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 0 < σ
Tactic:
linarith [hσ.1]
State after:
no goals

State before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 0 < |t| ^ (-σ)
Tactic:
positivity
State after:
no goals

State before:
σ t : ℝ
t_ge : 3 < |t|
hσ : σ ∈ Ioc (1 / 2) 2
neOne : ↑σ + ↑t * I ≠ 1
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
bnd : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
bnd' : (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 2 * |t|
⊢ 4 ≤ σ * 8
Tactic:
linarith [hσ.1]
State after:
no goals