Source indexedlemma · leanprover/lean4:v4.32.0

Erdos392.Params.initial.balance_ge_neg_M_mul_log

PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1514 to 1527

Source documentation

The balance of a small prime p is at least -M * floor(log_p n).

Exact Lean statement

lemma Params.initial.balance_ge_neg_M_mul_log (P : Params) {p : ℕ} (hp : p.Prime)
    (hp_le : p ≤ Real.sqrt P.n) (hp_gt : p > P.L) :
    P.initial.balance p ≥ - (P.M * (Nat.log p P.n) : ℤ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Params.initial.balance_ge_neg_M_mul_log (P : Params) {p : ℕ} (hp : p.Prime)    (hp_le : p ≤ Real.sqrt P.n) (hp_gt : p > P.L) :    P.initial.balance p ≥ - (P.M * (Nat.log p P.n) : ℤ) := by  have := Fact.mk hp  rw [Factorization.balance, Factorization.sum, initial.sum_valuation_eq_small P hp hp_le hp_gt,    factorization_def _ hp, padicValNat_factorial]  · simp only [cast_mul, cast_sum, Int.natCast_ediv, cast_pow, ge_iff_le, neg_le_sub_iff_le_add]    calc      _ ≤ ∑ k ∈ Ico 1 (Nat.log p P.n + 1), ((P.M : ℤ) *          (Finset.filter (p^k ∣ ·) (Ico (P.n - P.n / P.M) P.n)).card + P.M) :=        sum_le_sum fun k _ ↦ mod_cast initial.count_multiples_lower_bound P.n P.M (p^k)          (by linarith [P.hM]) (pow_pos hp.pos _)      _ = _ := by simp [sum_add_distrib, mul_sum, mul_comm]  · exact lt_succ_self _