Source indexedlemma · leanprover/lean4:v4.32.0

PT.admissible_bound_weaken

PrimeNumberTheoremAnd.IEANTN.SecondarySummary · PrimeNumberTheoremAnd/IEANTN/SecondarySummary.lean:65 to 88

Mathematical statement

Exact Lean statement

lemma admissible_bound_weaken {A B C x : ℝ}
    (hB : 3 / 2 ≤ B) (hB2 : B ≤ 2)
    (_hC : 0 ≤ C) (hCR : C ^ 2 * 5.5666305 ≤ 4 * 5.573412)
    (hA : 122 ≤ A)
    (hlogx : 5.5666305 ≤ log x) :
    admissible_bound 121.0961 (3 / 2) 2 5.5666305 x ≤ admissible_bound A B C 5.573412 x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma admissible_bound_weaken {A B C x : ℝ}    (hB : 3 / 2 ≤ B) (hB2 : B ≤ 2)    (_hC : 0 ≤ C) (hCR : C ^ 2 * 5.5666305 ≤ 4 * 5.573412)    (hA : 122 ≤ A)    (hlogx : 5.5666305 ≤ log x) :    admissible_bound 121.0961 (3 / 2) 2 5.5666305 x ≤ admissible_bound A B C 5.573412 x := by  refine mul_le_mul ?_ ?_ ?_ ?_ <;> try positivity  · have h_exp : (log x / 5.5666305) ^ (3 / 2 : ℝ) ≤        (log x / 5.573412) ^ B * ((5.573412 / 5.5666305) ^ B) := by      rw [← Real.mul_rpow (div_nonneg (by linarith) (by norm_num)) (by norm_num)]      ring_nf at *; norm_num at *      exact Real.rpow_le_rpow_of_exponent_le (by linarith) (by linarith)    have h_div : 121.0961 * ((5.573412 / 5.5666305) ^ B) ≤ A :=      le_trans (mul_le_mul_of_nonneg_left        (Real.rpow_le_rpow_of_exponent_le (by norm_num) hB2) (by norm_num))        (by norm_num; linarith)    nlinarith [Real.rpow_pos_of_pos      (show 0 < log x / 5.573412 from div_pos (lt_of_lt_of_le (by norm_num) hlogx) (by norm_num)) B]  · norm_num at *    rw [← Real.sqrt_eq_rpow, ← Real.sqrt_eq_rpow] at *    nlinarith [Real.sqrt_nonneg (log x / (11133261 / 2000000)),      Real.mul_self_sqrt (by linarith : 0 ≤ log x / (11133261 / 2000000)),      Real.sqrt_nonneg (log x / (1393353 / 250000)),      Real.mul_self_sqrt (by linarith : 0 ≤ log x / (1393353 / 250000))]