Erdos392.Params.initial.balance_large_prime_ge

@[blueprint  "initial-factorization-large-prime-ge"  (statement := /-- A large prime $p \geq n/L$ can be in deficit by at most $n/p$. -/)  (proof := /-- This is the number of times $p$ can divide $n!$. -/)  (latexEnv := "sublemma")]theorem Params.initial.balance_large_prime_ge (P : Params) {p : ℕ}    (hp : p ≥ P.n / P.L) : P.initial.balance p ≥ -(P.n / p) := by  have hsum : (P.initial.a.map (·.factorization p)).sum = 0 := sum_eq_zero fun x hx ↦ by    simp only [Multiset.mem_map, initial, Multiset.mem_filter] at hx    obtain ⟨m, ⟨_, hsmooth⟩, rfl⟩ := hx    rw [factorization_eq_zero_iff, mem_smoothNumbers'] at *    by_cases hprime : p.Prime    · by_cases hdvd : p ∣ m      · exact ((hsmooth p hprime hdvd).not_ge hp).elim      · exact .inr (.inl hdvd)    · exact .inl hprime  have hfact : (P.n.factorial.factorization p : ℤ) ≤ P.n / p := by    rcases eq_or_ne p 0 with rfl | -; · simp    by_cases hprime : p.Prime    · have hn_pos : (0 : ℝ) < P.n := by        have := Nat.lt_of_lt_of_le (Nat.mul_pos P.hL_pos P.hL_pos) P.hL.le        exact_mod_cast this      have hL_lt_sqrt : (P.L : ℝ) < Real.sqrt P.n := by        rw [Real.lt_sqrt (Nat.cast_nonneg _)]; exact_mod_cast by nlinarith [P.hL]      have hp_gt_sqrt : (p : ℝ) > Real.sqrt P.n := calc        (p : ℝ) ≥ (P.n / P.L : ℕ) := by exact_mod_cast hp        _ > Real.sqrt P.n := P.hL'      rw [factorial_factorization_eq_div hprime hp_gt_sqrt,        Int.le_ediv_iff_mul_le (by exact_mod_cast hprime.pos)]      exact_mod_cast Nat.div_mul_le_self P.n p    · simp only [Nat.factorization_eq_zero_of_not_prime _ hprime, Nat.cast_zero]; positivity  simp only [Factorization.balance, Factorization.sum, hsum, Nat.cast_zero, zero_sub,    neg_le_neg_iff, hfact]