Finite logarithmic lcm-weight bounds

These finite arithmetic estimates depend only on divisor moments and harmonic sums, not on smoothing, Poisson summation, or dispersion estimates.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LcmWeightBounds.sum_div_multiples_le_log {L : ℝ} (hL : 1 ≤ L) {d : ℕ} (hd : 0 < d) : (∑ r ∈ Finset.Ioc 0 ⌊L⌋₊, if d ∣ r then ↑d / ↑r else 0) ≤ 1 + Real.log L

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LcmWeightBounds.sum_gcd_div_le_tau_log {L : ℝ} (hL : 1 ≤ L) (Q : Finset ℕ) (hQ : Q ⊆ Finset.Ioc 0 ⌊L⌋₊) {q : ℕ} (hq : 0 < q) : ∑ r ∈ Q, ↑(q.gcd r) / ↑r ≤ ↑((LiLiuPrereqFouvry.fouvryTau 2) q) * (1 + Real.log L)

The gcd harmonic row sum is paid by tau_2(q), independently of any modulus coefficient or coprimality restriction.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LcmWeightBounds.one_div_lcm_eq_gcd_div {q r : ℕ} (hq : q ≠ 0) (hr : r ≠ 0) : 1 / ↑(q.lcm r) = ↑(q.gcd r) / (↑q * ↑r)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LcmWeightBounds.sum_one_div_lcm_le_tau_log {L : ℝ} (hL : 1 ≤ L) (Q : Finset ℕ) (hQ : Q ⊆ Finset.Ioc 0 ⌊L⌋₊) {q : ℕ} (hq : 0 < q) : ∑ r ∈ Q, 1 / ↑(q.lcm r) ≤ ↑((LiLiuPrereqFouvry.fouvryTau 2) q) / ↑q * (1 + Real.log L)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LcmWeightBounds.sum_abs_lcm_weight_le_log (j : ℕ) {L : ℝ} (hL : 1 ≤ L) (Q : Finset ℕ) (hQ : Q ⊆ Finset.Ioc 0 ⌊L⌋₊) (c : ℕ → ℝ) (hc : ∀ q ∈ Q, |c q| ≤ ↑((LiLiuPrereqFouvry.fouvryTau j) q)) : ∑ q ∈ Q, ∑ r ∈ Q, |c q * c r / ↑(q.lcm r)| ≤ (1 + Real.log L) ^ (2 * j ^ 2 + 1)

Fully evaluated double lcm sum for arbitrary signed fixed-order modulus weights. Even order zero is allowed.