Source indexedlemma · leanprover/lean4:v4.32.0

BKLNW.C_bk_S_antitone

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_tables · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_tables.lean:1269 to 1280

Source documentation

C_bk_S is antitone in b (for nonnegative c, C): each exp term decreases.

Exact Lean statement

lemma C_bk_S_antitone {b b' c C : ℝ} (hbb : b' ≤ b) (hc : 0 ≤ c) (hC : 0 ≤ C) :
    C_bk_S b c C ≤ C_bk_S b' c C

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma C_bk_S_antitone {b b' c C : ℝ} (hbb : b' ≤ b) (hc : 0 ≤ c) (hC : 0 ≤ C) :    C_bk_S b c C ≤ C_bk_S b' c C := by  have hc0 : (0 : ℝ) ≤ RS_prime.c₀ := by norm_num [RS_prime.c₀]  have m1 := mul_le_mul_of_nonneg_left (exp_le_exp.mpr (by linarith : -b / 2 ≤ -b' / 2))    (by linarith : (0 : ℝ) ≤ C + 1)  have m2 := mul_le_mul_of_nonneg_left    (exp_le_exp.mpr (by linarith : -2 * b / 3 ≤ -2 * b' / 3)) hc0  have m3 := mul_le_mul_of_nonneg_left    (exp_le_exp.mpr (by linarith : -3 * b / 4 ≤ -3 * b' / 4)) hc  have m4 := mul_le_mul_of_nonneg_left    (exp_le_exp.mpr (by linarith : -4 * b / 5 ≤ -4 * b' / 5)) hc0  unfold C_bk_S; linarith