Source indexedtheorem · leanprover/lean4:v4.32.0

MobiusLemma.mobius_lemma_2_sub_1

PrimeNumberTheoremAnd.IEANTN.MobiusLemma · PrimeNumberTheoremAnd/IEANTN/MobiusLemma.lean:401 to 426

Source documentation

Since our sums start from $1$ , the sum $\sum_{k\leq K}$ is empty for $K=0$ .

Exact Lean statement

@[blueprint
  "mobius-lemma-2-sub-1"
  (title := "Mobius Lemma 2 - first step")
  (statement := /--
    For any $K \leq x$,
    $$
    \sum_{k\leq x} M\left(\sqrt{\frac{x}{k}}\right) = \sum_{k\leq K} M\left(\sqrt{\frac{x}{k}}\right)
    + \sum_{K < k\leq x+1} \int_{k-\frac{1}{2}}^{k+\frac{1}{2}}
      M\left(\sqrt{\frac{x}{k}}\right) du.
    $$
  -/)
  (proof := /-- This is just splitting the sum at $K$. -/)
  (latexEnv := "sublemma")
  (discussion := 528)]
theorem mobius_lemma_2_sub_1 (x : ℝ) (hx : x > 0) (K : ℕ) (hK : (K : ℝ) ≤ x) :
    ∑ k ∈ Ioc 0 ⌊x⌋₊, M (Real.sqrt (x / k)) = ∑ k ∈ range (K + 1), M (Real.sqrt (x / k)) +
      ∑ k ∈ Ico (K + 1) (⌊x⌋₊ + 2), ∫ _ in (k - 0.5)..(k + 0.5), (M (Real.sqrt (x / k)) : ℝ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "mobius-lemma-2-sub-1"  (title := "Mobius Lemma 2 - first step")  (statement := /--    For any $K \leq x$,    $$    \sum_{k\leq x} M\left(\sqrt{\frac{x}{k}}\right) = \sum_{k\leq K} M\left(\sqrt{\frac{x}{k}}\right)    + \sum_{K < k\leq x+1} \int_{k-\frac{1}{2}}^{k+\frac{1}{2}}      M\left(\sqrt{\frac{x}{k}}\right) du.    $$  -/)  (proof := /-- This is just splitting the sum at $K$. -/)  (latexEnv := "sublemma")  (discussion := 528)]theorem mobius_lemma_2_sub_1 (x : ℝ) (hx : x > 0) (K : ℕ) (hK : (K : ℝ) ≤ x) :    ∑ k ∈ Ioc 0 ⌊x⌋₊, M (Real.sqrt (x / k)) = ∑ k ∈ range (K + 1), M (Real.sqrt (x / k)) +      ∑ k ∈ Ico (K + 1) (⌊x⌋₊ + 2), ∫ _ in (k - 0.5)..(k + 0.5), (M (Real.sqrt (x / k)) : ℝ) := by  norm_num [sum_Ico_eq_sub]  rw [sum_range_add_sum_Ico]  · erw [← Icc_succ_left_eq_Ioc, sum_Ico_eq_sub _]    · norm_num [Finset.sum_range_succ, M]      rw [Nat.floor_eq_zero.mpr]      · norm_num      · rw [div_lt_one (by positivity), sqrt_lt_sqrt_iff] <;> linarith [Nat.lt_floor_add_one x]    · simp  · linarith [Nat.le_floor hK]