Erdos392.Params.initial.sum_valuation_le_M_mul_interval_count

lemma Params.initial.sum_valuation_le_M_mul_interval_count (P : Params) {p : ℕ}    (hp' : (p : ℝ) > Real.sqrt P.n) : (P.initial.a.map (·.factorization p)).sum ≤      P.M * (Finset.filter (p ∣ ·) (Finset.Ico (P.n - P.n / P.M) P.n)).card := by  set S := Multiset.join (Multiset.replicate P.M (Multiset.Ico (P.n - P.n / P.M) P.n))  have hle : P.initial.a ≤ S := by    unfold initial    aesop  have hval : ∀ m ∈ S, m.factorization p ≤ if p ∣ m then 1 else 0 := fun m hm ↦ by    have h1 : m.factorization p ≤ 1 := by      by_cases hm_zero : m = 0      · simp [hm_zero]      · have hm_lt : (m : ℝ) < p ^ 2 := by          have : (m : ℝ) < P.n := by            simp only [S, Multiset.mem_join, Multiset.mem_replicate] at hm            obtain ⟨_, ⟨_, rfl⟩, hs₂⟩ := hm            aesop          nlinarith [sqrt_nonneg P.n, mul_self_sqrt (cast_nonneg P.n)]        norm_cast at hm_lt        exact le_of_not_gt fun h ↦ hm_lt.not_ge <|          le_of_dvd (pos_of_ne_zero hm_zero) <| dvd_trans (pow_dvd_pow _ h) (ordProj_dvd _ _)    split_ifs <;> simp_all [factorization_eq_zero_iff]  have hsub : (P.initial.a.map (·.factorization p)).sum ≤ (S.map (·.factorization p)).sum :=    Multiset.le_iff_exists_add.mp hle |>.elim fun k hk ↦ by simp [hk]  calc (P.initial.a.map (·.factorization p)).sum      _ ≤ (S.map (·.factorization p)).sum := hsub      _ ≤ (S.map fun m ↦ if p ∣ m then 1 else 0).sum :=          Multiset.sum_map_le_sum_map _ _ hval      _ = P.M * (Finset.filter (p ∣ ·) (.Ico (P.n - P.n / P.M) P.n)).card := by          simp only [S, map_join, sum_join, map_replicate, Multiset.sum_replicate, smul_eq_mul,            Multiset.Ico, card_filter, sum_eq_multiset_sum]