Source indexedlemma · leanprover/lean4:v4.32.0

ZetaInvBnd_aux2

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:2686 to 2702

Mathematical statement

Exact Lean statement

lemma ZetaInvBnd_aux2 {A C₁ C₂ : ℝ} (Apos : 0 < A) (C₁pos : 0 < C₁) (C₂pos : 0 < C₂)
    (hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ (4 : ℝ)) :
    0 < (C₁ * A ^ (3 / 4 : ℝ) - C₂ * 2 * A)⁻¹

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ZetaInvBnd_aux2 {A C₁ C₂ : ℝ} (Apos : 0 < A) (C₁pos : 0 < C₁) (C₂pos : 0 < C₂)    (hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ (4 : ℝ)) :    0 < (C₁ * A ^ (3 / 4 : ℝ) - C₂ * 2 * A)⁻¹ := by  simp only [inv_pos, sub_pos]  apply div_lt_iff₀ (by positivity) |>.mp  rw [div_eq_mul_inv, ← Real.rpow_neg (by positivity), mul_assoc]  apply lt_div_iff₀' (by positivity) |>.mp  nth_rewrite 1 [← Real.rpow_one A]  rw [← Real.rpow_add (by positivity)]  norm_num  apply Real.rpow_lt_rpow_iff (z := 4) (by positivity) (by positivity) (by positivity) |>.mp  rw [← Real.rpow_mul (by positivity)]  norm_num  apply lt_of_le_of_lt hA  rw [div_mul_comm, mul_one, Real.rpow_ofNat]  apply half_lt_self  positivity