Counting a saved prime factor in the total rough logarithmic mass

theorem NairTenenbaum.rough_logMass_le_saved_factors {ι : Type u_1} (S H : Finset ι) (hH : H ⊆ S) (b : ι → ℕ) (hb : ∀ i ∈ S, b i ≠ 0) {k : ℕ} (hk : 2 ≤ k) {P : ℝ} (hP : 1 ≤ P) (hprimes : ∀ i ∈ S, ∀ p ∈ (b i).primeFactors, ↑p ≤ P) (hΩ : ∀ i ∈ S, bigOmega (b i) ≤ k - 1) (hΩH : ∀ i ∈ H, bigOmega (b i) ≤ k - 2) : ∑ i ∈ S, Real.log ↑(b i) ≤ ((↑k - 1) * ↑S.card - ↑H.card) * Real.log P