Chebyshev.E_nu_bound

@[blueprint  "cheby-E-val"  (title := "$E$ lies between $0$ and $1$")  (statement := /-- One has $0 \leq E(x) \leq 1$ for all $x \geq 0$. -/)  (proof := /-- This follows from direct computation for $0 \leq x < 30$, and then by periodicity for larger $x$. -/)  (latexEnv := "lemma")  (discussion := 836)]theorem E_nu_bound (x : ℝ) (hx : x ≥ 0) : 0 ≤ E ν x ∧ E ν x ≤ 1 := by  have : ∀ y, 0 ≤ y → y < 30 → 0 ≤ E ν y ∧ E ν y ≤ 1 := fun y hy0 hy30 ↦ by    simp only [E_nu_expand, Nat.floor_eq_zero.mpr (by linarith : y / 30 < 1), Nat.cast_zero, add_zero]    have h2 := floor_div_bounds hy0 (k := 2) (by norm_num)    have h3 := floor_div_bounds hy0 (k := 3) (by norm_num)    have h5 := floor_div_bounds hy0 (k := 5) (by norm_num)    push_cast at h2 h3 h5    have hfy : ⌊y⌋₊ < 30 := Nat.floor_lt' (by norm_num) |>.mpr (by exact_mod_cast hy30)    have hlb : ⌊y/2⌋₊ + ⌊y/3⌋₊ + ⌊y/5⌋₊ ≤ ⌊y⌋₊ := by omega    have hub : ⌊y⌋₊ ≤ ⌊y/2⌋₊ + ⌊y/3⌋₊ + ⌊y/5⌋₊ + 1 := by omega    have hlb' : ((⌊y/2⌋₊ + ⌊y/3⌋₊ + ⌊y/5⌋₊ : ℕ) : ℝ) ≤ (⌊y⌋₊ : ℝ) := by exact_mod_cast hlb    have hub' : ((⌊y⌋₊ : ℕ) : ℝ) ≤ ((⌊y/2⌋₊ + ⌊y/3⌋₊ + ⌊y/5⌋₊ + 1 : ℕ) : ℝ) := by exact_mod_cast hub    push_cast at hlb' hub'    refine ⟨by linarith, by linarith⟩  let y := x - ⌊x / 30⌋₊ * 30  have hy : 0 ≤ y ∧ y < 30 := ⟨by linarith [Nat.floor_le (by positivity : 0 ≤ x/30)], by    linarith [Nat.lt_floor_add_one (x/30)]⟩  have hxy : E ν x = E ν y := by    have : x = y + ⌊x/30⌋₊ * 30 := by ring    rw [this]; induction ⌊x/30⌋₊ with    | zero => simp    | succ n ih => simp [add_mul, ← add_assoc, E_nu_period _ (by linarith : y + n * 30 ≥ 0), ih]  exact hxy ▸ this y hy.1 hy.2