Erdos392.Params.initial.balance_medium_prime_le

@[blueprint  "initial-factorization-medium-prime-le"  (statement := /-- A medium prime $\sqrt{n} < p ≤ n/L$ can be in surplus by at most $M$.-/)  (proof := /-- Routine computation using Legendre's formula.-/)  (latexEnv := "sublemma")]theorem Params.initial.balance_medium_prime_le (P : Params) {p : ℕ} (hp : p > Real.sqrt P.n) :    P.initial.balance p ≤ P.M := by  by_cases hprime : p.Prime  · have : (P.initial.a.map (·.factorization p)).sum ≤ P.n / p + P.M := by      calc (P.initial.a.map (·.factorization p)).sum        _ ≤ P.M * (Finset.filter (p ∣ ·) (.Ico (P.n - P.n / P.M) P.n)).card :=            sum_valuation_le_M_mul_interval_count P hp        _ ≤ P.M * ((P.n / P.M + p - 1) / p) := mul_le_mul_left _ <| by            convert count_multiples_le (P.n - P.n / P.M) P.n p hprime.pos using 1            rw [Nat.sub_sub_self (div_le_self _ _)]        _ ≤ P.n / p + P.M := by          have := count_bound_aux P.n P.M p          grind    simp only [Factorization.balance, Factorization.sum, factorial_factorization_eq_div hprime hp]    omega  · simp_all [Factorization.balance, Factorization.sum]