apply le_trans this ?_
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t| ^ (1 - σ) ≤ A.exp
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t| ^ (A / |t|.log) ≤ A.exp