Lemma 7 on the actual extracted arithmetic carrier

Fouvry (1987), pp. 628--629, III.7. The pair is (n₂,n₁*s'). Its positivity, coprimality and growing prime-factor bounds are derived from the original retained masks. The partition acts on tuples, not on their possibly repeated pair images, so no beta-index multiplicity is lost.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimePair (z : WExtractedTuple) : ℕ × ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimePair z = ((MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuple (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal z)).n₂, (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuple (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal z)).n₁ * z.1.2.2)

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimePairBound (N : Finset ℕ) (S : ℝ) : ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimePairBound N S = max 2 (max (N.sup id) (N.sup id * ⌊S⌋₊))

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeOrder (x : ℝ) : ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeOrder x = ⌊2 * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmegaCutoff x⌋₊

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimePair_admissible {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {x η R S : ℝ} {z : WExtractedTuple} (hz : z ∈ wFactorExtractionTuples N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x)) : wCoprimePair z ∈ LiLiuPrereqFouvry.CoprimePartition.admissiblePairs (wCoprimePairBound N S) (wCoprimeOrder x)

Every retained tuple, including one with zero coefficient, is in the precise domain of Lemma 7. No roughness or SW assumption is needed here.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeLabel (x : ℝ) (N : Finset ℕ) (S : ℝ) (t : WExtractedTuple × ℤ) : Finset (ℕ × ℕ)

The exact label depends only on the pair, not on k₁, r' or the frequency. This is the independence used when forming Cauchy pairs.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeLabel x N S t = LiLiuPrereqFouvry.CoprimePartition.cell (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimePairBound N S) (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeOrder x) (LiLiuPrereqFouvry.CoprimePartition.matrixColor (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimePairBound N S) (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeOrder x) (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimePair t.1))

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeFiber (x : ℝ) (N : Finset ℕ) (S : ℝ) (U : Finset (WExtractedTuple × ℤ)) (c : Finset (ℕ × ℕ)) : Finset (WExtractedTuple × ℤ)

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeFiber x N S U c = {t ∈ U | MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeLabel x N S t = c}

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeLabel_eq_of_pair_eq (x : ℝ) (N : Finset ℕ) (S : ℝ) {t u : WExtractedTuple × ℤ} (h : wCoprimePair t.1 = wCoprimePair u.1) : wCoprimeLabel x N S t = wCoprimeLabel x N S u

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeLabel_mem_partition {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {x η R S : ℝ} {b : ℕ} {K : WExtractedKey} {t : WExtractedTuple × ℤ} (ht : t ∈ wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) : wCoprimeLabel x N S t ∈ LiLiuPrereqFouvry.CoprimePartition.partition (wCoprimePairBound N S) (wCoprimeOrder x) ∧ wCoprimePair t.1 ∈ wCoprimeLabel x N S t

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeFiber_cross_coprime {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {x η R S : ℝ} {b : ℕ} {K : WExtractedKey} {U : Finset (WExtractedTuple × ℤ)} (hU : U ⊆ wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) {c : Finset (ℕ × ℕ)} {t u : WExtractedTuple × ℤ} (ht : t ∈ wCoprimeFiber x N S U c) (hu : u ∈ wCoprimeFiber x N S U c) : (wCoprimePair t.1).1.Coprime (wCoprimePair u.1).2 ∧ (wCoprimePair u.1).1.Coprime (wCoprimePair t.1).2

Cross-coprimality now holds for two distinct actual tuples in a cell, not just for two abstract admissible pairs.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wCoprimeFibers {A : Type u_1} [AddCommMonoid A] (x : ℝ) (N : Finset ℕ) (S : ℝ) (U : Finset (WExtractedTuple × ℤ)) (F : WExtractedTuple × ℤ → A) : ∑ t ∈ U, F t = ∑ c ∈ Finset.image (wCoprimeLabel x N S) U, ∑ t ∈ wCoprimeFiber x N S U c, F t

This identity keeps all tuple multiplicities and all signed weights. There is no absolute value inside a cell.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeLabel_image_card_le {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {x η R S : ℝ} {b : ℕ} {K : WExtractedKey} {U : Finset (WExtractedTuple × ℤ)} (hU : U ⊆ wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) : (Finset.image (wCoprimeLabel x N S) U).card ≤ (LiLiuPrereqFouvry.CoprimePartition.partition (wCoprimePairBound N S) (wCoprimeOrder x)).card

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.eventually_wCoprimeLabel_image_card_le {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (a : ℤ) (η R S : ℝ) (b : ℕ) (K : WExtractedKey) (U : Finset (WExtractedTuple × ℤ)), (∀ n ∈ N, 0 < n) → (∀ q ∈ Q, 0 < q) → ↑(wCoprimePairBound N S) ≤ x → U ⊆ wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K → ↑(Finset.image (wCoprimeLabel x N S) U).card ≤ x ^ ε

The original 2*(log x)^(1/5) product-variable order has subpolynomial cost. The threshold precedes every finite carrier and every varying residue.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimePairBound_c2_le {x ν ε : ℝ} (hx : 4 ≤ x) (hε : 0 ≤ ε) (hεν : ε ≤ ν) (hν : ν ≤ 1 / 10) {N : Finset ℕ} (hN : ∀ n ∈ N, ↑n ≤ 2 * x ^ ν) : ↑(wCoprimePairBound N (x ^ c2SExponent ν ε)) ≤ x

The actual C.2 levels satisfy the pair cutoff required above, including the near-endpoint branch S = 1. Thus the cutoff is not a new analytic input.