theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RemainderMajorant_divCount {ι : Type u_1} (S : Finset ι) (a : ι → ℕ) (w : ι → ℝ) (L d : ℕ) (hd : 0 < d) (J : ℝ) (ha : ∀ x ∈ S, a x ≤ L) (hf : ∀ r ≤ L, (∑ x ∈ S, if a x = r then w x else 0) ≤ J) : (∑ x ∈ S, if d ∣ a x then w x else 0) ≤ J * ↑(L / d + 1)

Counting multiples by their value, not by injectivity of the source labels. The range starts at zero: zero values are retained.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.fouvryG9RemainderMajorant_multipleCount {N d : ℕ} (hd : 0 < d) (hdN : d ≤ N) : ↑(4 * N / d + 1) ≤ 5 * ↑N / ↑d

The elementary real estimate used for every d ≤ N.