Erdos392.Factorization.score_le_of_add_submultiset

lemma Factorization.score_le_of_add_submultiset {n : ℕ} (f : Factorization n) (L : ℕ)    (M : Multiset ℕ) (hM_le : M ≤ deficitMultiset f L)    (m : ℕ) (hm : m ≤ n) (hm_pos : 0 < m) (h_m_prod : m = M.prod)    (h_prod_gt : n < m * L) (hM_card_pos : 0 < M.card) (hL_ge_2 : 2 ≤ L) :    (addFactor f m hm hm_pos).score L ≤ f.score L := by  unfold score  let f' := addFactor f m hm hm_pos  have h_sum_eq : (∑ p ∈ (n + 1).primesBelow,      if f'.balance p > 0 then (f'.balance p : ℝ) * Real.log p      else if p ≤ L then -(f'.balance p : ℝ) * Real.log L      else -(f'.balance p : ℝ) * Real.log (n / p)) -    (∑ p ∈ (n + 1).primesBelow,      if f.balance p > 0 then (f.balance p : ℝ) * Real.log p      else if p ≤ L then -(f.balance p : ℝ) * Real.log L      else -(f.balance p : ℝ) * Real.log (n / p)) = -M.card * Real.log L := by    convert score_sum_change_multiset f f' L M hM_le (fun p _ ↦ ?_) using 1    · norm_num [Finset.sum_ite]    · simp only [f', addFactor_balance]      rw [h_m_prod, factorization_prod_eq_count (fun q hq ↦        (mem_deficitMultiset f L q (Multiset.mem_of_le hM_le hq)).1)]  have h_waste_eq : f'.waste = f.waste + Real.log (n / m) := addFactor_waste f m hm hm_pos  have h_score_diff : f'.waste + (∑ p ∈ (n + 1).primesBelow,      if f'.balance p > 0 then (f'.balance p : ℝ) * Real.log p      else if p ≤ L then -(f'.balance p : ℝ) * Real.log L      else -(f'.balance p : ℝ) * Real.log (n / p)) ≤    (f.waste + (∑ p ∈ (n + 1).primesBelow,      if f.balance p > 0 then (f.balance p : ℝ) * Real.log p      else if p ≤ L then -(f.balance p : ℝ) * Real.log L      else -(f.balance p : ℝ) * Real.log (n / p))) + (Real.log n - Real.log m - Real.log L) := by    rw [Real.log_div (by norm_cast; omega) (by positivity)] at h_waste_eq    nlinarith [show (M.card : ℝ) ≥ 1 by norm_cast,      log_nonneg (show (L : ℝ) ≥ 1 by norm_cast; omega),        log_le_log (by positivity) (by norm_cast : (m : ℝ) ≤ n)]  split_ifs with h_imb_pos h_imb_zero <;> norm_num at *  · have h_log_sum : Real.log m + Real.log L ≥ Real.log n := by      rw [← log_mul (by positivity) (by positivity)]      exact log_le_log (by norm_cast; omega) (by norm_cast; omega)    linarith  · have h_bal_zero : ∀ p ∈ (n + 1).primesBelow, f.balance p = 0 := by      unfold total_imbalance at h_imb_zero      aesop    have h_deficit_empty : deficitMultiset f L = 0 := by      unfold deficitMultiset      aesop    simp [Multiset.le_zero.mp (h_deficit_empty ▸ hM_le)] at hM_card_pos  · linarith [log_nonneg (show (m : ℝ) ≥ 1 by norm_cast),      log_nonneg (show (L : ℝ) ≥ 1 by norm_cast; omega)]  · refine h_score_diff.trans ?_    norm_num [add_assoc]    rw [← log_mul (by positivity) (by positivity), log_le_log_iff] <;> norm_cast <;> nlinarith