Erdos392.Params.initial.balance_small_prime_ge

@[blueprint  "initial-factorization-small-prime-ge"  (statement := /-- A small prime $L < p \leq \sqrt{n}$ can be in deficit by at most  $M\log n$.-/)  (proof := /-- Routine computation using Legendre's formula, noting that at most  $\log n / \log 2$ powers of $p$ divide any given number up to $n$.-/)  (latexEnv := "sublemma")  (discussion := 514)]theorem Params.initial.balance_small_prime_ge (P : Params) {p : ℕ} (hp : p ≤ Real.sqrt P.n)    (hp' : p > P.L) : P.initial.balance p ≥ - P.M * (Real.log P.n) / (Real.log 2) := by  have h_bound_ℝ : (P.initial.balance p : ℝ) ≥ -(P.M * (Real.log P.n / Real.log p)) := by    refine le_trans (b := - (P.M * (Nat.log p P.n : ℝ))) ?_ ?_    · gcongr      have h_p_gt_1 : 1 < p := lt_of_le_of_lt (succ_le_of_lt P.hL_pos) hp'      have hn_pos : 0 < P.n := by        refine pos_iff_ne_zero.mpr fun h ↦ ?_        simp only [h, CharP.cast_eq_zero, Real.sqrt_zero, cast_nonpos] at hp        linarith [hp, hp', P.hL_pos]      rw [le_div_iff₀ (log_pos (by exact_mod_cast lt_of_le_of_lt (succ_le_of_lt P.hL_pos) hp'))]      nth_rw 1 [← Real.log_pow]      exact log_le_log (by positivity) <|        by norm_cast; exact pow_log_le_self p (Nat.ne_of_gt hn_pos)    norm_cast    by_cases hp_prime : p.Prime    · simpa using initial.balance_ge_neg_M_mul_log P hp_prime hp hp'    · simp only [cast_mul, Factorization.balance, hp_prime, not_false_eq_true,        factorization_eq_zero_of_not_prime, CharP.cast_eq_zero, sub_zero]      rw [neg_le_iff_add_nonneg']      positivity  exact le_trans (by    rw [mul_div]; ring_nf; gcongr; norm_cast; linarith [P.hL_pos]) h_bound_ℝ