Erdos392.Factorization.lower_score_3_case2a

lemma Factorization.lower_score_3_case2a {n : ℕ} (f : Factorization n) (L : ℕ)    (h_surplus : ∀ p, f.balance p ≤ 0)    (hf : ∃ p ∈ (n + 1).primesBelow, p ≤ L ∧ f.balance p < 0) (hL_gt_n : L > n) :    ∃ f' : Factorization n,      f'.total_imbalance < f.total_imbalance ∧ f'.score L ≤ f.score L := by  obtain ⟨p, hp_mem, hp_le_L, hp_def⟩ := hf  have hp_le_n : p ≤ n := Nat.lt_succ_iff.mp (mem_primesBelow.mp hp_mem).1  have hp_pos : 0 < p := (prime_of_mem_primesBelow hp_mem).pos  have hn_pos : 0 < n := hp_pos.trans_le hp_le_n  have hp_prime : p.Prime := prime_of_mem_primesBelow hp_mem  have h_imb : (addFactor f p hp_le_n hp_pos).total_imbalance = f.total_imbalance - 1 := by    have hM : {p} ≤ deficitMultiset f L := Multiset.singleton_le.mpr <|      Multiset.mem_bind.mpr ⟨p, Finset.mem_filter.mpr ⟨hp_mem, hp_le_L, hp_def⟩,        Multiset.mem_replicate.mpr ⟨(Int.natAbs_pos.mpr hp_def.ne).ne', rfl⟩⟩    simpa using addFactor_submultiset_total_imbalance f L h_surplus {p} hM p      hp_le_n hp_pos (Multiset.prod_singleton (a := p)).symm  have h_bal : (addFactor f p hp_le_n hp_pos).balance p = f.balance p + 1 := by    rw [addFactor_balance, hp_prime.factorization, Finsupp.single_eq_same]; ring  have h_bal_eq : ∀ q ∈ (n + 1).primesBelow, q ≠ p →      (addFactor f p hp_le_n hp_pos).balance q = f.balance q := fun q hq hq_ne_p ↦ by    rw [addFactor_balance, factorization_eq_zero_of_not_dvd, Int.ofNat_zero, add_zero]    exact fun hdvd ↦      hq_ne_p ((prime_dvd_prime_iff_eq (prime_of_mem_primesBelow hq) hp_prime).mp hdvd)  have h_score_sum := score_sum_change f (addFactor f p hp_le_n hp_pos) L p hp_mem hp_le_L hp_def    h_bal h_bal_eq  have h_waste := addFactor_waste f p hp_le_n hp_pos  have h_total_imb_pos : f.total_imbalance > 0 :=    (Int.natAbs_pos.mpr hp_def.ne).trans_le      (Finset.single_le_sum (fun q _ ↦ (Int.natAbs (f.balance q)).zero_le) hp_mem)  have h_imbalance_penalty :      (addFactor f p hp_le_n hp_pos).score L ≤ f.score L + Real.log (n / p) - Real.log L := by    unfold score at *    have h_log_n : log (n : ℝ) ≥ 0 := log_nonneg (by exact_mod_cast hn_pos)    split_ifs at * <;> linarith [h_score_sum, h_waste, h_total_imb_pos]  refine ⟨addFactor f p hp_le_n hp_pos, ?_, h_imbalance_penalty.trans ?_⟩  · exact h_imb ▸ sub_lt h_total_imb_pos one_pos  · rw [add_sub_assoc]    refine add_le_of_nonpos_right (sub_nonpos_of_le (log_le_log (by positivity) ?_))    rw [div_le_iff₀ (by positivity : (0 : ℝ) < p)]    have h1 : (n : ℝ) * 1 ≤ n * p := by      exact_mod_cast mul_le_mul_left n <| one_le_iff_ne_zero.mpr hp_pos.ne'    have h2 : (n : ℝ) * p < L * p := by exact_mod_cast mul_lt_mul_of_pos_right hL_gt_n hp_pos    linarith