Main nonzero occupied labels, with the common index and r varying

Only the two ordered inner triples are fixed. The original beta/zeta weight is independent of both averaged coordinates; the shared k multiplicity remains in the already constructed Gram section.

@[reducible, inline]

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

Equations

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

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainJoin (v : WGramMainBase) (p : ℕ × ℕ) : WGramLabel

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainJoin v p = ((p.2, p.1), v)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainJoin_base (L : WGramLabel) : wGramMainJoin L.2 (L.1.2, L.1.1) = L

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

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainLabels 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.wGramMainBases (G : Finset WGramLabel) : Finset WGramMainBase

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainBases G = Finset.image Prod.snd G

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainFiber (G : Finset WGramLabel) (v : WGramMainBase) : Finset (ℕ × ℕ)

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainFiber G v = Finset.image (fun (L : MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGramLabel) => (L.1.2, L.1.1)) ({L ∈ G | L.2 = v})

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_wGramMainFiber {G : Finset WGramLabel} {v : WGramMainBase} {p : ℕ × ℕ} : p ∈ wGramMainFiber G v ↔ wGramMainJoin v p ∈ G

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wGramMainFiber {A : Type u_1} [AddCommMonoid A] (G : Finset WGramLabel) (F : WGramLabel → A) : ∑ L ∈ G, F L = ∑ v ∈ wGramMainBases G, ∑ p ∈ wGramMainFiber G v, F (wGramMainJoin v p)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainJoin_weight (K : WExtractedKey) (β ζ : ℕ → ℝ) (v : WGramMainBase) (p : ℕ × ℕ) : wGramWeight K β ζ (wGramMainJoin v p) = ζ (wKSectionDeltaPrime K * v.1.2.1) * β (K.1.1 * v.1.1) * (ζ (wKSectionDeltaPrime K * v.2.2.1) * β (K.1.1 * v.2.1))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wGramMainFiber_weight (G : Finset WGramLabel) (K : WExtractedKey) (β ζ : ℕ → ℝ) (F : WGramLabel → ℝ) : ∑ L ∈ G, |wGramWeight K β ζ L| * F L = ∑ v ∈ wGramMainBases G, |wGramWeight K β ζ (wGramMainJoin v (0, 0))| * ∑ p ∈ wGramMainFiber G v, F (wGramMainJoin v p)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramLabels_n_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.2 ∈ Finset.Ioc (2 ^ j 2 - 1) (2 ^ (j 2 + 1) - 1)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainBox (K : WExtractedKey) (a : ℤ) (j : Fin 5 → ℕ) (v : WGramMainBase) : Finset (ℕ × ℕ)

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainBox K a j v = {n ∈ Finset.Ioc (2 ^ j 2 - 1) (2 ^ (j 2 + 1) - 1) | MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3CorrelationNumerator K.1.2.1 n v.1.1 v.2.1 v.1.2.1 v.2.2.1 a v.1.2.2 v.2.2.2 ≠ 0} ×ˢ Finset.Ioc (2 ^ j 3 - 1) (2 ^ (j 3 + 1) - 1)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainFiber_subset_box {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 : WGramMainBase) : wGramMainFiber (wGramMainLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c)) v ⊆ wGramMainBox K a j v

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainBases_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 : WGramMainBase} (hv : v ∈ wGramMainBases (wGramMainLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c))) : 0 < v.1.1 ∧ 0 < v.2.1 ∧ 0 < v.1.2.1 ∧ 0 < v.2.2.1 ∧ v.2.2.2 * ↑v.1.2.1 ≠ v.1.2.2 * ↑v.2.2.1

The nonzero constant term and positive coordinates required by the mean are consequences of an occupied canonical Gram witness.