Source indexedlemma · leanprover/lean4:v4.32.0

Erdos392.sum_factorization_eq_sum_multiples

PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1295 to 1313

Source documentation

The sum of p-adic valuations of numbers in an interval equals the sum over k of the count of multiples of p^k in that interval.

Exact Lean statement

lemma sum_factorization_eq_sum_multiples {A B p : ℕ} (hp : p.Prime) (hA : 0 < A) :
    ∑ m ∈ .Ico A B, m.factorization p =
      ∑ k ∈ .Ico 1 B, ((Finset.Ico A B).filter (p ^ k ∣ ·)).card

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma sum_factorization_eq_sum_multiples {A B p : ℕ} (hp : p.Prime) (hA : 0 < A) :    ∑ m ∈ .Ico A B, m.factorization p =      ∑ k ∈ .Ico 1 B, ((Finset.Ico A B).filter (p ^ k ∣ ·)).card := by  have h_factorization : ∀ m ∈ Finset.Ico A B, m.factorization p = ∑ k ∈ .Ico 1 B,      if p^k ∣ m then 1 else 0 := fun m hm ↦ by    have hm' : m ≠ 0 := (hA.trans_le (Finset.mem_Ico.mp hm).1).ne'    have : (Finset.Ico 1 B).filter (p^· ∣ m) = Finset.Ico 1 (m.factorization p + 1) := by      ext k      simp only [Finset.mem_filter, Finset.mem_Ico]      exact ⟨fun ⟨⟨h1, _⟩, h2⟩ ↦ ⟨h1, Nat.lt_succ_iff.mpr <| le_of_not_gt fun h ↦        pow_succ_factorization_not_dvd hm' hp <| (pow_dvd_pow p h).trans h2⟩,        fun ⟨h1, h2⟩ ↦          ⟨⟨h1, (le_of_lt_succ h2).trans_lt            (factorization_lt p hm') |>.trans_le            (Finset.mem_Ico.mp hm).2.le⟩,            (pow_dvd_pow p (le_of_lt_succ h2)).trans (ordProj_dvd m p)⟩⟩    simp [sum_boole, this]  rw [sum_congr rfl h_factorization, sum_comm]  simp [sum_boole]