Source indexedlemma · leanprover/lean4:v4.32.0

BKLNW.pTdd_nonneg

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:573 to 586

Mathematical statement

Exact Lean statement

lemma pTdd_nonneg {c : ℝ} (hc : 1 / 2 ≤ c) {m : ℕ} (hm : m ≤ 3) {y : ℝ} (hy20 : 20 ≤ y) :
    0 ≤ pTdd m c y

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma pTdd_nonneg {c : ℝ} (hc : 1 / 2 ≤ c) {m : ℕ} (hm : m ≤ 3) {y : ℝ} (hy20 : 20 ≤ y) :    0 ≤ pTdd m c y := by  unfold pTdd  apply mul_nonneg _ (Real.exp_pos _).le  have hM0 : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m  have hM3 : (m : ℝ) ≤ 3 := by exact_mod_cast hm  have hym : (0 : ℝ) ≤ y ^ m := pow_nonneg (by linarith) m  push_cast  have hfac : c ^ 2 * y ^ (m + 2) - 2 * c * ((m : ℝ) + 2) * y ^ (m + 1)        + ((m : ℝ) + 2) * ((m : ℝ) + 1) * y ^ m      = y ^ m * (c ^ 2 * y ^ 2 - 2 * c * ((m : ℝ) + 2) * y + ((m : ℝ) + 2) * ((m : ℝ) + 1)) := by    ring  rw [hfac]  exact mul_nonneg hym (quad_nonneg hc hy20 hM0 hM3)