sum_mobius_div_self_le

@[blueprint  "mun"  (statement := /-- We have $|\sum_{n \leq x} \frac{\mu(n)}{n}| \leq 1$. -/)  (proof := /--  From M\"obius inversion $1_{n=1} = \sum_{d|n} \mu(d)$ and summing we have    $$ 1 = \sum_{d \leq x} \mu(d) \lfloor \frac{x}{d} \rfloor$$    for any $x \geq 1$. Since $\lfloor \frac{x}{d} \rfloor = \frac{x}{d} - \epsilon_d$ with    $0 \leq \epsilon_d < 1$ and $\epsilon_x = 0$, we conclude that    $$ 1 ≥ x \sum_{d \leq x} \frac{\mu(d)}{d} - (x - 1)$$    and the claim follows.  -/)  (latexEnv := "proposition")]theorem sum_mobius_div_self_le (N : ℕ) : |∑ n ∈ range N, μ n / (n : ℚ)| ≤ 1 := by  cases N with  | zero => simp only [range_zero, sum_empty, abs_zero, zero_le_one]  | succ N =>  /- simple cases -/  obtain rfl | hN := N.eq_zero_or_pos  · simp  /- annoying case -/  have h_sum : 1 = (∑ d ∈ range (N + 1), (μ d / d : ℚ)) * N - ∑ d ∈ range (N + 1),      μ d * Int.fract (N / d : ℚ) := calc    (1 : ℚ) = ∑ m ∈ Ioc 0 N, ∑ d ∈ m.divisors, μ d := by      have (x : ℕ) (hx : x ∈ Ioc 0 N) : ∑ d ∈ divisors x, μ d = if x = 1 then 1 else 0 := by        rw [mem_Ioc] at hx        rw [← coe_mul_zeta_apply, moebius_mul_coe_zeta, one_apply]      rw [sum_congr rfl this]      simp [hN.ne']    _ = ∑ d ∈ range (N + 1), μ d * (N / d : ℕ) := by      simp_rw [← coe_mul_zeta_apply, ArithmeticFunction.sum_Ioc_mul_zeta_eq_sum]      rw [range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico (add_one_pos _),        sum_insert (by simp), Ico_add_one_add_one_eq_Ioc]      simp    _ = ∑ d ∈ range (N + 1), (μ d : ℚ) * ⌊(N / d : ℚ)⌋ := by      simp_rw [Rat.floor_natCast_div_natCast]      simp [← Int.natCast_ediv]    _ = (∑ d ∈ range (N + 1), (μ d / d : ℚ)) * N - ∑ d ∈ range (N + 1),        μ d * Int.fract (N / d : ℚ) := by      simp_rw [sum_mul, ← sum_sub_distrib, mul_comm_div, ← mul_sub, Int.self_sub_fract]  rw [eq_sub_iff_add_eq, eq_comm, ← eq_div_iff (by norm_num [Nat.pos_iff_ne_zero.mp hN])] at h_sum   /- Next, we establish bounds for the error term -/  have hf' (d : ℕ) : |Int.fract ((N : ℚ) / d)| < 1 := by    rw [abs_of_nonneg (Int.fract_nonneg _)]    exact Int.fract_lt_one _  have h_bound : |∑ d ∈ range (N + 1), μ d * Int.fract ((N : ℚ) / d)| ≤ N - 1 := by    /- range (N + 1) → Icc 1 N + part that evals to 0 -/    rw [range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico (by simp), sum_insert (by simp),      ArithmeticFunction.map_zero, Int.cast_zero, zero_mul, zero_add,      Finset.Ico_add_one_right_eq_Icc, zero_add]    /- Ico 1 (N + 1) → Ico 1 N ∪ {N + 1} that evals to 0 -/    rw [← Ico_insert_right hN, sum_insert (by simp), div_self (by simp; grind), Int.fract_one,      mul_zero, zero_add]    /- bound sum -/    have (d : ℕ) : |μ d * Int.fract ((N : ℚ) / d)| ≤ 1 := by      rw [abs_mul, ← one_mul 1]      refine mul_le_mul ?_ (hf' _).le (abs_nonneg _) zero_le_one      norm_cast      exact abs_moebius_le_one    apply (abs_sum_le_sum_abs _ _).trans    apply (sum_le_sum fun d _ ↦ this d).trans    simp [cast_sub (one_le_iff_ne_zero.mpr hN.ne')]   rw [h_sum, abs_le]  rw [abs_le, neg_sub] at h_bound  constructor  <;> simp only [le_div_iff₀, div_le_iff₀, cast_pos.mpr hN]  <;> linarith [h_bound.left]