Source indexedlemma · leanprover/lean4:v4.32.0

sum_mobius_mul_floor

PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:1647 to 1659

Mathematical statement

Exact Lean statement

lemma sum_mobius_mul_floor (x : ℝ) (hx : 1 ≤ x) :
  ∑ n ∈ Iic ⌊x⌋₊, (ArithmeticFunction.moebius n : ℝ) * (⌊x/n⌋ : ℝ) = 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma sum_mobius_mul_floor (x : ℝ) (hx : 1 ≤ x) :  ∑ n ∈ Iic ⌊x⌋₊, (ArithmeticFunction.moebius n : ℝ) * (⌊x/n⌋ : ℝ) = 1 := by  norm_cast  convert ArithmeticFunction.sum_Ioc_mul_zeta_eq_sum μ ⌊x⌋₊ |>.symm using 1  · rw [Iic_eq_Icc, bot_eq_zero, ← add_sum_Ioc_eq_sum_Icc (by simp)]    simp only [ArithmeticFunction.map_zero, CharP.cast_eq_zero, div_zero, Int.floor_zero, mul_zero,      zero_add, Int.natCast_ediv]    refine sum_congr rfl fun n hn ↦ ?_    congr    norm_cast    rw [← floor_div_natCast, Int.natCast_floor_eq_floor]    positivity  · simpa [moebius_mul_coe_zeta, one_apply]