Source indexedlemma · leanprover/lean4:v4.32.0

Erdos392.Params.initial_full_sum_valuation_eq

PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1602 to 1622

Source documentation

The sum of valuations in [n - n/M, n) equals ∑ k ∈ [1, log_p n], #{m ∈ I | p^k ∣ m}.

Exact Lean statement

lemma Params.initial_full_sum_valuation_eq (P : Params) (p : ℕ) (hp : p.Prime) :
    ∑ m ∈ Finset.Ico (P.n - P.n / P.M) P.n, (m.factorization p : ℤ) =
    ∑ k ∈ Finset.Ico 1 (Nat.log p P.n + 1),
      ((filter (p ^ k ∣ ·) (Finset.Ico (P.n - P.n / P.M) P.n)).card : ℤ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Params.initial_full_sum_valuation_eq (P : Params) (p : ℕ) (hp : p.Prime) :    ∑ m ∈ Finset.Ico (P.n - P.n / P.M) P.n, (m.factorization p : ℤ) =    ∑ k ∈ Finset.Ico 1 (Nat.log p P.n + 1),      ((filter (p ^ k ∣ ·) (Finset.Ico (P.n - P.n / P.M) P.n)).card : ℤ) := by  by_cases hPn : P.n = 0  · simp_all  · have h_zero : ∀ k > log p P.n,        (filter (p ^ k ∣ ·) (Finset.Ico (P.n - P.n / P.M) P.n)).card = 0 :=      fun k hk ↦ card_eq_zero.mpr (filter_eq_empty_iff.mpr fun x hx hdiv ↦ by        have hx_pos : 0 < x := pos_of_ne_zero fun h ↦ by          rw [Finset.mem_Ico, h] at hx          exact not_lt.mpr hx.1 (Nat.sub_pos_of_lt (div_lt_self hx.2 P.hM))        exact not_lt.mpr (le_of_dvd hx_pos hdiv) <| (Finset.mem_Ico.mp hx).2.trans_le          (lt_pow_of_log_lt hp.one_lt hk).le)    rw_mod_cast [sum_factorization_eq_sum_multiples]    · rw [← sum_subset (Ico_subset_Ico_right (succ_le_of_lt        (log_lt_of_lt_pow hPn (show P.n < p ^ P.n from Nat.recOn P.n (by norm_num)          fun n ihn ↦ by rw [_root_.pow_succ']; nlinarith [hp.one_lt, ihn]))))]      aesop    · assumption    · exact Nat.sub_pos_of_lt (div_lt_self (pos_of_ne_zero hPn) P.hM)