Source indexedlemma · leanprover/lean4:v4.32.0

sum_mobius_floor

PrimeNumberTheoremAnd.Consequences · PrimeNumberTheoremAnd/Consequences.lean:2254 to 2262

Mathematical statement

Exact Lean statement

lemma sum_mobius_floor (x : ℝ) (hx : 1 ≤ x) : ∑ n ∈ Icc 1 ⌊x⌋₊, (μ n : ℝ) * ⌊x / n⌋ = 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma sum_mobius_floor (x : ℝ) (hx : 1 ≤ x) : ∑ n ∈ Icc 1 ⌊x⌋₊, (μ n : ℝ) * ⌊x / n⌋ = 1 := by  classical  have h := sum_mobius_mul_floor x hx  have h0 : (0 : ℕ) ∈ Iic ⌊x⌋₊ := by simp [Finset.mem_Iic]  have hI : (Iic ⌊x⌋₊).erase 0 = Icc 1 ⌊x⌋₊ := by    ext n    simp [Finset.mem_Iic, Finset.mem_Icc, Nat.one_le_iff_ne_zero, and_comm]  rw [← Finset.sum_erase_add (Iic ⌊x⌋₊) (fun n => (μ n : ℝ) * (⌊x / n⌋ : ℝ)) h0] at h  simpa [hI] using h