Erdos392.Params.initial.balance_medium_prime_ge

@[blueprint  "initial-factorization-medium-prime-ge"  (statement := /-- A medium prime $\sqrt{n} < p ≤ n/L$ can be in deficit by at most $M$.-/)  (proof := /-- The number of times $p$ divides $a_1 \dots a_t$ is at least $M \lfloor n/Mp  \rfloor ≥ n/p - M$ (note that the removal of the non-smooth numbers  does not remove any multiples  of $p$).  Meanwhile, the number of times $p$ divides $n!$ is at most $n/p$.-/)  (latexEnv := "sublemma")]theorem Params.initial.balance_medium_prime_ge (P : Params) {p : ℕ} (hp : p < P.n / P.L)    (hp' : p > Real.sqrt P.n) : P.initial.balance p ≥ -P.M := by  by_cases hp_prime : p.Prime  · have : (P.initial.a.map (·.factorization p)).sum ≥ P.n / p - P.M :=      (initial.sum_valuation_eq P hp_prime hp' hp).symm ▸ sub_le_of_le_add        (initial.count_multiples_lower_bound P.n P.M p (by linarith [P.hM]) hp_prime.pos)    simp only [Factorization.balance, Factorization.sum,      factorial_factorization_eq_div hp_prime hp']    omega  · simp_all [Factorization.balance, Factorization.sum]