have bnd := UpperBnd_aux5 t_ge hσ.2
σ 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| ^ (-σ)
σ 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| ^ (-σ)