Logarithmic lcm-weight sum and the very-large-gcd zero mode

The symmetric inequality 2 |c_q c_r| ≤ c_q² + c_r² pays the two modulus weights by a single divisor moment. No submultiplicativity of tau_j at noncoprime arguments, and no arithmetic-progression input, is assumed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.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 ≤ ↑((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.LiLiuPrereqFouvry.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) ≤ ↑((fouvryTau 2) q) / ↑q * (1 + Real.log L)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.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| ≤ ↑((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.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWULargeDelta_abs_le_highDelta {k : ℕ} (hk : 1 ≤ k) (j : ℕ) {T L : ℝ} (hT : 1 ≤ T) (hL : 1 ≤ L) (M : ℝ) (N Q : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 ⌊T⌋₊) (hQ : Q ⊆ Finset.Ioc 0 ⌊L⌋₊) (β c : ℕ → ℝ) (hβ : ∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) (hc : ∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) (a : ℤ) : |smoothWULargeDelta M T N Q β c a| ≤ |M * dyadicCutoffMass| * T * (1 + Real.log T) ^ (k ^ 2 - 1) * (1 + Real.log L) ^ (2 * j ^ 2 + 1)

The actual very-large-gcd remainder, uniformly for every integer residue and signed beta/modulus weights. This is the endpoint δ > T, not δ > log^B.