structure MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.PrimeC2Interval : Type

Geometry only: no analytic assertion is stored in the interval index.

• scale : ℝ
• lower : ℝ
• upper : ℝ
• one_le_scale : 1 ≤ self.scale
• scale_le_lower : self.scale ≤ self.lower
• lower_le_upper : self.lower ≤ self.upper
• upper_le_twice : self.upper ≤ 2 * self.scale

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeC2Interval_support (z : PrimeC2Interval) (n : ℕ) : n ∈ primeSWInterval z.lower z.upper → z.scale ≤ ↑n ∧ ↑n ≤ 2 * z.scale

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta_le_order_one (n : ℕ) : |primeSWBeta n| ≤ ↑((fouvryTau 1) n)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeC2_unconditional (i j A : ℕ) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (z : PrimeC2Interval) (M ν : ℝ), 1 ≤ M → 4 * M * z.scale = x → ε ≤ ν → ν ≤ 1 / 10 → z.scale = x ^ ν → ∀ (U : Finset ℕ), (∀ n ∈ U, M ≤ ↑n ∧ ↑n ≤ 2 * M) → ∀ (α c : ℕ → ℝ), (∀ n ∈ U, |α n| ≤ ↑((fouvryTau i) n)) → SignedWellFactorable j (x ^ ((5 - 5 * ν) / 9 - ε)) c → ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ x → |signedError U (primeSWInterval z.lower z.upper) (Finset.Ioc 0 ⌊x ^ ((5 - 5 * ν) / 9 - ε)⌋₊) α primeSWBeta c a| ≤ x / Real.log x ^ A

No SW premise: the actual prime-interval producer is consumed here.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeSWBeta_clean_nat (N n : ℕ) : betaClean primeSWBeta (↑N) n = if n.Coprime N then primeSWBeta n else 0

For primes, divisor deletion is exactly the actual Goldbach coprime mask.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeC2_clean_family {ε : ℝ} (hε : 0 < ε) : BetaCoprimeSWFamily 3 (fun (z : BetaCleanIndex PrimeC2Interval.scale ε) => z.index.scale) (fun (z : BetaCleanIndex PrimeC2Interval.scale ε) => primeSWInterval z.index.lower z.index.upper) fun (z : BetaCleanIndex PrimeC2Interval.scale ε) => betaClean primeSWBeta z.residue

The independent sieve order increases, while all changing residues stay after the constants.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.primeC2_clean_unconditional (i j A : ℕ) {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 < δ) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (z : BetaCleanIndex PrimeC2Interval.scale δ) (M ν : ℝ), 1 ≤ M → 4 * M * z.index.scale = x → ε ≤ ν → ν ≤ 1 / 10 → z.index.scale = x ^ ν → ∀ (U : Finset ℕ), (∀ n ∈ U, M ≤ ↑n ∧ ↑n ≤ 2 * M) → ∀ (α c : ℕ → ℝ), (∀ n ∈ U, |α n| ≤ ↑((fouvryTau i) n)) → SignedWellFactorable j (x ^ ((5 - 5 * ν) / 9 - ε)) c → ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ x → |signedError U (primeSWInterval z.index.lower z.index.upper) (Finset.Ioc 0 ⌊x ^ ((5 - 5 * ν) / 9 - ε)⌋₊) α (betaClean primeSWBeta z.residue) c a| ≤ x / Real.log x ^ A

Concrete cleaned prime intervals feed C.2 without an analytic premise.