theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_coefficient_support {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) : K.2 * (wCorrelationOuter t).2.1 ∈ Finset.Ioc 0 ⌊R⌋₊ ∧ K.1.2.2.1 * K.1.2.2.2.1 * (wCorrelationOuter t).1 ∈ Q ∧ K.1.1 * K.1.2.1 * (wCorrelationOuter t).2.2 ∈ N ∧ K.1.2.2.1 * K.1.2.2.2.2 / K.2 * t.1.1.2.2 ∈ Finset.Ioc 0 ⌊S⌋₊ ∧ K.1.1 * (wGCDTuple (wExtractedOriginal t.1)).n₂ ∈ N

All five coefficient arguments are the original support arguments.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_outer_n_le {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ T : ℝ} {b : ℕ} {K : WExtractedKey} {t : WExtractedTuple × ℤ} (ht : t ∈ wExtractedKeyFiber H N Q a P R S ξ b K) (hNT : ∀ n ∈ N, ↑n ≤ 2 * T) : 0 < (wCorrelationOuter t).2.2 ∧ ↑(wCorrelationOuter t).2.2 ≤ 2 * T

One original beta coordinate bounds the shared reduced n1; no second copy.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.direct_actual_weights (k j : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 0 < C ∧ ∀ (X : ℝ), 1 ≤ X → ∀ (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) (b : ℕ) (K : WExtractedKey) (β γ ζ : ℕ → ℝ), (∀ n ∈ N, 0 < n) → (∀ q ∈ Q, 0 < q) → (∀ n ∈ N, ↑n ≤ X) → (∀ q ∈ Q, ↑q ≤ X) → 0 ≤ R → 0 ≤ S → R ≤ X → S ≤ X → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ (n : ℕ), |γ n| ≤ ↑((fouvryTau j) n)) → (∀ (n : ℕ), |ζ n| ≤ ↑((fouvryTau j) n)) → ∀ t ∈ wExtractedKeyFiber H N Q a P R S ξ b K, |wCorrelationInnerWeight K (betaClean β a) ζ t| ≤ (C * X ^ δ) ^ 2 ∧ |wCorrelationOuterWeight K (betaClean β a) (factorConvolution γ (betaLowOmega ζ ξ)) γ (wCorrelationOuter t)| ≤ (C * X ^ δ) ^ 3

Uniform actual inner and outer weights; no support enlargement of beta.