Erdos392.Factorization.lower_score_2

@[blueprint  "score-lower-2"  (statement := /-- If there is a prime $p$ in deficit larger than $L$, one can remove it without  increasing the score.-/)  (proof := /-- Add an additional factor of $p$ to the factorization.-/)  (latexEnv := "sublemma")]theorem Factorization.lower_score_2 {n : ℕ} (f : Factorization n) (L : ℕ)    (hf : ∃ p ∈ (n + 1).primesBelow, p > L ∧ f.balance p < 0) :    ∃ f' : Factorization n,      f'.total_imbalance < f.total_imbalance ∧ f'.score L ≤ f.score L := by  obtain ⟨p, hp_mem, hp_gt_L, hp_balance⟩ := hf  have hp := prime_of_mem_primesBelow hp_mem  set f' : Factorization n := ⟨f.a + {p}, fun m hm => by    simp only [Multiset.mem_add, Multiset.mem_singleton] at hm    rcases hm with hm | rfl    · exact f.ha m hm    · exact le_of_lt_succ (lt_of_mem_primesBelow hp_mem),    fun m hm ↦ by    simp only [Multiset.mem_add, Multiset.mem_singleton] at hm    rcases hm with hm | rfl    · exact f.hpos m hm    · exact hp.pos⟩  have h_balance_p : f'.balance p = f.balance p + 1 := by    unfold balance sum    simp only [show f'.a = f.a + {p} from rfl, Multiset.map_add, Multiset.sum_add,      Multiset.map_singleton, Multiset.sum_singleton, Prime.factorization_self hp]    omega  have h_balance_q : ∀ q, q ≠ p → f'.balance q = f.balance q := fun q hq ↦ by    have hq_fac : p.factorization q = 0 := by      rw [Prime.factorization hp]      simp [hq.symm]    unfold balance sum    simp only [show f'.a = f.a + {p} from rfl, Multiset.map_add, Multiset.sum_add,      Multiset.map_singleton, Multiset.sum_singleton, hq_fac, add_zero]  have h_total_imbalance : f'.total_imbalance < f.total_imbalance := by    refine Finset.sum_lt_sum (fun q _ ↦ ?_) ⟨p, hp_mem, by rw [h_balance_p]; omega⟩    by_cases hq : q = p    · subst hq; rw [h_balance_p]; omega    · rw [h_balance_q q hq]  have h_waste : f'.waste ≤ f.waste + Real.log (n / p) := by    unfold waste sum    simp only [show f'.a = f.a + {p} from rfl, Multiset.map_add, Multiset.sum_add,      Multiset.map_singleton, Multiset.sum_singleton]    linarith  have h_sum_q : ∀ q ∈ (n + 1).primesBelow, q ≠ p →      (if f'.balance q > 0 then (f'.balance q : ℝ) * Real.log q       else if q ≤ L then (-f'.balance q) * Real.log L else (-f'.balance q) * Real.log (n / q)) =      (if f.balance q > 0 then (f.balance q : ℝ) * Real.log q       else if q ≤ L then (-f.balance q) * Real.log L       else (-f.balance q) * Real.log (n / q)) := by    intro q _ hqp    rw [h_balance_q q hqp]  have h_term_p : (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)) ≤      (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 / p) := by    rw [h_balance_p]    split_ifs <;> try linarith    push_cast    ring_nf    norm_num  have h_sum_term : ∑ q ∈ (n + 1).primesBelow,      (if f'.balance q > 0 then (f'.balance q : ℝ) * Real.log q       else if q ≤ L then (-f'.balance q) * Real.log L       else (-f'.balance q) * Real.log (n / q)) ≤      ∑ q ∈ (n + 1).primesBelow,      (if f.balance q > 0 then (f.balance q : ℝ) * Real.log q       else if q ≤ L then (-f.balance q) * Real.log L else (-f.balance q) * Real.log (n / q)) -      Real.log (n / p) := by    rw [← Finset.add_sum_erase _ _ hp_mem, ← Finset.add_sum_erase _ _ hp_mem]    have h_rest := Finset.sum_congr rfl fun x hx ↦      h_sum_q x (Finset.mem_erase.mp hx).2 (Finset.mem_erase.mp hx).1    linarith  have h_penalty : (if f'.total_imbalance > 0 then Real.log n else 0) ≤      (if f.total_imbalance > 0 then Real.log n else 0) := by    split_ifs <;> first | linarith | positivity  have h_score : f'.score L ≤ f.score L := by    unfold score    linarith  exact ⟨f', h_total_imbalance, h_score⟩