Source indexedlemma · leanprover/lean4:v4.32.0

Erdos392.Params.initial.term_bound

PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1317 to 1330

Source documentation

The contribution of the k-th power of p to the balance is bounded by M. Specifically, M * count(p^k) ≤ floor(n/p^k) + M.

Exact Lean statement

lemma Params.initial.term_bound (P : Params) {p k : ℕ} (hp : p.Prime) :
    P.M * ((Finset.Ico (P.n - P.n / P.M) P.n).filter (p ^ k ∣ ·)).card ≤
      P.n / p ^ k + P.M

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Params.initial.term_bound (P : Params) {p k : ℕ} (hp : p.Prime) :    P.M * ((Finset.Ico (P.n - P.n / P.M) P.n).filter (p ^ k ∣ ·)).card ≤      P.n / p ^ k + P.M := by  calc    _ ≤ P.M * ((P.n / P.M + p ^ k - 1) / p ^ k) := Nat.mul_le_mul_left _ (by        convert initial.count_multiples_le (P.n - P.n / P.M) P.n (p ^ k) <|          pow_pos hp.pos k using 1        rw [Nat.sub_sub_self (div_le_self _ _)])    _ ≤ P.M * (P.n / P.M / p ^ k + 1) := mul_le_mul_left _      (by rw [← add_div_right _ <| pow_pos hp.pos k]; exact Nat.div_le_div_right <| sub_le ..)    _ ≤ P.n / p ^ k + P.M := by        rw [mul_add, mul_one]        exact Nat.add_le_add_right (le_trans (mul_div_le_mul_div_assoc ..)          (Nat.div_le_div_right <| by rw [mul_comm]; exact div_mul_le_self ..)) ..