Sparse modulus support and inverse-lcm mass

The canonical supported parts δ₁,δ₂ force a large square divisor in the corresponding modulus. A gcd harmonic row estimate and three fixed-order divisor bounds preserve this saving for signed inverse-lcm weights.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.deltaOne_mem_largeSquareDivisorSet (r N₁ N₂ : ℕ) {q T : ℕ} {Y : ℝ} (hq : q ∈ Finset.Ioc 0 T) (hY : 0 ≤ Y) (hlarge : Y < ↑(wGCDData q r N₁ N₂).δ₁) : q ∈ largeSquareDivisorSet T √Y

Large canonical δ₁ forces a large square divisor of the first modulus.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.deltaTwo_mem_largeSquareDivisorSet (q N₁ N₂ : ℕ) {r T : ℕ} {Y : ℝ} (hr : r ∈ Finset.Ioc 0 T) (hY : 0 ≤ Y) (hlarge : Y < ↑(wGCDData q r N₁ N₂).δ₂) : r ∈ largeSquareDivisorSet T √Y

Large canonical δ₂ forces a large square divisor of the second modulus.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_abs_lcm_weight_sparse_le {L Z A B : ℝ} (hL : 1 ≤ L) (hZ : 0 < Z) (hA : 0 ≤ A) (hB : 0 ≤ B) (Q S : Finset ℕ) (hQ : Q ⊆ Finset.Ioc 0 ⌊L⌋₊) (hSQ : S ⊆ Q) (hS : S ⊆ largeSquareDivisorSet ⌊L⌋₊ Z) (c : ℕ → ℝ) (hc : ∀ q ∈ Q, |c q| ≤ A) (hτ : ∀ q ∈ S, ↑((fouvryTau 2) q) ≤ B) : ∑ q ∈ S, ∑ r ∈ Q, |c q * c r / ↑(q.lcm r)| ≤ 2 * A ^ 2 * B * (1 + Real.log L) ^ 2 / Z

A deterministic sparse inverse-lcm estimate: two coefficient bounds and one divisor bound suffice. The support may be any subset of the sparse set.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_abs_lcm_weight_sparse_uniform (j : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (L x Z : ℝ), 1 ≤ L → L ≤ x → 0 < Z → ∀ (Q S : Finset ℕ), Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → S ⊆ Q → S ⊆ largeSquareDivisorSet ⌊L⌋₊ Z → ∀ (c : ℕ → ℝ), (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∑ q ∈ S, ∑ r ∈ Q, |c q * c r / ↑(q.lcm r)| ≤ C * x ^ ε * (1 + Real.log L) ^ 2 / Z

Constants depend only on the fixed divisor order and positive exponent, and precede all changing scales, supports, and signed coefficients.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_abs_lcm_weight_sparse_pairs_uniform (j : ℕ) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (L x Z : ℝ), 1 ≤ L → L ≤ x → 0 < Z → ∀ Q ⊆ Finset.Ioc 0 ⌊L⌋₊, ∀ (c : ℕ → ℝ), (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ F ⊆ Q ×ˢ Q, (∀ p ∈ F, p.1 ∈ largeSquareDivisorSet ⌊L⌋₊ Z ∨ p.2 ∈ largeSquareDivisorSet ⌊L⌋₊ Z) → ∑ p ∈ F, |c p.1 * c p.2 / ↑(p.1.lcm p.2)| ≤ C * x ^ ε * (1 + Real.log L) ^ 2 / Z

Either coordinate may carry the large square divisor. Arbitrary further pair restrictions are allowed; overlap of the two sparse strips costs at most a factor of two, and the original lcm denominator is unchanged.