Source indexedlemma · leanprover/lean4:v4.32.0

FKS2.log_div_self_mul_integral_le_of_ge

PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3261 to 3267

Mathematical statement

Exact Lean statement

lemma log_div_self_mul_integral_le_of_ge {x₁ : ℝ} (hx₁ : 14 ≤ x₁) {y : ℝ} (hy : x₁ ≤ y) :
    (Real.log y / y) * ∫ s in x₁..y, 1 / (Real.log s) ^ 2 ≤ (Real.log x₁ / (Real.log x₁ - 2)) / Real.log y

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma log_div_self_mul_integral_le_of_ge {x₁ : ℝ} (hx₁ : 14 ≤ x₁) {y : ℝ} (hy : x₁ ≤ y) :    (Real.log y / y) * ∫ s in x₁..y, 1 / (Real.log s) ^ 2 ≤ (Real.log x₁ / (Real.log x₁ - 2)) / Real.log y := by  have hlogy_pos : 0 < Real.log y := Real.log_pos ((by linarith : 1 < x₁).trans_le hy)  refine (mul_le_mul_of_nonneg_left (integral_one_div_log_sq_le_of_ge hx₁ hy)      (div_nonneg hlogy_pos.le (by linarith))).trans_eq ?_  have hlogx₁_gt : 2 < Real.log x₁ := log_gt_two_of_ge_14 hx₁  field_simp [show Real.log x₁ - 2 ≠ 0 by linarith, hlogy_pos.ne', show y ≠ 0 by linarith]