Theorem: sum_mobius_div_self_le (PrimeNumberTheoremAnd/Consequences.lean)

State before:
N : ℕ
⊢ |∑ n ∈ range N, ↑(μ n) / ↑n| ≤ 1
Tactic:
cases' N with N
State after:
case zero

⊢ |∑ n ∈ range 0, ↑(μ n) / ↑n| ≤ 1

case succ
N : ℕ
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

State before:
case zero

⊢ |∑ n ∈ range 0, ↑(μ n) / ↑n| ≤ 1

case succ
N : ℕ
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
simp only [range_zero, sum_empty, abs_zero, zero_le_one]
State after:
case succ
N : ℕ
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

State before:
case succ
N : ℕ
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
by_cases hN : 1 ≤ N
State after:
case pos
N : ℕ
hN : 1 ≤ N
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

case neg
N : ℕ
hN : ¬1 ≤ N
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

State before:
case pos
N : ℕ
hN : 1 ≤ N
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

case neg
N : ℕ
hN : ¬1 ≤ N
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
swap
State after:
case neg
N : ℕ
hN : ¬1 ≤ N
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

case pos
N : ℕ
hN : 1 ≤ N
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

State before:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
rw [sum_congr rfl (g := fun d ↦ (μ d : ℚ) * ⌊(N : ℚ) / (d : ℚ)⌋)] at h_sum
State after:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
⊢ ∀ x ∈ range (N + 1), ↑(μ x) * ↑(N / x) = ↑(μ x) * ↑⌊↑N / ↑x⌋

State before:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
⊢ ∀ x ∈ range (N + 1), ↑(μ x) * ↑(N / x) = ↑(μ x) * ↑⌊↑N / ↑x⌋
Tactic:
swap
State after:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
⊢ ∀ x ∈ range (N + 1), ↑(μ x) * ↑(N / x) = ↑(μ x) * ↑⌊↑N / ↑x⌋

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

State before:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
⊢ ∀ x ∈ range (N + 1), ↑(μ x) * ↑(N / x) = ↑(μ x) * ↑⌊↑N / ↑x⌋

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
intros
State after:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
x✝ : ℕ
a✝ : x✝ ∈ range (N + 1)
⊢ ↑(μ x✝) * ↑(N / x✝) = ↑(μ x✝) * ↑⌊↑N / ↑x✝⌋

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

State before:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
x✝ : ℕ
a✝ : x✝ ∈ range (N + 1)
⊢ ↑(μ x✝) * ↑(N / x✝) = ↑(μ x✝) * ↑⌊↑N / ↑x✝⌋

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
rw [show (N : ℚ) = ((N : ℤ) : ℚ) by norm_cast, Rat.floor_int_div_nat_eq_div]
State after:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
x✝ : ℕ
a✝ : x✝ ∈ range (N + 1)
⊢ ↑(μ x✝) * ↑(N / x✝) = ↑(μ x✝) * ↑(↑N / ↑x✝)

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

State before:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
x✝ : ℕ
a✝ : x✝ ∈ range (N + 1)
⊢ ↑(μ x✝) * ↑(N / x✝) = ↑(μ x✝) * ↑(↑N / ↑x✝)

case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
congr
State after:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

State before:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
have hf' (d : ℕ) : |Int.fract ((N : ℚ) / d)| < 1 := by
  rw [abs_of_nonneg (Int.fract_nonneg _)]
  exact Int.fract_lt_one _
State after:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

State before:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
have h_bound : |∑ d in range (N + 1), μ d * Int.fract ((N : ℚ) / d)| ≤ N - 1 := by
  
  rw [range_eq_Ico, ← Ico_insert_succ_left, sum_insert, ArithmeticFunction.map_zero,
    Int.cast_zero, zero_mul, zero_add, Ico_succ_right]
  all_goals simp
  
  rw [← Ico_insert_right, sum_insert, div_self, Int.fract_one, mul_zero]
  all_goals simp [hN, Nat.pos_iff_ne_zero.mp hN]
  
  have (d : ℕ) : |μ d * Int.fract ((N : ℚ) / d)| ≤ 1 := by
    rw [abs_mul, ← one_mul 1]
    apply mul_le_mul ?_ (hf' _).le (abs_nonneg _) zero_le_one
    norm_cast
    simp [moebius]
    split_ifs <;> simp only [abs_zero, zero_le_one, abs_pow, abs_neg, abs_one, one_pow, le_refl]
  apply (abs_sum_le_sum_abs _ _).trans
  apply (sum_le_sum fun d _ ↦ this d).trans
  all_goals simp [sum_ite, cast_sub hN]
State after:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

State before:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
rw [sum_congr rfl (g := fun d : ℕ ↦ μ d * ((N : ℚ) / d - Int.fract ((N : ℚ) / d)))
  fun d _ ↦ by simp only [Int.fract, sub_sub_self]] at h_sum
State after:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * (↑N / ↑d - Int.fract (↑N / ↑d))
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

State before:
case pos
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * (↑N / ↑d - Int.fract (↑N / ↑d))
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
simp_rw (config := {singlePass := true}) [mul_sub] at h_sum
State after:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : 1 = ∑ x ∈ range (N + 1), (↑(μ x) * (↑N / ↑x) - ↑(μ x) * Int.fract (↑N / ↑x))
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

State before:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : 1 = ∑ x ∈ range (N + 1), (↑(μ x) * (↑N / ↑x) - ↑(μ x) * Int.fract (↑N / ↑x))
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
simp_rw [← mul_comm_div, sum_sub_distrib, ← sum_mul] at h_sum
State after:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : 1 = (∑ i ∈ range (N + 1), ↑(μ i) / ↑i) * ↑N - ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

State before:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : 1 = (∑ i ∈ range (N + 1), ↑(μ i) / ↑i) * ↑N - ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
rw [eq_sub_iff_add_eq, eq_comm, ← eq_div_iff (by norm_num [Nat.pos_iff_ne_zero.mp hN])] at h_sum
State after:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : ∑ i ∈ range (N + 1), ↑(μ i) / ↑i = (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

State before:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : ∑ i ∈ range (N + 1), ↑(μ i) / ↑i = (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
rw [h_sum, abs_le]
State after:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : ∑ i ∈ range (N + 1), ↑(μ i) / ↑i = (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N
⊢ -1 ≤ (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N ∧
    (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N ≤ 1

State before:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : ∑ i ∈ range (N + 1), ↑(μ i) / ↑i = (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N
⊢ -1 ≤ (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N ∧
    (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N ≤ 1
Tactic:
rw [abs_le, neg_sub] at h_bound
State after:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound :
  1 - ↑N ≤ ∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d) ∧
    ∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d) ≤ ↑N - 1
h_sum : ∑ i ∈ range (N + 1), ↑(μ i) / ↑i = (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N
⊢ -1 ≤ (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N ∧
    (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N ≤ 1

State before:
case pos
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound :
  1 - ↑N ≤ ∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d) ∧
    ∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d) ≤ ↑N - 1
h_sum : ∑ i ∈ range (N + 1), ↑(μ i) / ↑i = (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N
⊢ -1 ≤ (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N ∧
    (1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)) / ↑N ≤ 1
Tactic:
constructor
<;> simp only [le_div_iff, div_le_iff, cast_pos.mpr hN]
<;> linarith [h_bound.left]
State after:
no goals

State before:
case neg
N : ℕ
hN : ¬1 ≤ N
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
simp only [not_le, lt_one_iff] at hN
State after:
case neg
N : ℕ
hN : N = 0
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1

State before:
case neg
N : ℕ
hN : N = 0
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
subst hN
State after:
case neg

⊢ |∑ n ∈ range (0 + 1), ↑(μ n) / ↑n| ≤ 1

State before:
case neg

⊢ |∑ n ∈ range (0 + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
simp
State after:
no goals

State before:
N : ℕ
hN : 1 ≤ N
⊢ 1 = ↑(∑ m ∈ Icc 1 N, ∑ d ∈ m.divisors, μ d)
Tactic:
have {N : ℕ} : (1 : ArithmeticFunction _) N = ∑ d in N.divisors, μ d := by
  rw [← coe_mul_zeta_apply, moebius_mul_coe_zeta]
State after:
N : ℕ
hN : 1 ≤ N
this : ∀ {N : ℕ}, 1 N = ∑ d ∈ N.divisors, μ d
⊢ 1 = ↑(∑ m ∈ Icc 1 N, ∑ d ∈ m.divisors, μ d)

State before:
N : ℕ
hN : 1 ≤ N
this : ∀ {N : ℕ}, 1 N = ∑ d ∈ N.divisors, μ d
⊢ 1 = ↑(∑ m ∈ Icc 1 N, ∑ d ∈ m.divisors, μ d)
Tactic:
rw [Icc_eq_cons_Ioc hN, Finset.sum_cons, divisors_one, sum_singleton, moebius_apply_one]
State after:
N : ℕ
hN : 1 ≤ N
this : ∀ {N : ℕ}, 1 N = ∑ d ∈ N.divisors, μ d
⊢ 1 = ↑(1 + ∑ x ∈ Ioc 1 N, ∑ d ∈ x.divisors, μ d)

State before:
N : ℕ
hN : 1 ≤ N
this : ∀ {N : ℕ}, 1 N = ∑ d ∈ N.divisors, μ d
⊢ 1 = ↑(1 + ∑ x ∈ Ioc 1 N, ∑ d ∈ x.divisors, μ d)
Tactic:
have {x : ℕ} (hx : x ∈ Ioc 1 N) : ∑ d in divisors x, μ d = 0 := by
  rw [mem_Ioc] at hx
  simp only [← this, one_apply, hx.left.ne.symm, if_false]
State after:
N : ℕ
hN : 1 ≤ N
this✝ : ∀ {N : ℕ}, 1 N = ∑ d ∈ N.divisors, μ d
this : ∀ {x : ℕ}, x ∈ Ioc 1 N → ∑ d ∈ x.divisors, μ d = 0
⊢ 1 = ↑(1 + ∑ x ∈ Ioc 1 N, ∑ d ∈ x.divisors, μ d)

State before:
N : ℕ
hN : 1 ≤ N
this✝ : ∀ {N : ℕ}, 1 N = ∑ d ∈ N.divisors, μ d
this : ∀ {x : ℕ}, x ∈ Ioc 1 N → ∑ d ∈ x.divisors, μ d = 0
⊢ 1 = ↑(1 + ∑ x ∈ Ioc 1 N, ∑ d ∈ x.divisors, μ d)
Tactic:
rw [sum_congr rfl (fun _ ↦ this), sum_const, smul_zero, add_zero, Int.cast_one]
State after:
no goals

State before:
N✝ : ℕ
hN : 1 ≤ N✝
N : ℕ
⊢ 1 N = ∑ d ∈ N.divisors, μ d
Tactic:
rw [← coe_mul_zeta_apply, moebius_mul_coe_zeta]
State after:
no goals

State before:
N : ℕ
hN : 1 ≤ N
this : ∀ {N : ℕ}, 1 N = ∑ d ∈ N.divisors, μ d
x : ℕ
hx : x ∈ Ioc 1 N
⊢ ∑ d ∈ x.divisors, μ d = 0
Tactic:
rw [mem_Ioc] at hx
State after:
N : ℕ
hN : 1 ≤ N
this : ∀ {N : ℕ}, 1 N = ∑ d ∈ N.divisors, μ d
x : ℕ
hx : 1 < x ∧ x ≤ N
⊢ ∑ d ∈ x.divisors, μ d = 0

State before:
N : ℕ
hN : 1 ≤ N
this : ∀ {N : ℕ}, 1 N = ∑ d ∈ N.divisors, μ d
x : ℕ
hx : 1 < x ∧ x ≤ N
⊢ ∑ d ∈ x.divisors, μ d = 0
Tactic:
simp only [← this, one_apply, hx.left.ne.symm, if_false]
State after:
no goals

State before:
N : ℕ
hN : 1 ≤ N
⊢ ↑(∑ m ∈ Icc 1 N, ∑ d ∈ m.divisors, μ d) = ↑(∑ d ∈ range (N + 1), μ d * (↑N / ↑d))
Tactic:
simp_rw [← coe_mul_zeta_apply, ArithmeticFunction.sum_Icc_mul_zeta, nsmul_eq_mul, mul_comm]
State after:
N : ℕ
hN : 1 ≤ N
⊢ ↑(∑ x ∈ Icc 1 N, ↑(N / x) * μ x) = ↑(∑ x ∈ range (N + 1), ↑N / ↑x * μ x)

State before:
N : ℕ
hN : 1 ≤ N
⊢ ↑(∑ x ∈ Icc 1 N, ↑(N / x) * μ x) = ↑(∑ x ∈ range (N + 1), ↑N / ↑x * μ x)
Tactic:
rw [range_eq_Ico, ← Ico_insert_succ_left (succ_pos _), sum_insert, ArithmeticFunction.map_zero,
  mul_zero, zero_add]
State after:
N : ℕ
hN : 1 ≤ N
⊢ ↑(∑ x ∈ Icc 1 N, ↑(N / x) * μ x) = ↑(∑ x ∈ Ico (succ 0) N.succ, ↑N / ↑x * μ x)

N : ℕ
hN : 1 ≤ N
⊢ 0 ∉ Ico (succ 0) N.succ

State before:
N : ℕ
hN : 1 ≤ N
⊢ ↑(∑ x ∈ Icc 1 N, ↑(N / x) * μ x) = ↑(∑ x ∈ Ico (succ 0) N.succ, ↑N / ↑x * μ x)
Tactic:
congr
State after:
no goals

State before:
N : ℕ
hN : 1 ≤ N
⊢ 0 ∉ Ico (succ 0) N.succ
Tactic:
simp
State after:
no goals

State before:
N : ℕ
hN : 1 ≤ N
⊢ ↑(∑ d ∈ range (N + 1), μ d * (↑N / ↑d)) = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
Tactic:
norm_num [Int.cast_sum]
State after:
N : ℕ
hN : 1 ≤ N
⊢ ∑ x ∈ range (N + 1), ↑(μ x) * ↑(↑N / ↑x) = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)

State before:
N : ℕ
hN : 1 ≤ N
⊢ ∑ x ∈ range (N + 1), ↑(μ x) * ↑(↑N / ↑x) = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
Tactic:
rfl
State after:
no goals

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
x✝ : ℕ
a✝ : x✝ ∈ range (N + 1)
⊢ ↑N = ↑↑N
Tactic:
norm_cast
State after:
no goals

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
d : ℕ
⊢ |Int.fract (↑N / ↑d)| < 1
Tactic:
rw [abs_of_nonneg (Int.fract_nonneg _)]
State after:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
d : ℕ
⊢ Int.fract (↑N / ↑d) < 1

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
d : ℕ
⊢ Int.fract (↑N / ↑d) < 1
Tactic:
exact Int.fract_lt_one _
State after:
no goals

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
Tactic:
rw [range_eq_Ico, ← Ico_insert_succ_left, sum_insert, ArithmeticFunction.map_zero,
  Int.cast_zero, zero_mul, zero_add, Ico_succ_right]
State after:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ |∑ x ∈ Icc (succ 0) N, ↑(μ x) * Int.fract (↑N / ↑x)| ≤ ↑N - 1

N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ 0 ∉ Ico (succ 0) (N + 1)

N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ 0 < N + 1

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ |∑ x ∈ Icc (succ 0) N, ↑(μ x) * Int.fract (↑N / ↑x)| ≤ ↑N - 1

N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ 0 ∉ Ico (succ 0) (N + 1)

N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ 0 < N + 1
Tactic:
all_goals simp
State after:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ |∑ x ∈ Icc 1 N, ↑(μ x) * Int.fract (↑N / ↑x)| ≤ ↑N - 1

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ |∑ x ∈ Icc 1 N, ↑(μ x) * Int.fract (↑N / ↑x)| ≤ ↑N - 1
Tactic:
rw [← Ico_insert_right, sum_insert, div_self, Int.fract_one, mul_zero]
State after:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ |0 + ∑ x ∈ Ico 1 N, ↑(μ x) * Int.fract (↑N / ↑x)| ≤ ↑N - 1

N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ ↑N ≠ 0

N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ N ∉ Ico 1 N

N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ 1 ≤ N

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ |0 + ∑ x ∈ Ico 1 N, ↑(μ x) * Int.fract (↑N / ↑x)| ≤ ↑N - 1

N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ ↑N ≠ 0

N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ N ∉ Ico 1 N

N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ 1 ≤ N
Tactic:
all_goals simp [hN, Nat.pos_iff_ne_zero.mp hN]
State after:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ |∑ x ∈ Ico 1 N, ↑(μ x) * Int.fract (↑N / ↑x)| ≤ ↑N - 1

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ |∑ x ∈ Ico 1 N, ↑(μ x) * Int.fract (↑N / ↑x)| ≤ ↑N - 1
Tactic:
have (d : ℕ) : |μ d * Int.fract ((N : ℚ) / d)| ≤ 1 := by
  rw [abs_mul, ← one_mul 1]
  apply mul_le_mul ?_ (hf' _).le (abs_nonneg _) zero_le_one
  norm_cast
  simp [moebius]
  split_ifs <;> simp only [abs_zero, zero_le_one, abs_pow, abs_neg, abs_one, one_pow, le_refl]
State after:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
this : ∀ (d : ℕ), |↑(μ d) * Int.fract (↑N / ↑d)| ≤ 1
⊢ |∑ x ∈ Ico 1 N, ↑(μ x) * Int.fract (↑N / ↑x)| ≤ ↑N - 1

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
this : ∀ (d : ℕ), |↑(μ d) * Int.fract (↑N / ↑d)| ≤ 1
⊢ |∑ x ∈ Ico 1 N, ↑(μ x) * Int.fract (↑N / ↑x)| ≤ ↑N - 1
Tactic:
apply (abs_sum_le_sum_abs _ _).trans
State after:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
this : ∀ (d : ℕ), |↑(μ d) * Int.fract (↑N / ↑d)| ≤ 1
⊢ ∑ i ∈ Ico 1 N, |↑(μ i) * Int.fract (↑N / ↑i)| ≤ ↑N - 1

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
this : ∀ (d : ℕ), |↑(μ d) * Int.fract (↑N / ↑d)| ≤ 1
⊢ ∑ i ∈ Ico 1 N, |↑(μ i) * Int.fract (↑N / ↑i)| ≤ ↑N - 1
Tactic:
apply (sum_le_sum fun d _ ↦ this d).trans
State after:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
this : ∀ (d : ℕ), |↑(μ d) * Int.fract (↑N / ↑d)| ≤ 1
⊢ ∑ i ∈ Ico 1 N, 1 ≤ ↑N - 1

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
this : ∀ (d : ℕ), |↑(μ d) * Int.fract (↑N / ↑d)| ≤ 1
⊢ ∑ i ∈ Ico 1 N, 1 ≤ ↑N - 1
Tactic:
all_goals simp [sum_ite, cast_sub hN]
State after:
no goals

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ 0 < N + 1
Tactic:
simp
State after:
no goals

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
⊢ 1 ≤ N
Tactic:
simp [hN, Nat.pos_iff_ne_zero.mp hN]
State after:
no goals

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
d : ℕ
⊢ |↑(μ d) * Int.fract (↑N / ↑d)| ≤ 1
Tactic:
rw [abs_mul, ← one_mul 1]
State after:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
d : ℕ
⊢ |↑(μ d)| * |Int.fract (↑N / ↑d)| ≤ 1 * 1

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
d : ℕ
⊢ |↑(μ d)| * |Int.fract (↑N / ↑d)| ≤ 1 * 1
Tactic:
apply mul_le_mul ?_ (hf' _).le (abs_nonneg _) zero_le_one
State after:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
d : ℕ
⊢ |↑(μ d)| ≤ 1

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
d : ℕ
⊢ |↑(μ d)| ≤ 1
Tactic:
norm_cast
State after:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
d : ℕ
⊢ |μ d| ≤ 1

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
d : ℕ
⊢ |μ d| ≤ 1
Tactic:
simp [moebius]
State after:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
d : ℕ
⊢ |if Squarefree d then (-1) ^ Ω d else 0| ≤ 1

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
d : ℕ
⊢ |if Squarefree d then (-1) ^ Ω d else 0| ≤ 1
Tactic:
split_ifs <;> simp only [abs_zero, zero_le_one, abs_pow, abs_neg, abs_one, one_pow, le_refl]
State after:
no goals

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
this : ∀ (d : ℕ), |↑(μ d) * Int.fract (↑N / ↑d)| ≤ 1
⊢ ∑ i ∈ Ico 1 N, 1 ≤ ↑N - 1
Tactic:
simp [sum_ite, cast_sub hN]
State after:
no goals

State before:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
d : ℕ
x✝ : d ∈ range (N + 1)
⊢ ↑(μ d) * ↑⌊↑N / ↑d⌋ = (fun d => ↑(μ d) * (↑N / ↑d - Int.fract (↑N / ↑d))) d
Tactic:
simp only [Int.fract, sub_sub_self]
State after:
no goals

State before:
N : ℕ
hN : 1 ≤ N
hf' : ∀ (d : ℕ), |Int.fract (↑N / ↑d)| < 1
h_bound : |∑ d ∈ range (N + 1), ↑(μ d) * Int.fract (↑N / ↑d)| ≤ ↑N - 1
h_sum : (∑ i ∈ range (N + 1), ↑(μ i) / ↑i) * ↑N = 1 + ∑ x ∈ range (N + 1), ↑(μ x) * Int.fract (↑N / ↑x)
⊢ ↑N ≠ 0
Tactic:
norm_num [Nat.pos_iff_ne_zero.mp hN]
State after:
no goals