Chebyshev.psi_upper_clean

@[blueprint  "psi-upper-clean"  (title := "Clean upper bound for $\\psi$")  (statement := /-- For $x > 0$, we have $\psi(x) \leq 1.11 x$. -/)  (proof := /-- Strong induction on $x$.  For $x \leq 11723$ one can use Sublemma \ref{psi-num-2}.  Otherwise, we can use Proposition \ref{psi-diff-upper} and the triangle inequality. -/)  (latexEnv := "theorem")  (discussion := 844)]theorem psi_upper_clean (x : ℝ) (hx : x > 0) : ψ x ≤ 1.11 * x := by  have hlog_large : ∀ y : ℝ, 11723 < y → 5 * log y - 5 ≤ (37 / 10000 : ℝ) * y := by    intro y hy    have hlog_11723 : log (11723 : ℝ) ≤ 937 / 100 := LogTables.log_11723_lt    calc 5 * log y - 5        ≤ 5 * (937 / 100 + (y / 11723 - 1)) - 5 := by linarith [hlog_y y hy]      _ = 5 / 11723 * y + 3685 / 100 := by ring      _ ≤ 37 / 10000 * y := by linarith  have hNat : ∀ n : ℕ, ψ (n : ℝ) ≤ 1.11 * n := by    intro n    refine Nat.strong_induction_on n ?_    intro n ih    by_cases hn0 : n = 0    · subst hn0; simp [psi_eq_zero_of_lt_two (by norm_num : (0 : ℝ) < 2)]    · have hn : 0 < n := Nat.pos_of_ne_zero hn0      by_cases! hsmall : (n : ℝ) ≤ 11723      · exact psi_num_2 n (by exact_mod_cast hn) hsmall      · let m : ℕ := ⌊(n : ℝ) / 6⌋₊        have hm_lt_n : m < n := by          exact_mod_cast show (m : ℝ) < n from            lt_of_le_of_lt (Nat.floor_le (by positivity)) (by nlinarith)        have hpsi_div : ψ ((n : ℝ) / 6) ≤ 1.11 * ((n : ℝ) / 6) := calc          ψ ((n : ℝ) / 6) = ψ (m : ℝ) := by simp [m, psi_eq_psi_coe_floor]          _ ≤ 1.11 * (m : ℝ) := ih m hm_lt_n          _ ≤ 1.11 * ((n : ℝ) / 6) := by nlinarith [Nat.floor_le (by positivity : 0 ≤ (n : ℝ) / 6)]        calc ψ (n : ℝ)            ≤ ψ ((n : ℝ) / 6) + a * n + 5 * log (n : ℝ) - 5 := by                linarith [psi_diff_upper (n : ℝ) (by linarith)]          _ ≤ 1.11 * ((n : ℝ) / 6) + 0.92130 * n + (37 / 10000 : ℝ) * n := by                nlinarith [hpsi_div, hlog_large (n : ℝ) hsmall, a_bound.2,                  show (0 : ℝ) < n from by exact_mod_cast hn]          _ = 1.11 * n := by ring  rw [psi_eq_psi_coe_floor x]  calc ψ (⌊x⌋₊ : ℝ) ≤ 1.11 * ⌊x⌋₊ := hNat ⌊x⌋₊    _ ≤ 1.11 * x := by nlinarith [Nat.floor_le hx.le]