Erdos392.Params.initial.balance_tiny_prime_ge

@[blueprint  "initial-factorization-tiny-prime-ge"  (statement := /-- A tiny prime $p \leq L$ can be in deficit by at most $M\log n + ML\pi(n)$.-/)  (proof := /-- In addition to the Legendre calculations, one potentially removes factors of the  form $plq$ with $l \leq L$ and $q \leq n$ a prime up to $M$ times each, with at most $L$ copies  of $p$ removed at each factor.-/)  (latexEnv := "sublemma")  (discussion := 515)]theorem Params.initial.balance_tiny_prime_ge (P : Params) {p : ℕ} (hp : p ≤ P.L) :    P.initial.balance p ≥ -P.M * Real.log P.n - P.M * P.L ^ 2 * primeCounting P.n := by  have h_full := initial_full_balance_ge P  by_cases hprime : p.Prime  · have h_eq := initial_balance_eq P p    have h_sum := rough_valuation_sum_le P p hp hprime    have h_aux := balance_inequality_aux P p hprime    simp_all only [neg_mul, div_eq_mul_inv, ge_iff_le, one_mul, Int.cast_sub, Int.cast_mul,      Int.cast_natCast, Int.cast_sum, tsub_le_iff_right]    norm_num [← @Int.cast_inj ℝ] at *    nlinarith [h_full p hprime,      (by norm_cast : (∑ m ∈ rough_set P, (m.factorization p : ℕ) : ℝ) ≤        P.n.primeCounting * P.L * Nat.log p P.L),      Real.log_pos one_lt_two, mul_inv_cancel₀          (ne_of_gt (log_pos one_lt_two))]  · simp only [Factorization.balance, hprime, not_false_eq_true,      factorization_eq_zero_of_not_prime,      CharP.cast_eq_zero, sub_zero, Int.cast_natCast,      neg_mul, ge_iff_le, tsub_le_iff_right]    exact le_trans (neg_nonpos_of_nonneg (by positivity)) (by positivity)