Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuFouvryKLargeGCDOriginal

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.