Erdos392.Params.initial_full_balance_ge

lemma Params.initial_full_balance_ge (P : Params) (p : ℕ) (hp : p.Prime) :    (initial_full P).balance p ≥ -P.M * Real.log P.n / Real.log 2 := by  have h_balance : (initial_full P).balance p = P.M * (∑ k ∈ Finset.Ico 1 (Nat.log p P.n + 1),    ((filter (p ^ k ∣ ·) (Finset.Ico (P.n - P.n / P.M) P.n)).card : ℤ)) -      (∑ k ∈ Finset.Ico 1 (Nat.log p P.n + 1), (P.n / p ^ k : ℤ)) := by    convert initial_full_balance_eq P p using 1    congr! 2    · exact (initial_full_sum_valuation_eq P p hp).symm    · rw [factorization_def]      · have := Fact.mk hp; rw [padicValNat_factorial] <;> aesop      · assumption  have h_term : ∀ k ∈ Finset.Ico 1 (log p P.n + 1),      (P.M : ℤ) * ((filter (p ^ k ∣ ·) (Finset.Ico (P.n - P.n / P.M) P.n)).card : ℤ) -      (P.n / p ^ k : ℤ) ≥ -P.M := fun k _ ↦ initial_full_term_bound P p k hp.pos  have h_sum : (P.M : ℤ) * (∑ k ∈ Finset.Ico 1 (log p P.n + 1),      ((filter (p ^ k ∣ ·) (Finset.Ico (P.n - P.n / P.M) P.n)).card : ℤ)) -      (∑ k ∈ Finset.Ico 1 (log p P.n + 1), (P.n / p ^ k : ℤ)) ≥ -P.M * log p P.n := by    simpa [mul_comm, mul_sum, sum_mul] using sum_le_sum h_term  have hn_pos : P.n > 0 := by nlinarith [P.hL, P.hL_pos]  have h_log : (log p P.n : ℝ) ≤ Real.log P.n / Real.log 2 := by    rw [le_div_iff₀ (log_pos one_lt_two), ← Real.log_pow]    gcongr    norm_cast    exact (pow_le_pow_left' hp.two_le _).trans (Nat.pow_log_le_self _ hn_pos.ne')  simp_all only [Finset.mem_Ico, Order.lt_add_one_iff, ge_iff_le, neg_le_sub_iff_le_add,    and_imp, neg_mul, Int.cast_sub, Int.cast_mul, Int.cast_natCast, Int.cast_sum]  rw [div_le_iff₀ (by positivity)] at *  rw [le_div_iff₀ (log_pos (by norm_num))] at h_log  norm_num [← @Int.cast_le ℝ] at *  nlinarith [Real.log_pos one_lt_two]