Source indexedlemma · leanprover/lean4:v4.32.0

FKS2.ratio_eq_g

PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:2197 to 2208

Source documentation

We obtain our final bound for converting bounds on $E_\theta$ to bounds on $E_\pi$ . -/

/- The following lemmas are used for theorem_3. -/

-- Helper: admissible_bound is linear in A lemma admissible_bound_mul (A K B C R x : ℝ) : admissible_bound (A * K) B C R x = K * admissible_bound A B C R x := by simp [admissible_bound]; ring

/- Helper: the ratio log x / (x * admissible_bound A B C R x) equals R^B / A * g_bound 1 (1-B) (C/√R) x

Exact Lean statement

lemma ratio_eq_g {A B C R x : ℝ}
    (hR : R > 0) (hx : x > 0) (hlogx : log x > 0) :
    log x / (x * admissible_bound A B C R x) =
    R ^ B / A * g_bound 1 (1 - B) (C / sqrt R) x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ratio_eq_g {A B C R x : ℝ}    (hR : R > 0) (hx : x > 0) (hlogx : log x > 0) :    log x / (x * admissible_bound A B C R x) =    R ^ B / A * g_bound 1 (1 - B) (C / sqrt R) x := by  unfold admissible_bound g_bound; ring_nf;  rw [ Real.mul_rpow ( by positivity ) ( by positivity ), Real.inv_rpow ( by positivity ) ] ; norm_num [ Real.rpow_sub, Real.rpow_neg, Real.sqrt_mul, hR.le, hx.le, hlogx.le ] ; ring_nf;  rw [ Real.rpow_sub hlogx, Real.rpow_one ] ; norm_num [ Real.exp_neg ] ; ring_nf;  next =>    norm_num    left    rw [show (log x * R⁻¹) ^ (1 / 2 : ℝ) = Real.sqrt (log x * R⁻¹) by rw [Real.sqrt_eq_rpow]]    rw [Real.sqrt_mul, Real.sqrt_inv] <;> linarith