theorem
MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_largeGCD_kscale
{k : ℕ}
(hk : 1 ≤ k)
(j : ℕ)
{ε Cscale : ℝ}
(hε : 0 < ε)
(hCscale : 1 ≤ Cscale)
:
∃ (C : ℝ),
0 < C ∧ ∀ (M T Y x : ℝ),
1 ≤ M →
1 ≤ T →
0 < Y →
1 ≤ x →
M * T ≤ x →
∀ (N Q : Finset ℕ),
N ⊆ Finset.Ioc 0 ⌊T⌋₊ →
∀ (β c : ℕ → ℝ),
(∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) →
(∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) →
∀ (a : ℤ),
|↑a| ≤ Cscale * x →
(∀ n ∈ N, β n ≠ 0 → ¬↑n ∣ a) →
∀ (P : WOriginalTuple → Prop),
(∀ t ∈ wOriginalTuples N Q a, P t → Y < ↑(t.2.1.gcd t.2.2)) →
|wMaskedOriginal M N Q β c a P| ≤ C * M * x ^ ε * (T ^ 2 * (1 + Real.log T) ^ (k ^ 2 - 1) * √((1 + Real.log T) / Y))
The fixed shift enlargement changes only the constant in the original large-gcd estimate. The pair carrier and its cutoff remain unchanged.
Inspect dependencies
MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedOriginal_abs_le_largeGCD_kscale · compiled type and proof/definition references.