Chebyshev.psi_num

@[blueprint  "psi-num"  (title := "Numerical bound for $\\psi(x)$ for very small $x$")  (statement := /-- For $0 < x \leq 30$, we have $\psi(x) \leq 1.015 x$. -/)  (proof := /-- Numerical check (the maximum occurs at $x=19$).  One only needs to check the case when $x$ is a prime power.-/)  (latexEnv := "sublemma")]theorem psi_num (x : ℝ) (hx : x > 0) (hx2 : x ≤ 30) : ψ x ≤ 1.015 * x := by  suffices ∀ n ∈ Icc (0 : ℕ) 30, ψ n ≤ 1.015 * n by    rw [psi_eq_psi_coe_floor]    grw [this]    · gcongr      exact Nat.floor_le hx.le    · simp only [mem_Icc, zero_le, true_and]      exact Nat.floor_le_of_le hx2  unfold psi  have primes : Λ 2 = log 2 ∧ Λ 3 = log 3 ∧ Λ 5 = log 5 ∧ Λ 7 = log 7 ∧ Λ 11 = log 11 ∧ Λ 13 = log 13 ∧ Λ 17 = log 17 ∧ Λ 19 = log 19 ∧ Λ 23 = log 23 ∧ Λ 29 = log 29 := by    split_ands <;> exact vonMangoldt_apply_prime (by decide)  have lam_pow : (Λ (2 ^ 2) = log 2) ∧ Λ (2 ^ 3) = log 2 ∧ Λ (2 ^ 4) = log 2 ∧ Λ (3 ^ 2) = log 3 ∧ Λ (3 ^ 3) = log 3 ∧ Λ (5 ^ 2) = log 5:= by    split_ands <;> rw [vonMangoldt_apply_pow (by norm_num)] <;> (try rw [primes.1]) <;> simp_all  have comps : Λ 6 = 0 ∧ Λ 10 = 0 ∧ Λ 12 = 0 ∧ Λ 14 = 0 ∧ Λ 15 = 0 ∧ Λ 18 = 0 ∧ Λ 20 = 0 ∧ Λ 21 = 0 ∧ Λ 22 = 0 ∧ Λ 24 = 0 ∧ Λ 26 = 0 ∧ Λ 28 = 0 ∧ Λ 30 = 0 := by    split_ands <;> rw [vonMangoldt_eq_zero_iff, isPrimePow_nat_iff_bounded_log] <;> decide  intro n hn  fin_cases hn  · simp  · simp; norm_num  all_goals    simp_all only [gt_iff_lt, Nat.reducePow, zero_add, Nat.reduceAdd, Nat.cast_ofNat,      Nat.floor_ofNat, zero_le, sum_Ioc_succ_top, Nat.Ioc_succ_singleton, sum_singleton,      vonMangoldt_apply_one, add_zero]    try grw [log_2_lt]; try grw [log_3_lt]; try grw [log_5_lt]; try grw [log_7_lt]    try grw [log_11_lt]; try grw [log_13_lt]; try grw [log_17_lt]; try grw [log_19_lt]    try grw [log_23_lt]; try grw [log_29_lt]    norm_num