Actual secondary labels, with only the common r varying

The base retains (n,n₂,s,h,n₂',s',h'). Reindexing is exact on occupied ordered labels; in particular neither beta index nor frequency is identified. The signed coefficient weight is independent of the fiber coordinate r.

@[reducible, inline]

abbrev MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGramSecondaryBase : Type

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGramSecondaryBase = (ℕ × (ℕ × ℕ × ℤ) × ℕ × ℕ × ℤ)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryBase (L : WGramLabel) : WGramSecondaryBase

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryBase L = (L.1.2, L.2)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryJoin (v : WGramSecondaryBase) (r : ℕ) : WGramLabel

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryJoin v r = ((r, v.1), v.2)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryJoin_base (L : WGramLabel) : wGramSecondaryJoin (wGramSecondaryBase L) L.1.1 = L

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryLabels (K : WExtractedKey) (a : ℤ) (V : Finset (WExtractedTuple × ℤ)) : Finset WGramLabel

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryLabels K a V = {L ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramLabels V | MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramNumerator K a L ≠ 0 ∧ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryResonant L}

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryBases (G : Finset WGramLabel) : Finset WGramSecondaryBase

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryBases G = Finset.image MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryBase G

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryFiber (G : Finset WGramLabel) (v : WGramSecondaryBase) : Finset ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryFiber G v = Finset.image (fun (L : MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGramLabel) => L.1.1) ({L ∈ G | MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryBase L = v})

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_wGramSecondaryFiber {G : Finset WGramLabel} {v : WGramSecondaryBase} {r : ℕ} : r ∈ wGramSecondaryFiber G v ↔ wGramSecondaryJoin v r ∈ G

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wGramSecondaryFiber {A : Type u_1} [AddCommMonoid A] (G : Finset WGramLabel) (F : WGramLabel → A) : ∑ L ∈ G, F L = ∑ v ∈ wGramSecondaryBases G, ∑ r ∈ wGramSecondaryFiber G v, F (wGramSecondaryJoin v r)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryJoin_weight (K : WExtractedKey) (β ζ : ℕ → ℝ) (v : WGramSecondaryBase) (r : ℕ) : wGramWeight K β ζ (wGramSecondaryJoin v r) = ζ (wKSectionDeltaPrime K * v.2.1.2.1) * β (K.1.1 * v.2.1.1) * (ζ (wKSectionDeltaPrime K * v.2.2.2.1) * β (K.1.1 * v.2.2.1))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wGramSecondaryFiber_weight (G : Finset WGramLabel) (K : WExtractedKey) (β ζ : ℕ → ℝ) (F : WGramLabel → ℝ) : ∑ L ∈ G, |wGramWeight K β ζ L| * F L = ∑ v ∈ wGramSecondaryBases G, |wGramWeight K β ζ (wGramSecondaryJoin v 0)| * ∑ r ∈ wGramSecondaryFiber G v, F (wGramSecondaryJoin v r)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramLabels_r_mem_dyadic {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {a : ℤ} {x η R S M Z : ℝ} {K : WExtractedKey} {b : ℕ} {j cap : Fin 5 → ℕ} {positive : Bool} {c : Finset (ℕ × ℕ)} {L : WGramLabel} (hL : L ∈ wGramLabels (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c)) : L.1.1 ∈ Finset.Ioc (2 ^ j 3 - 1) (2 ^ (j 3 + 1) - 1)

The interval follows from the actual dyadic block, not from an assumed support bound on arbitrary labels. Both endpoints are natural numbers.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryFiber_subset_dyadic {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {a : ℤ} {x η R S M Z : ℝ} {K : WExtractedKey} {b : ℕ} {j cap : Fin 5 → ℕ} {positive : Bool} {c : Finset (ℕ × ℕ)} (v : WGramSecondaryBase) : wGramSecondaryFiber (wGramSecondaryLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c)) v ⊆ Finset.Ioc (2 ^ j 3 - 1) (2 ^ (j 3 + 1) - 1)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryBases_data {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {a : ℤ} {x η R S M Z : ℝ} {K : WExtractedKey} {b : ℕ} {j cap : Fin 5 → ℕ} {positive : Bool} {c : Finset (ℕ × ℕ)} {v : WGramSecondaryBase} (hv : v ∈ wGramSecondaryBases (wGramSecondaryLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c))) : 0 < v.1 ∧ 0 < v.2.1.2.1 ∧ 0 < v.2.2.2.1 ∧ v.2.2.2.2 * ↑v.2.1.2.1 = v.2.1.2.2 * ↑v.2.2.2.1 ∧ iv3CorrelationNumerator K.1.2.1 v.1 v.2.1.1 v.2.2.1 v.2.1.2.1 v.2.2.2.1 a v.2.1.2.2 v.2.2.2.2 ≠ 0

Only occupied bases are tested. Positivity and the nonzero correlation numerator are recovered from a label witness, so empty fibers need no inputs.