Source indexedlemma · leanprover/lean4:v4.32.0

UpperBnd_aux2

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1528 to 1536

Mathematical statement

Exact Lean statement

lemma UpperBnd_aux2 {A σ t : ℝ} (t_ge : 3 < |t|) (σ_ge : 1 - A / Real.log |t| ≤ σ) :
      |t| ^ (1 - σ) ≤ Real.exp A

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma UpperBnd_aux2 {A σ t : ℝ} (t_ge : 3 < |t|) (σ_ge : 1 - A / Real.log |t| ≤ σ) :      |t| ^ (1 - σ) ≤ Real.exp A := by  have : |t| ^ (1 - σ) ≤ |t| ^ (A / Real.log |t|) :=    Real.rpow_le_rpow_of_exponent_le (by linarith) (by linarith)  apply le_trans this ?_  conv => lhs; lhs; rw [← Real.exp_log (by linarith : 0 < |t|)]  rw [div_eq_mul_inv, Real.rpow_mul (by positivity), ← Real.exp_mul, ← Real.exp_mul, mul_comm,    ← mul_assoc, inv_mul_cancel₀, one_mul]  apply Real.log_ne_zero.mpr; split_ands <;> linarith