Source indexedtheorem · leanprover/lean4:v4.32.0

Ramanujan.criterion

PrimeNumberTheoremAnd.IEANTN.Ramanujan.Ramanujan · PrimeNumberTheoremAnd/IEANTN/Ramanujan/Ramanujan.lean:434 to 494

Mathematical statement

Exact Lean statement

@[blueprint
  "ramanujan-criterion"
  (title := "Criterion for Ramanujan's inequality")
  (statement := /-- \cite[Lemma 2.1]{dudek-platt}
Let $m_a, M_a \in \mathbb{R}$  and suppose that for $x>x_a$ we have
$$ x \sum_{k=0}^{4} \frac{k!}{\log^{k+1}x}+ \frac{m_a x}{\log^6 x} < \pi(x)$$

and for $x > ex_a$ one has
$$ \pi(x) < x \sum_{k=0}^{4} \frac{k!}{\log^{k+1}x}+\frac{M_a x}{\log^6 x}.$$
%
Then Ramanujan's inequality is true for $x > x_0$ if

$$x_0 ≥ e x_{a}$$
and
$$ \epsilon_{M_a} (x_0) - \epsilon'_{m_a}(x_0) < \log x.$$
 -/)
  (proof := /-- Combine the previous two sublemmas.
 -/)
  (latexEnv := "proposition")
  (discussion := 985)]
theorem criterion (mₐ Mₐ xₐ x₀ : ℝ)
  (hxₐ : 1 < xₐ)
  (hlower : ∀ x > xₐ, x * ∑ k ∈ Finset.range 5, (k.factorial / log x ^ (k + 1)) + (mₐ * x / log x ^ 6) < pi x)
  (hupper : ∀ x > exp 1 * xₐ, pi x < x * ∑ k ∈ Finset.range 5, (k.factorial / log x ^ (k + 1)) + (Mₐ * x / log x ^ 6))
  (hx₀xₐ : x₀ ≥ exp 1 * xₐ)
  (hcrit : ∀ ⦃x : ℝ⦄, x > x₀ → ε Mₐ x - εlower mₐ xₐ x < log x) :
    ∀ x > x₀, pi x ^ 2 < exp 1 * x / log x * pi (x / exp 1)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "ramanujan-criterion"  (title := "Criterion for Ramanujan's inequality")  (statement := /-- \cite[Lemma 2.1]{dudek-platt}Let $m_a, M_a \in \mathbb{R}$  and suppose that for $x>x_a$ we have$$ x \sum_{k=0}^{4} \frac{k!}{\log^{k+1}x}+ \frac{m_a x}{\log^6 x} < \pi(x)$$ and for $x > ex_a$ one has$$ \pi(x) < x \sum_{k=0}^{4} \frac{k!}{\log^{k+1}x}+\frac{M_a x}{\log^6 x}.$$%Then Ramanujan's inequality is true for $x > x_0$ if $$x_0 ≥ e x_{a}$$and$$ \epsilon_{M_a} (x_0) - \epsilon'_{m_a}(x_0) < \log x.$$ -/)  (proof := /-- Combine the previous two sublemmas. -/)  (latexEnv := "proposition")  (discussion := 985)]theorem criterion (mₐ Mₐ xₐ x₀ : ℝ)  (hxₐ : 1 < xₐ)  (hlower : ∀ x > xₐ, x * ∑ k ∈ Finset.range 5, (k.factorial / log x ^ (k + 1)) + (mₐ * x / log x ^ 6) < pi x)  (hupper : ∀ x > exp 1 * xₐ, pi x < x * ∑ k ∈ Finset.range 5, (k.factorial / log x ^ (k + 1)) + (Mₐ * x / log x ^ 6))  (hx₀xₐ : x₀ ≥ exp 1 * xₐ)  (hcrit : ∀ ⦃x : ℝ⦄, x > x₀ → ε Mₐ x - εlower mₐ xₐ x < log x) :    ∀ x > x₀, pi x ^ 2 < exp 1 * x / log x * pi (x / exp 1) := by  intro x hx  have hxexₐ : x > exp 1 * xₐ := lt_of_le_of_lt hx₀xₐ hx  have hsq := sq_pi_lt Mₐ (exp 1 * xₐ) hupper x hxexₐ  have hlow := ex_pi_gt mₐ xₐ hxₐ hlower x hxexₐ  let U : ℝ := 1 / log x ^ 2 + 2 / log x ^ 3 + 5 / log x ^ 4 + 16 / log x ^ 5 + 64 / log x ^ 6 +    ε Mₐ x / log x ^ 7  let L : ℝ := 1 / log x ^ 2 + 2 / log x ^ 3 + 5 / log x ^ 4 + 16 / log x ^ 5 + 65 / log x ^ 6 +    εlower mₐ xₐ x / log x ^ 7  have hsq' : pi x ^ 2 < x ^ 2 * U := by    simpa [U] using hsq  have hlow' : x ^ 2 * L < exp 1 * x / log x * pi (x / exp 1) := by    simpa [L] using hlow  have hx_gt_e : exp 1 < x := by    have h1 : exp 1 < exp 1 * xₐ := by      nlinarith [hxₐ, exp_pos (1 : ℝ)]    exact lt_of_lt_of_le h1 (le_of_lt hxexₐ)  have hlog_pos : 0 < log x :=    log_pos (lt_trans ((Real.one_lt_exp_iff).2 (by norm_num)) hx_gt_e)  have hnum_neg : ε Mₐ x - εlower mₐ xₐ x - log x < 0 := by    linarith [hcrit hx]  have hden_pos : 0 < log x ^ 7 := by positivity  have hlog_ne : log x ≠ 0 := ne_of_gt hlog_pos  have hUL_eq : U - L = (ε Mₐ x - εlower mₐ xₐ x - log x) / log x ^ 7 := by    simp [U, L]    field_simp [hlog_ne]    ring  have hUL_neg : U - L < 0 := by    rw [hUL_eq]    exact div_neg_of_neg_of_pos hnum_neg hden_pos  have hU_lt_L : U < L := by linarith  have hx_pos : 0 < x := lt_trans (by positivity : 0 < exp 1 * xₐ) hxexₐ  have hmul : x ^ 2 * U < x ^ 2 * L :=    mul_lt_mul_of_pos_left hU_lt_L (sq_pos_of_pos hx_pos)  exact lt_trans hsq' (lt_trans hmul hlow')