Finite counting of the genuine zero-numerator branch

Fouvry (1987), pp. 631--632, (4.8)--(4.9). The first beta index n is common to both phases. Frequencies remain integers: no positivity or same-tuple restriction is imposed on the variable frequency.

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

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_resonance_n₂_dvd {d₁ n n₂ n₂' s s' : ℕ} {a h h' : ℤ} (ha : a ≠ 0) (hc : (d₁ * n).Coprime n₂) (hl : iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h' = 0) : n₂ ∣ (h * ↑n₂' * ↑s').natAbs

Primitivity makes the variable second beta coordinate a divisor of the fixed signed product, rather than of a product involving itself.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_resonance_s_dvd {d₁ n n₂ n₂' s s' : ℕ} {a h h' : ℤ} (ha : a ≠ 0) (hl : iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h' = 0) : s ∣ (h * ↑n₂' * ↑s' * (↑d₁ * ↑n - ↑n₂)).natAbs

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_resonance_frequency_unique {d₁ n n₂ n₂' s s' : ℕ} {a h h₁ h₂ : ℤ} (ha : a ≠ 0) (hn₂ : 0 < n₂) (hs : 0 < s) (hδ : ↑d₁ * ↑n - ↑n₂' ≠ 0) (h₁l : iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h₁ = 0) (h₂l : iv3CorrelationNumerator d₁ n n₂ n₂' s s' a h h₂ = 0) : h₁ = h₂

The signed frequency is unique once the two natural coordinates are fixed. Both signs are covered by cancellation in the integers.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3ResonanceDivisorPairs (d₁ n : ℕ) (P : ℤ) : Finset ((_ : ℕ) × ℕ)

The two finite divisor choices which encode every resonant triple.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3ResonanceDivisorPairs d₁ n P = P.natAbs.divisors.sigma fun (n₂ : ℕ) => (P * (↑d₁ * ↑n - ↑n₂)).natAbs.divisors

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.card_iv3ResonanceDivisorPairs (d₁ n : ℕ) (P : ℤ) : (iv3ResonanceDivisorPairs d₁ n P).card = ∑ n₂ ∈ P.natAbs.divisors, (fouvryTau 2) (P * (↑d₁ * ↑n - ↑n₂)).natAbs

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3ResonanceEncode (t : ℕ × ℕ × ℤ) : (_ : ℕ) × ℕ

Forget the uniquely determined signed frequency, not either natural coordinate.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3ResonanceEncode t = ⟨t.1, t.2.1⟩

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_resonance_encode_injOn {d₁ n n₂' s' : ℕ} {a h : ℤ} (ha : a ≠ 0) (hδ' : ↑d₁ * ↑n - ↑n₂' ≠ 0) {S : Finset (ℕ × ℕ × ℤ)} (hS : ∀ t ∈ S, 0 < t.1 ∧ 0 < t.2.1 ∧ iv3CorrelationNumerator d₁ n t.1 n₂' t.2.1 s' a h t.2.2 = 0) : Set.InjOn iv3ResonanceEncode ↑S

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_resonance_encode_mem {d₁ n n₂' s' : ℕ} {a h : ℤ} (ha : a ≠ 0) (hP : h * ↑n₂' * ↑s' ≠ 0) {t : ℕ × ℕ × ℤ} (hc : (d₁ * n).Coprime t.1) (hδ : ↑d₁ * ↑n - ↑t.1 ≠ 0) (hl : iv3CorrelationNumerator d₁ n t.1 n₂' t.2.1 s' a h t.2.2 = 0) : iv3ResonanceEncode t ∈ iv3ResonanceDivisorPairs d₁ n (h * ↑n₂' * ↑s')

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_resonance_card_le_divisor_sum {d₁ n n₂' s' : ℕ} {a h : ℤ} (ha : a ≠ 0) (hP : h * ↑n₂' * ↑s' ≠ 0) (hδ' : ↑d₁ * ↑n - ↑n₂' ≠ 0) (S : Finset (ℕ × ℕ × ℤ)) (hS : ∀ t ∈ S, 0 < t.1 ∧ 0 < t.2.1 ∧ (d₁ * n).Coprime t.1 ∧ ↑d₁ * ↑n - ↑t.1 ≠ 0 ∧ iv3CorrelationNumerator d₁ n t.1 n₂' t.2.1 s' a h t.2.2 = 0) : S.card ≤ ∑ n₂ ∈ (h * ↑n₂' * ↑s').natAbs.divisors, (fouvryTau 2) (h * ↑n₂' * ↑s' * (↑d₁ * ↑n - ↑n₂)).natAbs

A genuine aggregate bound over every resonant triple in an arbitrary finite carrier. There is no restriction to equal labels or equal frequencies.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_resonance_sum_le_divisor_sum {d₁ n n₂' s' : ℕ} {a h : ℤ} (ha : a ≠ 0) (hP : h * ↑n₂' * ↑s' ≠ 0) (hδ' : ↑d₁ * ↑n - ↑n₂' ≠ 0) (S : Finset (ℕ × ℕ × ℤ)) (hS : ∀ t ∈ S, 0 < t.1 ∧ 0 < t.2.1 ∧ (d₁ * n).Coprime t.1 ∧ ↑d₁ * ↑n - ↑t.1 ≠ 0 ∧ iv3CorrelationNumerator d₁ n t.1 n₂' t.2.1 s' a h t.2.2 = 0) (w : ℕ × ℕ × ℤ → ℝ) (W : ℕ → ℕ → ℝ) (hW : ∀ (j k : ℕ), 0 ≤ W j k) (hw : ∀ t ∈ S, w t ≤ W t.1 t.2.1) : ∑ t ∈ S, w t ≤ ∑ n₂ ∈ (h * ↑n₂' * ↑s').natAbs.divisors, ∑ s ∈ (h * ↑n₂' * ↑s' * (↑d₁ * ↑n - ↑n₂)).natAbs.divisors, W n₂ s

Coordinate-dependent nonnegative weights can be summed directly over the finite divisor encoding; arbitrary signed original weights are allowed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_resonance_sum_le_const_mul {d₁ n n₂' s' : ℕ} {a h : ℤ} (ha : a ≠ 0) (hP : h * ↑n₂' * ↑s' ≠ 0) (hδ' : ↑d₁ * ↑n - ↑n₂' ≠ 0) (S : Finset (ℕ × ℕ × ℤ)) (hS : ∀ t ∈ S, 0 < t.1 ∧ 0 < t.2.1 ∧ (d₁ * n).Coprime t.1 ∧ ↑d₁ * ↑n - ↑t.1 ≠ 0 ∧ iv3CorrelationNumerator d₁ n t.1 n₂' t.2.1 s' a h t.2.2 = 0) (w : ℕ × ℕ × ℤ → ℝ) {B : ℝ} (hB : 0 ≤ B) (hw : ∀ t ∈ S, w t ≤ B) : ∑ t ∈ S, w t ≤ B * ∑ n₂ ∈ (h * ↑n₂' * ↑s').natAbs.divisors, ↑((fouvryTau 2) (h * ↑n₂' * ↑s' * (↑d₁ * ↑n - ↑n₂)).natAbs)

In particular each fixed Gram weight or span bound can be paid once per divisor encoding, with the actual resonance multiplicity.