Reciprocal mass of the large-square-divisor support

Exact finite reindexing of multiples, followed by the inverse-square tail, retains the square-root saving in harmonic rather than counting measure.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_one_div_multiples_le_log {L : ℝ} (hL : 1 ≤ L) {d : ℕ} (hd : 0 < d) : ∑ n ∈ Finset.Ioc 0 ⌊L⌋₊ with d ∣ n, 1 / ↑n ≤ (1 + Real.log L) / ↑d

The harmonic mass of the positive multiples of d up to a real endpoint.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_one_div_largeSquareDivisorSet_le {L Z : ℝ} (hL : 1 ≤ L) (hZ : 0 < Z) : ∑ n ∈ largeSquareDivisorSet ⌊L⌋₊ Z, 1 / ↑n ≤ 2 / Z * (1 + Real.log L)

Uniform harmonic saving for large square divisors, with constant 2.