internlm/Lean-Github huggingface dataset:
Theorem: sum_mobius_div_self_le
Proof 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]
Proof state after:
no goals
Theorem: sum_mobius_div_self_le
Proof 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
Proof state after:
case neg
N : ℕ
hN : N = 0
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Theorem: sum_mobius_div_self_le
Proof state before:
case neg
N : ℕ
hN : N = 0
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
subst hN
Proof state after:
case neg

⊢ |∑ n ∈ range (0 + 1), ↑(μ n) / ↑n| ≤ 1
Theorem: sum_mobius_div_self_le
Proof state before:
case neg

⊢ |∑ n ∈ range (0 + 1), ↑(μ n) / ↑n| ≤ 1
Tactic:
simp
Proof state after:
no goals
Theorem: sum_mobius_div_self_le
Proof 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]
Proof state after:
N : ℕ
hN : 1 ≤ N
this : ∀ {N : ℕ}, 1 N = ∑ d ∈ N.divisors, μ d
⊢ 1 = ↑(∑ m ∈ Icc 1 N, ∑ d ∈ m.divisors, μ d)
Theorem: sum_mobius_div_self_le
Proof 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]
Proof state after:
N : ℕ
hN : 1 ≤ N
this : ∀ {N : ℕ}, 1 N = ∑ d ∈ N.divisors, μ d
⊢ 1 = ↑(1 + ∑ x ∈ Ioc 1 N, ∑ d ∈ x.divisors, μ d)
Theorem: sum_mobius_div_self_le
Proof 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]
Proof 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)
Theorem: sum_mobius_div_self_le
Proof 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]
Proof state after:
no goals
Theorem: sum_mobius_div_self_le
Proof state before:
N✝ : ℕ
hN : 1 ≤ N✝
N : ℕ
⊢ 1 N = ∑ d ∈ N.divisors, μ d
Tactic:
rw [← coe_mul_zeta_apply, moebius_mul_coe_zeta]
Proof state after:
no goals
Theorem: sum_mobius_div_self_le
Proof 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
Proof 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
Theorem: sum_mobius_div_self_le
Proof 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]
Proof state after:
no goals
Theorem: sum_mobius_div_self_le
Proof 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]
Proof state after:
N : ℕ
hN : 1 ≤ N
⊢ ↑(∑ x ∈ Icc 1 N, ↑(N / x) * μ x) = ↑(∑ x ∈ range (N + 1), ↑N / ↑x * μ x)
Theorem: sum_mobius_div_self_le
Proof 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]
Proof 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
Theorem: sum_mobius_div_self_le
Proof state before:
N : ℕ
hN : 1 ≤ N
⊢ ↑(∑ x ∈ Icc 1 N, ↑(N / x) * μ x) = ↑(∑ x ∈ Ico (succ 0) N.succ, ↑N / ↑x * μ x)
Tactic:
congr
Proof state after:
no goals
Theorem: sum_mobius_div_self_le
Proof state before:
N : ℕ
hN : 1 ≤ N
⊢ 0 ∉ Ico (succ 0) N.succ
Tactic:
simp
Proof state after:
no goals
Theorem: sum_mobius_div_self_le
Proof 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]
Proof state after:
N : ℕ
hN : 1 ≤ N
⊢ ∑ x ∈ range (N + 1), ↑(μ x) * ↑(↑N / ↑x) = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
Theorem: sum_mobius_div_self_le
Proof state before:
N : ℕ
hN : 1 ≤ N
⊢ ∑ x ∈ range (N + 1), ↑(μ x) * ↑(↑N / ↑x) = ∑ d ∈ range (N + 1), ↑(μ d) * ↑(N / d)
Tactic:
rfl
Proof state after:
no goals
Theorem: sum_mobius_div_self_le
Proof 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
Proof state after:
no goals
Theorem: sum_mobius_div_self_le
Proof 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 _)]
Proof state after:
N : ℕ
hN : 1 ≤ N
h_sum : 1 = ∑ d ∈ range (N + 1), ↑(μ d) * ↑⌊↑N / ↑d⌋
d : ℕ
⊢ Int.fract (↑N / ↑d) < 1
Theorem: sum_mobius_div_self_le
Proof 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 _
Proof state after:
no goals
Theorem: sum_mobius_div_self_le
Proof 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]
Proof 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
Theorem: sum_mobius_div_self_le
Proof 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
Proof 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
Theorem: sum_mobius_div_self_le
Proof 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]
Proof 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
Theorem: sum_mobius_div_self_le
Proof 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]
Proof 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
Theorem: sum_mobius_div_self_le
Proof 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]
Proof 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
Theorem: sum_mobius_div_self_le
Proof 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
Proof 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
Theorem: sum_mobius_div_self_le
Proof 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
Proof 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
Theorem: sum_mobius_div_self_le
Proof 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]
Proof state after:
no goals
Theorem: sum_mobius_div_self_le
Proof 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
Proof state after:
no goals
Theorem: sum_mobius_div_self_le
Proof 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]
Proof state after:
no goals
Theorem: sum_mobius_div_self_le
Proof 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]
Proof 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
Theorem: sum_mobius_div_self_le
Proof 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
Proof 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
Theorem: sum_mobius_div_self_le
Proof 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
Proof 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
Theorem: sum_mobius_div_self_le
Proof 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]
Proof 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
Theorem: sum_mobius_div_self_le
Proof 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]
Proof state after:
no goals
Theorem: sum_mobius_div_self_le
Proof 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]
Proof state after:
no goals
Theorem: sum_mobius_div_self_le
Proof 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]
Proof state after:
no goals
Theorem: sum_mobius_div_self_le
Proof 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]
Proof state after:
no goals
Theorem: mu_pnt
Proof state before:
⊢ (fun x => ∑ n ∈ range ⌊x⌋₊, μ n) =o[atTop] fun x => x
Tactic:
sorry
Proof state after:
no goals
Theorem: lambda_pnt
Proof state before:
⊢ (fun x => ∑ n ∈ range ⌊x⌋₊, (-1) ^ Ω n) =o[atTop] fun x => x
Tactic:
sorry
Proof state after:
no goals
Theorem: mu_pnt_alt
Proof state before:
⊢ (fun x => ∑ n ∈ range ⌊x⌋₊, ↑(μ n) / ↑n) =o[atTop] fun x => 1
Tactic:
sorry
Proof state after:
no goals
Theorem: VIntegral_symm
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
⊢ VIntegral f x y₁ y₂ = -VIntegral f x y₂ y₁
Tactic:
simp_rw [VIntegral, integral_symm y₁ y₂, smul_neg, neg_neg]
Proof state after:
no goals
Theorem: verticalIntegral_split_three
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ a b : ℝ
hf : Integrable (fun t => f (↑σ + ↑t * I)) volume
⊢ VerticalIntegral f σ =
    (I • ∫ (t : ℝ) in Iic a, f (↑σ + ↑t * I)) + VIntegral f σ a b + I • ∫ (t : ℝ) in Ici b, f (↑σ + ↑t * I)
Tactic:
simp_rw [VerticalIntegral, VIntegral, ← smul_add]
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ a b : ℝ
hf : Integrable (fun t => f (↑σ + ↑t * I)) volume
⊢ I • ∫ (t : ℝ), f (↑σ + ↑t * I) =
    I •
      (((∫ (t : ℝ) in Iic a, f (↑σ + ↑t * I)) + ∫ (t : ℝ) in a..b, f (↑σ + ↑t * I)) +
        ∫ (t : ℝ) in Ici b, f (↑σ + ↑t * I))
Theorem: verticalIntegral_split_three
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ a b : ℝ
hf : Integrable (fun t => f (↑σ + ↑t * I)) volume
⊢ I • ∫ (t : ℝ), f (↑σ + ↑t * I) =
    I •
      (((∫ (t : ℝ) in Iic a, f (↑σ + ↑t * I)) + ∫ (t : ℝ) in a..b, f (↑σ + ↑t * I)) +
        ∫ (t : ℝ) in Ici b, f (↑σ + ↑t * I))
Tactic:
congr
Proof state after:
case e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ a b : ℝ
hf : Integrable (fun t => f (↑σ + ↑t * I)) volume
⊢ ∫ (t : ℝ), f (↑σ + ↑t * I) =
    ((∫ (t : ℝ) in Iic a, f (↑σ + ↑t * I)) + ∫ (t : ℝ) in a..b, f (↑σ + ↑t * I)) + ∫ (t : ℝ) in Ici b, f (↑σ + ↑t * I)
Theorem: verticalIntegral_split_three
Proof state before:
case e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ a b : ℝ
hf : Integrable (fun t => f (↑σ + ↑t * I)) volume
⊢ ∫ (t : ℝ), f (↑σ + ↑t * I) =
    ((∫ (t : ℝ) in Iic a, f (↑σ + ↑t * I)) + ∫ (t : ℝ) in a..b, f (↑σ + ↑t * I)) + ∫ (t : ℝ) in Ici b, f (↑σ + ↑t * I)
Tactic:
rw [← intervalIntegral.integral_Iic_sub_Iic hf.restrict hf.restrict, add_sub_cancel,
  integral_Iic_eq_integral_Iio, intervalIntegral.integral_Iio_add_Ici hf.restrict hf.restrict]
Proof state after:
no goals
Theorem: DiffVertRect_eq_UpperLowerUs
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ VerticalIntegral f σ' - VerticalIntegral f σ - RectangleIntegral f (↑σ - I * ↑T) (↑σ' + I * ↑T) =
    UpperUIntegral f σ σ' T - LowerUIntegral f σ σ' T
Tactic:
rw [verticalIntegral_split_three (-T) T f_int_σ, verticalIntegral_split_three (-T) T f_int_σ']
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) + VIntegral f σ' (-T) T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) -
        ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I)) + VIntegral f σ (-T) T +
          I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      RectangleIntegral f (↑σ - I * ↑T) (↑σ' + I * ↑T) =
    UpperUIntegral f σ σ' T - LowerUIntegral f σ σ' T
Theorem: DiffVertRect_eq_UpperLowerUs
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) + VIntegral f σ' (-T) T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) -
        ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I)) + VIntegral f σ (-T) T +
          I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      RectangleIntegral f (↑σ - I * ↑T) (↑σ' + I * ↑T) =
    UpperUIntegral f σ σ' T - LowerUIntegral f σ σ' T
Tactic:
simp only [RectangleIntegral, UpperUIntegral, LowerUIntegral]
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) + VIntegral f σ' (-T) T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) -
        ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I)) + VIntegral f σ (-T) T +
          I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      (HIntegral f (↑σ - I * ↑T).re (↑σ' + I * ↑T).re (↑σ - I * ↑T).im -
            HIntegral f (↑σ - I * ↑T).re (↑σ' + I * ↑T).re (↑σ' + I * ↑T).im +
          VIntegral f (↑σ' + I * ↑T).re (↑σ - I * ↑T).im (↑σ' + I * ↑T).im -
        VIntegral f (↑σ - I * ↑T).re (↑σ - I * ↑T).im (↑σ' + I * ↑T).im) =
    ((HIntegral f σ σ' T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) - I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      ((HIntegral f σ σ' (-T) - I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) +
        I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I))
Theorem: DiffVertRect_eq_UpperLowerUs
Proof state before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) + VIntegral f σ' (-T) T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) -
        ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I)) + VIntegral f σ (-T) T +
          I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      (HIntegral f (↑σ - I * ↑T).re (↑σ' + I * ↑T).re (↑σ - I * ↑T).im -
            HIntegral f (↑σ - I * ↑T).re (↑σ' + I * ↑T).re (↑σ' + I * ↑T).im +
          VIntegral f (↑σ' + I * ↑T).re (↑σ - I * ↑T).im (↑σ' + I * ↑T).im -
        VIntegral f (↑σ - I * ↑T).re (↑σ - I * ↑T).im (↑σ' + I * ↑T).im) =
    ((HIntegral f σ σ' T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) - I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      ((HIntegral f σ σ' (-T) - I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) +
        I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I))
Tactic:
simp only [sub_re, mul_re, I_re, add_re, ofReal_re, I_im, ofReal_im, sub_im, mul_im, add_im]
Proof state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ✝ σ σ' T : ℝ
f_int_σ : Integrable (fun t => f (↑σ + ↑t * I)) volume
f_int_σ' : Integrable (fun t => f (↑σ' + ↑t * I)) volume
⊢ ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) + VIntegral f σ' (-T) T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) -
        ((I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I)) + VIntegral f σ (-T) T +
          I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      (HIntegral f (σ - (0 * T - 1 * 0)) (σ' + (0 * T - 1 * 0)) (0 - (0 * 0 + 1 * T)) -
            HIntegral f (σ - (0 * T - 1 * 0)) (σ' + (0 * T - 1 * 0)) (0 + (0 * 0 + 1 * T)) +
          VIntegral f (σ' + (0 * T - 1 * 0)) (0 - (0 * 0 + 1 * T)) (0 + (0 * 0 + 1 * T)) -
        VIntegral f (σ - (0 * T - 1 * 0)) (0 - (0 * 0 + 1 * T)) (0 + (0 * 0 + 1 * T))) =
    ((HIntegral f σ σ' T + I • ∫ (t : ℝ) in Ici T, f (↑σ' + ↑t * I)) - I • ∫ (t : ℝ) in Ici T, f (↑σ + ↑t * I)) -
      ((HIntegral f σ σ' (-T) - I • ∫ (t : ℝ) in Iic (-T), f (↑σ' + ↑t * I)) +
        I • ∫ (t : ℝ) in Iic (-T), f (↑σ + ↑t * I))