Chebyshev.T.le

@[blueprint  "cheby-T-upper"  (title := "Upper bound on $T$")  (statement := /-- For $x \geq 1$, we have $T(x) \leq x \log x - x + 1 + \log x$. -/)  (proof := /-- Upper bound $\log n$ by $\int_n^{n+1} \log t\ dt$ for $n < x-1$ and by $\log x$ for $x-1 < n \leq x$ to bound  $$T(x) \leq \int_1^x \log t\ dt + \log x$$  giving the claim. -/)  (latexEnv := "lemma")  (discussion := 831)]theorem T.le (x : ℝ) (hx : 1 ≤ x) : T x ≤ x * log x - x + 1 + log x := by  rw [T, ← Ico_insert_right <| Nat.one_le_iff_ne_zero.mpr (Nat.floor_pos.mpr hx).ne',    sum_insert right_notMem_Ico]  have : MonotoneOn log (Set.Icc (1 : ℕ) ⌊x⌋₊) :=    fun a ha _ _ hab ↦ log_le_log (lt_of_lt_of_le one_pos (by grind)) hab  have : ∑ n ∈ Finset.Ico 1 ⌊x⌋₊, log n ≤ ⌊x⌋₊ * log ⌊x⌋₊ - ⌊x⌋₊ + 1 :=    calc ∑ n ∈ Finset.Ico 1 ⌊x⌋₊, log n        ≤ ∫ t in (1 : ℕ)..(⌊x⌋₊ : ℕ), log t := this.sum_le_integral_Ico <|          Nat.one_le_iff_ne_zero.mpr (Nat.floor_pos.mpr hx).ne'      _ = ⌊x⌋₊ * log ⌊x⌋₊ - ⌊x⌋₊ + 1 := by simp  have h1 : (1 : ℝ) ≤ ⌊x⌋₊ := by simp_all  have h3 : ∀ t ∈ interior (Set.Ici 1), DifferentiableWithinAt ℝ (_root_.id * log - _root_.id) (interior (Set.Ici 1)) t := by    intro t ht    simp only [Set.nonempty_Iio, interior_Ici', Set.mem_Ioi] at ht    fun_prop ( disch := positivity )  have h4 : ∀ t ∈ interior (Set.Ici 1), 0 ≤ deriv (fun t ↦ t * log t - t) t := by    intro t ht    simp only [Set.nonempty_Iio, interior_Ici', Set.mem_Ioi] at ht    have : DifferentiableAt ℝ (fun t ↦ t * log t) t := by fun_prop ( disch := positivity )    have hderiv : deriv (fun t ↦ t * log t - t) t = log t := by      simp [show (fun t ↦ t * log t - t) = (fun t ↦ t * log t) - _root_.id by rfl,        deriv_sub this differentiableAt_id, deriv_mul_log (by linarith)]    exact hderiv ▸ log_nonneg (le_of_lt ht)  have h5 : ContinuousOn (fun t ↦ t * log t - t) (Set.Ici 1) := by fun_prop  have h2 : MonotoneOn (fun t ↦ t * log t - t) (Set.Ici 1) :=    monotoneOn_of_deriv_nonneg (convex_Ici 1) h5 h3 h4  have : (⌊x⌋₊ : ℝ) * log ⌊x⌋₊ - ⌊x⌋₊ ≤ x * log x - x := by    exact h2 (Set.mem_Ici.mpr h1) (Set.mem_Ici.mpr hx) <| Nat.floor_le (by grind)  linarith [log_le_log (by positivity) <| Nat.floor_le (by linarith)]