Source indexedlemma · leanprover/lean4:v4.32.0

FKS2.sixty_thousand_mul_exp_neg_230_le

PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:891 to 900

Source documentation

Purely numerical tail bound used at the end: 60000 * exp (-230) ≤ 1e-5. This can be discharged by interval_decide.

Exact Lean statement

lemma sixty_thousand_mul_exp_neg_230_le :
    (60000 : ℝ) * Real.exp (-230) ≤ (1e-5 : ℝ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma sixty_thousand_mul_exp_neg_230_le :    (60000 : ℝ) * Real.exp (-230) ≤ (1e-5 : ℝ) := by  have h_exp : Real.exp (-230) ≤ BKLNW.exp_neg_one_ub ^ (100 : ℕ) := by    simpa using (BKLNW.exp_neg_le_pow (n := 100) (x := 230) (by norm_num))  have h_mul :      (60000 : ℝ) * Real.exp (-230) ≤ 60000 * BKLNW.exp_neg_one_ub ^ (100 : ℕ) := by    exact mul_le_mul_of_nonneg_left h_exp (by norm_num)  have h_num : 60000 * BKLNW.exp_neg_one_ub ^ (100 : ℕ) ≤ (1e-5 : ℝ) := by    norm_num [BKLNW.exp_neg_one_ub]  exact h_mul.trans h_num