The nonzero secondary resonance with a common first beta index

The relation h'*s = h*s' does not force the correlation numerator to vanish. In this branch its common n*s' factor is extracted before averaging in r, never by applying a nonzero-coefficient mean in n.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3SecondaryNumerator (d₁ n₂ n₂' : ℕ) (a h : ℤ) : ℤ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3SecondaryNumerator d₁ n₂ n₂' a h = a * ↑d₁ * h * (↑n₂' - ↑n₂)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3CorrelationNumerator_secondary {d₁ n n₂ n₂' s s' : ℕ} {a h h' : ℤ} (hsec : h' * ↑s = h * ↑s') : iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h' = ↑(n * s') * iv3SecondaryNumerator d₁ n₂ n₂' a h

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3SecondaryNumerator_ne_zero {d₁ n n₂ n₂' s s' : ℕ} {a h h' : ℤ} (hsec : h' * ↑s = h * ↑s') (hl : iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h' ≠ 0) : iv3SecondaryNumerator d₁ n₂ n₂' a h ≠ 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_secondary_gcd {d₁ n n₂ n₂' r s s' : ℕ} {a h h' : ℤ} (hsec : h' * ↑s = h * ↑s') : (n * r * s * s').gcd (iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h').natAbs = n * s' * (r * s).gcd (iv3SecondaryNumerator d₁ n₂ n₂' a h).natAbs

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_secondary_gcd_sum {d₁ n n₂ n₂' s s' : ℕ} {a h h' : ℤ} (hs : 0 < s) (hsec : h' * ↑s = h * ↑s') (hl : iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h' ≠ 0) (B : ℕ) : ∑ r ∈ Finset.Ioc 0 B, (n * r * s * s').gcd (iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h').natAbs ≤ n * s' * (B * s * (iv3SecondaryNumerator d₁ n₂ n₂' a h).natAbs.divisors.card)

A mean over a progression of multiples follows from the already proved finite gcd mean by injective inclusion, with its step cost explicit.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_secondary_sqrt_gcd_sum {d₁ n n₂ n₂' s s' : ℕ} {a h h' : ℤ} (hs : 0 < s) (hsec : h' * ↑s = h * ↑s') (hl : iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h' ≠ 0) (B : ℕ) : ∑ r ∈ Finset.Ioc 0 B, √↑((n * r * s * s').gcd (iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h').natAbs) ≤ ↑B * √↑(n * s' * s * (iv3SecondaryNumerator d₁ n₂ n₂' a h).natAbs.divisors.card)

Square-root gcd mean in the secondary branch. It is uniform in the common n, including the case where the coefficient for an n-mean is zero.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryResonant (L : WGramLabel) : Prop

The secondary branch is not excluded by the nonzero numerator filter.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryResonant L = (L.2.2.2.2 * ↑L.2.1.2.1 = L.2.1.2.2 * ↑L.2.2.2.1)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wGram_nonzero_split_secondary (G : Finset WGramLabel) (K : WExtractedKey) (a : ℤ) (F : WGramLabel → ℝ) : ∑ L ∈ G with wGramNumerator K a L ≠ 0, F L = ∑ L ∈ G with wGramNumerator K a L ≠ 0 ∧ wGramSecondaryResonant L, F L + ∑ L ∈ G with wGramNumerator K a L ≠ 0 ∧ ¬wGramSecondaryResonant L, F L

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramFouvryCost_secondary_sum {ε C : ℝ} (hε : 0 ≤ ε) (hC : 0 ≤ C) (a : ℤ) (R S M Z : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) {n n₂ n₂' s s' : ℕ} {h h' : ℤ} (hn : 0 < n) (hs : 0 < s) (hs' : 0 < s') (hsec : h' * ↑s = h * ↑s') (hl : iv3CorrelationNumerator K.1.2.1 n n₂ n₂' s s' a h h' ≠ 0) (lo hi : ℕ) : ∑ r ∈ Finset.Ioc lo hi, wGramFouvryCost ε C a R S M Z K j cap ((r, n), (n₂, s, h), n₂', s', h') ≤ C * ↑a.natAbs.divisors.card * (↑K.D' + ↑(wKSectionGridUpper R S K j cap + 1) / ↑(n * (lo + 1) * s * s')) * ↑(n * hi * s * s') ^ (1 / 2 + ε) * (↑hi * √↑(n * s' * s * (iv3SecondaryNumerator K.1.2.1 n₂ n₂' a h).natAbs.divisors.card))

A quantitative r-mean of the actual Fouvry cost on the secondary branch. Both local endpoints are retained in the modulus bounds. This does not assume the signed linear coefficient for an n-mean is nonzero.