Erdos392.Factorization.waste_eq

@[blueprint  "waste-eq"  (statement := /-- The waste of a factorization is equal to $t \log n - \log n!$, where $t$ is the  number of elements.-/)  (latexEnv := "lemma")]theorem Factorization.waste_eq {n : ℕ} (f : Factorization n) (hf : f.total_imbalance = 0) :    f.a.card * (Real.log n) = Real.log n.factorial + f.waste := by  unfold waste sum  have hlog : log (n.factorial : ℝ) = (f.a.map (fun m : ℕ ↦ log (m : ℝ))).sum := by    rw [← f.zero_total_imbalance hf, prod, map_id, cast_multiset_prod, log_multiset_prod,      Multiset.map_map]    · rfl    · exact fun x hx ↦ by        obtain ⟨m, hm, rfl⟩ := Multiset.mem_map.mp hx; exact cast_ne_zero.mpr (f.hpos m hm).ne'  rcases eq_or_ne n 0 with rfl | hn  · simp [Multiset.eq_zero_of_forall_notMem       fun m hm ↦ (f.hpos m hm).ne' (le_zero.mp (f.ha m hm))]  · have hn_pos : (0 : ℝ) < n := cast_pos.mpr (pos_of_ne_zero hn)    rw [hlog, ← Multiset.sum_map_add]    conv_lhs => rw [show f.a.card * log (n : ℝ) = (f.a.map (fun _ ↦ log (n : ℝ))).sum from      by rw [Multiset.map_const', Multiset.sum_replicate, nsmul_eq_mul]]    exact congrArg _ (Multiset.map_congr rfl fun m hm ↦ by      rw [Real.log_div hn_pos.ne' (cast_ne_zero.mpr (f.hpos m hm).ne')]; ring)