Source indexedlemma · leanprover/lean4:v4.32.0

BKLNW.g_decreasing_interval

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW.lean:806 to 829

Source documentation

\subsection{Bounding theta(x)-x with a logarithmic decay, I: large x}

In this section and the next ones we obtain bounds of the shape $x \left(1 - \frac{m_k}{\log^k x}\right) \leq \theta(x)$ for all $x \geq X_0$ and $\theta(x) \leq x \left(1 + \frac{M_k}{\log^k x}\right)$ for all $x \geq X_1$ , for various $k, m_k, M_k, X_0, X_1$ , with $k \in \{1,\dots,5\}$ .

For this section we focus on estimates that are useful when $x$ is extremely large, e.g., $x \geq e^{25000}$ . -/

/- Show that the function g in the proof of the following lemma is decreasing

Exact Lean statement

lemma g_decreasing_interval (A C : ℝ) (hA : 0 < A) (hC : 0 < C) (u v : ℝ) (hu : 4 * A ^ 2 / C ^ 2 ≤ u) (huv : u ≤ v) :
    v ^ A * Real.exp (-C * Real.sqrt v) ≤ u ^ A * Real.exp (-C * Real.sqrt u)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma g_decreasing_interval (A C : ℝ) (hA : 0 < A) (hC : 0 < C) (u v : ℝ) (hu : 4 * A ^ 2 / C ^ 2 ≤ u) (huv : u ≤ v) :    v ^ A * Real.exp (-C * Real.sqrt v) ≤ u ^ A * Real.exp (-C * Real.sqrt u) := by      -- Let $f(t) = t^A e^{-C\sqrt{t}}$. The derivative is $f'(t) = t^{A-1} e^{-C\sqrt{t}} (A - \frac{C}{2}\sqrt{t})$.      set f := fun t : ℝ => t ^ A * Real.exp (-C * Real.sqrt t)      have h_deriv : ∀ t > 0, deriv f t = t ^ (A - 1) * Real.exp (-C * Real.sqrt t) * (A - C / 2 * Real.sqrt t) := by        intro t ht; norm_num [ f, ht.ne', Real.sqrt_eq_rpow, Real.rpow_sub ht ]        rw [deriv_fun_mul, Real.deriv_rpow_const, _root_.deriv_exp]        · simp only [deriv.fun_neg', deriv_const_mul_field',          Real.deriv_rpow_const, mul_neg]          rw [rpow_sub_one (by linarith), rpow_sub_one (by linarith)]          ring        all_goals fun_prop (disch := linarith)      -- Since $4A^2/C^2 \le u \le v$, we have $f'(t) \le 0$ for $t \ge 4A^2/C^2$.      have h_deriv_nonpos : ∀ t > 0, 4 * A ^ 2 / C ^ 2 ≤ t → deriv f t ≤ 0 := by        intro t ht ht'; rw [ h_deriv t ht ] ; exact mul_nonpos_of_nonneg_of_nonpos ( mul_nonneg ( Real.rpow_nonneg ht.le _ ) ( Real.exp_nonneg _ ) ) ( sub_nonpos_of_le <| by rw [ div_le_iff₀ <| by positivity ] at *; nlinarith [ show 0 ≤ Real.sqrt t * C by positivity, Real.mul_self_sqrt ht.le ] ) ;      by_contra h_contra;      -- Apply the mean value theorem to $f$ on the interval $[u, v]$.      obtain ⟨c, hc⟩ : ∃ c ∈ Set.Ioo u v, deriv f c = (f v - f u) / (v - u) := by        apply_rules [ exists_deriv_eq_slope ];        · exact huv.lt_of_ne ( by rintro rfl; linarith );        · exact continuousOn_of_forall_continuousAt fun t ht => ContinuousAt.mul ( ContinuousAt.rpow continuousAt_id continuousAt_const <| Or.inr <| by linarith ) <| ContinuousAt.rexp <| ContinuousAt.mul continuousAt_const <| Real.continuous_sqrt.continuousAt;        · exact fun x hx => DifferentiableAt.differentiableWithinAt ( by exact DifferentiableAt.mul ( DifferentiableAt.rpow ( differentiableAt_id ) ( by norm_num ) ( by linarith [ hx.1, show 0 < u by exact lt_of_lt_of_le ( by positivity ) hu ] ) ) ( DifferentiableAt.exp ( DifferentiableAt.mul ( differentiableAt_const _ ) ( DifferentiableAt.sqrt ( differentiableAt_id ) ( by linarith [ hx.1, show 0 < u by exact lt_of_lt_of_le ( by positivity ) hu ] ) ) ) ) );      simp +zetaDelta only [gt_iff_lt, neg_mul, ge_iff_le, not_le, Set.mem_Ioo] at *      rw [ eq_div_iff ] at hc <;> nlinarith [ h_deriv_nonpos c ( by linarith [ show 0 < u by exact lt_of_lt_of_le ( by positivity ) hu ] ) ( by linarith ) ]