Exact resonance fibers of occupied Gram labels

The base is ((r,n₁),h,n₂',s'), and its fiber is (n₂,s,h'). Both maps retain the common first beta coordinate and signed frequencies. No diagonal restriction is imposed.

@[reducible, inline]

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

Equations

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

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceBase (L : WGramLabel) : WGramResonanceBase

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceBase L = (L.1, L.2.1.2.2, L.2.2.1, L.2.2.2.1)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceTriple (L : WGramLabel) : ℕ × ℕ × ℤ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceTriple L = (L.2.1.1, L.2.1.2.1, L.2.2.2.2)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceJoin (v : WGramResonanceBase) (t : ℕ × ℕ × ℤ) : WGramLabel

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceJoin v t = (v.1, (t.1, t.2.1, v.2.1), v.2.2.1, v.2.2.2, t.2.2)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceJoin_base_triple (L : WGramLabel) : wGramResonanceJoin (wGramResonanceBase L) (wGramResonanceTriple L) = L

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

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramZeroLabels K a V = {L ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramLabels V | MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramNumerator K a L = 0}

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceBases (G : Finset WGramLabel) : Finset WGramResonanceBase

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceBases G = Finset.image MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceBase G

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceFiber (G : Finset WGramLabel) (v : WGramResonanceBase) : Finset (ℕ × ℕ × ℤ)

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceFiber G v = Finset.image MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceTriple ({L ∈ G | MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceBase L = v})

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_wGramResonanceFiber {G : Finset WGramLabel} {v : WGramResonanceBase} {t : ℕ × ℕ × ℤ} : t ∈ wGramResonanceFiber G v ↔ wGramResonanceJoin v t ∈ G

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wGramResonanceFiber {A : Type u_1} [AddCommMonoid A] (G : Finset WGramLabel) (F : WGramLabel → A) : ∑ L ∈ G, F L = ∑ v ∈ wGramResonanceBases G, ∑ t ∈ wGramResonanceFiber G v, F (wGramResonanceJoin v t)

An exact finite reindexing, including every occupied base and triple.