The genuine full-level modulus carrier

Only the complete positive interval is used here. No arbitrary membership mask is absorbed into a well-factorable coefficient. The inner factor has an exact floor interval and explicitly retained arithmetic restrictions; the filtered fiber is not asserted to be an unweighted interval.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_reducedModuli_fullLevel_iff (L : ℝ) (a : ℤ) (q : ℕ) : q ∈ reducedModuli (Finset.Ioc 0 ⌊L⌋₊) a ↔ q ∈ Finset.Ioc 0 ⌊L⌋₊ ∧ a.natAbs.Coprime q

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_reducedModuli_fullLevel_mul_iff (L : ℝ) (a : ℤ) {d k : ℕ} (hd : 0 < d) : d * k ∈ reducedModuli (Finset.Ioc 0 ⌊L⌋₊) a ↔ k ∈ Finset.Ioc 0 (⌊L⌋₊ / d) ∧ a.natAbs.Coprime d ∧ a.natAbs.Coprime k

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.supported_product_mem_fullLevel {R S : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) {r s : ℕ} (hr : r ∈ Finset.Ioc 0 ⌊R⌋₊) (hs : s ∈ Finset.Ioc 0 ⌊S⌋₊) : r * s ∈ Finset.Ioc 0 ⌊R * S⌋₊

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.supported_product_reduced_fullLevel_iff {R S : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) {r s : ℕ} (hr : r ∈ Finset.Ioc 0 ⌊R⌋₊) (hs : s ∈ Finset.Ioc 0 ⌊S⌋₊) (a : ℤ) : r * s ∈ reducedModuli (Finset.Ioc 0 ⌊R * S⌋₊) a ↔ a.natAbs.Coprime r ∧ a.natAbs.Coprime s

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.positive_factor_box_iff {d k F : ℕ} (hd : 0 < d) (hk : 0 < k) : d ∈ Finset.Ioc 0 F ∧ k ∈ Finset.Ioc 0 F ∧ d * k ≤ F ↔ k ∈ Finset.Ioc 0 (F / d)

The real interval for a positive varying factor. Both coordinate caps in the broad extraction box are consequences of the product cap.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wRPrimeResidual (a : ℤ) (P : WOriginalTuple → Prop) (Δ Δ' s' q₁ n₁ n₂ r' : ℕ) : Prop

Residual restrictions on r' after the full modulus interval has been resolved. They are not dropped when applying partial summation or Cauchy.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wRPrimeResidual a P Δ Δ' s' q₁ n₁ n₂ r' = (a.natAbs.Coprime r' ∧ n₂.Coprime r' ∧ n₁ ≡ n₂ [MOD q₁.gcd (Δ * r' * (Δ' * s'))] ∧ P ((q₁, Δ * r' * (Δ' * s')), n₁, n₂) ∧ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSecondExtractionDivisor ((q₁, Δ * r' * (Δ' * s')), n₁, n₂) = Δ * Δ')

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_wFactorExtractionTuples_fullLevel_rPrime_iff {R S : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) (N : Finset ℕ) (a : ℤ) (P : WOriginalTuple → Prop) (ξ : ℝ) {Δ Δ' r' s' : ℕ} (hΔ : 0 < Δ) (hΔ' : 0 < Δ') (hr' : 0 < r') (hs' : 0 < s') (q₁ n₁ n₂ : ℕ) : (((Δ, Δ'), r', s'), q₁, n₁, n₂) ∈ wFactorExtractionTuples N (Finset.Ioc 0 ⌊R * S⌋₊) a P R S ξ ↔ r' ∈ Finset.Ioc 0 (⌊R⌋₊ / Δ) ∧ s' ∈ Finset.Ioc 0 (⌊S⌋₊ / Δ') ∧ q₁ ∈ Finset.Ioc 0 ⌊R * S⌋₊ ∧ a.natAbs.Coprime q₁ ∧ n₁ ∈ N ∧ n₂ ∈ N ∧ a.natAbs.Coprime Δ ∧ a.natAbs.Coprime Δ' ∧ a.natAbs.Coprime s' ∧ n₁.Coprime q₁ ∧ n₂.Coprime Δ ∧ n₂.Coprime Δ' ∧ n₂.Coprime s' ∧ ↑(Δ' * s').primeFactors.card ≤ ξ ∧ s'.Coprime Δ ∧ wRPrimeResidual a P Δ Δ' s' q₁ n₁ n₂ r'

Exact inner-variable conditions in the actual extracted W. The only range of r' is 0 < r' <= floor(R)/Delta; all remaining variable-dependent restrictions are displayed in wRPrimeResidual. No assertion of interval cancellation is made for this filtered set.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wUniformCutoff_frequency_iff {M Z : ℝ} (q r : ℕ) {h : ℤ} (hh : h ≠ 0) : h.natAbs ≤ wUniformCutoff M Z q r ↔ ↑(h.natAbs - 1) < ↑(q.lcm r) / M * Z

A nonzero retained frequency gives a strict lower endpoint. This uses the ceiling convention in the actual wUniformCutoff, including |h| = 1, for which the lower endpoint is zero.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wUniformCutoff_factor_interval_iff {M Z : ℝ} (hM : 0 < M) (hZ : 0 < Z) {q d k δ : ℕ} (hq : 0 < q) (hd : 0 < d) (hk : 0 < k) (hg : q.gcd (d * k) = δ) {h : ℤ} (hh : h ≠ 0) : h.natAbs ≤ wUniformCutoff M Z q (d * k) ↔ ⌊↑(h.natAbs - 1) * M * ↑δ / (↑q * ↑d * Z)⌋₊ < k

On a fixed gcd fiber the original modulus-dependent cutoff is an honest lower floor endpoint for the varying factor k. This is not an enlargement to a common cutoff.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wUniformCutoff_factor_mem_Ioc_iff {M Z : ℝ} (hM : 0 < M) (hZ : 0 < Z) {q d k δ F : ℕ} (hq : 0 < q) (hd : 0 < d) (hk : 0 < k) (hg : q.gcd (d * k) = δ) {h : ℤ} (hh : h ≠ 0) : k ≤ F ∧ h.natAbs ≤ wUniformCutoff M Z q (d * k) ↔ k ∈ Finset.Ioc ⌊↑(h.natAbs - 1) * M * ↑δ / (↑q * ↑d * Z)⌋₊ F

The exact retained inner interval after fixing the gcd. The upper endpoint comes from the factor support, not an arbitrary modulus mask.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal_reducedModuli {N Q : Finset ℕ} {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {z : WExtractedTuple} (hz : z ∈ wFactorExtractionTuples N Q a P R S ξ) : (wExtractedOriginal z).1.1 ∈ reducedModuli Q a ∧ (wExtractedOriginal z).1.2 ∈ reducedModuli Q a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wUniformCutoff_le_fullLevel {M Z L : ℝ} (hM : 0 < M) (hZ : 0 ≤ Z) (hL : 0 ≤ L) {q r : ℕ} (hq : q ∈ Finset.Ioc 0 ⌊L⌋₊) (hr : r ∈ Finset.Ioc 0 ⌊L⌋₊) : wUniformCutoff M Z q r ≤ ⌈L ^ 2 / M * Z⌉₊

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedMaxFrequency_le_fullLevel {M Z L : ℝ} (hM : 0 < M) (hZ : 0 ≤ Z) (hL : 0 ≤ L) (N : Finset ℕ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) : wExtractedMaxFrequency (wUniformCutoff M Z) N (Finset.Ioc 0 ⌊L⌋₊) a P R S ξ ≤ ⌈L ^ 2 / M * Z⌉₊

A scale-only dyadic count bound, uniform in the residue, the coefficients, and every surviving arithmetic mask.