Actual phase scales and nonempty-key guards

The source slow phase is estimated using the original beta coordinate N₁ = d*d₁*n₁, not the reduced coordinate n₁. In particular |a| <= 4*M*T and N₁ >= T give |a|/N₁ <= 4*M, uniformly in a.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WExtractedKey.D (K : WExtractedKey) : ℕ

Equations

• K.D = K.1.2.2.1 * K.1.2.2.2.1 * K.1.2.2.2.2

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WExtractedKey.D' (K : WExtractedKey) : ℕ

Equations

• K.D' = K.1.1 * K.1.2.1 * K.D

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyFiber_moduli {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {t : WExtractedTuple × ℤ} (ht : t ∈ wExtractedKeyFiber H N Q a P R S ξ b K) : (wGCDTuple (wExtractedOriginal t.1)).D = K.D ∧ (wGCDTuple (wExtractedOriginal t.1)).D' = K.D'

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyFiber_positive {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {t : WExtractedTuple × ℤ} (ht : t ∈ wExtractedKeyFiber H N Q a P R S ξ b K) : 0 < K.D ∧ 0 < K.D' ∧ 0 < K.2 ∧ 0 < t.1.1.1.2 ∧ 0 < (wGCDTuple (wExtractedOriginal t.1)).k₁ ∧ 0 < (wGCDTuple (wExtractedOriginal t.1)).n₁ ∧ 0 < t.1.1.2.1 ∧ 0 < t.1.1.2.2 ∧ t.2 ≠ 0

Positivity follows from a real member; no positivity is inferred from membership of the enclosing key box.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyExponential_eq_fixedWeight {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) (H : ℕ → ℕ → ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) (b : ℕ) (K : WExtractedKey) (u : ℝ) : wExtractedKeyExponential H N Q β c₁ γ ζ a P R S ξ b K u = ∑ t ∈ wExtractedKeyFiber H N Q a P R S ξ b K, have v := wGCDTuple (wExtractedOriginal t.1); ↑(wExtractedCoefficient β c₁ γ ζ t.1) * wExtractedArithmeticPhase a t.2 t.1 * wAnalyticWeight K.D K.D' a u ↑t.2 ↑v.k₁ ↑v.n₁ ↑t.1.1.2.1 ↑t.1.1.2.2

The constants of the analytic weight are genuinely fixed on a key.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.slow_denominator {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) : v.n₁ * v.k₁ * v.k₂ * v.D' = N₁ * q.lcm r

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalytic_phase_budget {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) {M T x u : ℝ} (hM : 0 ≤ M) (hT : 0 < T) (hNT : T ≤ ↑N₁) (hx : x = 4 * M * T) {a : ℤ} (ha : |↑a| ≤ x) (hu : |u| ≤ 3 * M) (h : ℤ) : |↑h| * (|u| / ↑(v.D * v.k₁ * v.k₂) + |↑a| / ↑(v.n₁ * v.k₁ * v.k₂ * v.D')) ≤ 7 * M * |↑h| / ↑(q.lcm r)

A scale bound for the two smooth phase monomials, retaining the original beta support and the uniform large-residue range.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wUniformCutoff_phase_scale_le {M Z : ℝ} (hM : 0 < M) (hZ : 0 ≤ Z) {q r : ℕ} (hq : q ≠ 0) (hr : r ≠ 0) {h : ℤ} (hh : h.natAbs ≤ wUniformCutoff M Z q r) : M * |↑h| / ↑(q.lcm r) ≤ Z + M / ↑(q.lcm r)

The actual ceiling cutoff only supplies Z + M/lcm. This explicitly records the boundary-frequency issue before any small-power variation claim.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalytic_reference_budget {D D' h k n r s H K N R S : ℝ} (hD : 0 < D) (hD' : 0 < D') (hk : 0 < k) (hn : 0 < n) (hr : 0 < r) (hs : 0 < s) (hK : 0 < K) (hN : 0 < N) (hR : 0 < R) (hS : 0 < S) (hH : 0 ≤ H) (hHh : H ≤ |h|) (hkK : k ≤ 2 * K) (hnN : n ≤ 2 * N) (hrR : r ≤ 2 * R) (hsS : s ≤ 2 * S) (u a : ℝ) : H * (|u| / (D * K * R * S) + |a| / (N * K * R * S * D')) ≤ 16 * (|h| * (|u| / (D * k * r * s) + |a| / (n * k * r * s * D')))

Positive dyadic reference scales enlarge the phase budget by at most sixteen. The estimate is for the complete rectangle, not just its masked arithmetic points.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticWeight_normalize (D D' : ℕ) (a : ℤ) (u H K N R S : ℝ) (v : Fin 5 → ℝ) : wAnalyticWeight D D' a u (H * v 0) (K * v 1) (N * v 2) (R * v 3) (S * v 4) = (↑↑D * ↑K * ↑R * ↑S)⁻¹ * ↑(v 1 * v 3 * v 4)⁻¹ * ↑(Real.fourierChar (-H * u / (↑D * K * R * S) * v 0 / (v 1 * v 3 * v 4) + H * ↑a / (N * K * R * S * ↑D') * v 0 / (v 1 * v 2 * v 3 * v 4)))

Exact normalization of the concrete five-variable weight. The two real parameters displayed here are the ones controlled by the reference budget; no arithmetic coefficient is part of this function.