The ratio-counting box for actual occupied secondary bases

The sign of both frequencies is fixed by the original block. Absolute values therefore give an injection, without identifying positive and negative labels. The three beta coordinates retain their distinct multiplicities.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.secondaryRatioQuadruples (H B : ℕ) : Finset ((ℕ × ℕ) × ℕ × ℕ)

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.secondaryRatioQuadruples H B = {p ∈ (Finset.Ioc 0 H ×ˢ Finset.Ico B (2 * B)) ×ˢ Finset.Ioc 0 H ×ˢ Finset.Ioc 0 (2 * B) | p.2.1 * p.1.2 = p.1.1 * p.2.2}

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.secondaryRatioQuadruples_card (H B : ℕ) : (secondaryRatioQuadruples H B).card = ∑ h ∈ Finset.Ioc 0 H, ∑ s ∈ Finset.Ico B (2 * B), (secondaryRatioPartners H (2 * B) h s).card

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.secondaryRatioQuadruples_card_le {B : ℕ} (hB : 0 < B) (H : ℕ) : ↑(secondaryRatioQuadruples H B).card ≤ 4 * ↑H * ↑B * (1 + Real.log ↑H)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.secondary_frequency_natAbs_injective (i : ℕ) (positive : Bool) : Set.InjOn Int.natAbs ↑(wGramResonanceScaleFrequencies i positive)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramPrefix_coordinate_mem_scale {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {a : ℤ} {x η R S M Z : ℝ} {K : WExtractedKey} {b : ℕ} {j cap : Fin 5 → ℕ} {positive : Bool} {c : Finset (ℕ × ℕ)} {t : WExtractedTuple × ℤ} (ht : t ∈ wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c) (i : Fin 5) : wAnalyticCoordinates t i ∈ wGramResonanceScaleInterval (j i)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramPrefix_frequency_mem_scale {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {a : ℤ} {x η R S M Z : ℝ} {K : WExtractedKey} {b : ℕ} {j cap : Fin 5 → ℕ} {positive : Bool} {c : Finset (ℕ × ℕ)} {t : WExtractedTuple × ℤ} (ht : t ∈ wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c) : t.2 ∈ wGramResonanceScaleFrequencies (j 0) positive

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryBases_scale_data {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {F : ℕ} (hNF : ∀ n ∈ N, n ≤ F) {a : ℤ} {x η R S M Z : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) (hM : 0 < M) (hZ : 0 < 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))) : v.1 ∈ wGramResonanceScaleInterval (j 2) ∧ v.2.1.1 ∈ Finset.Ioc 0 (F / K.1.1) ∧ v.2.2.1 ∈ Finset.Ioc 0 (F / K.1.1) ∧ v.2.1.2.1 ∈ wGramResonanceScaleInterval (j 4) ∧ v.2.2.2.1 ∈ wGramResonanceScaleInterval (j 4) ∧ v.2.1.2.2 ∈ wGramResonanceScaleFrequencies (j 0) positive ∧ v.2.2.2.2 ∈ wGramResonanceScaleFrequencies (j 0) positive ∧ v.2.2.2.2 * ↑v.2.1.2.1 = v.2.1.2.2 * ↑v.2.2.2.1

An occupied seven-coordinate base supplies every scale bound before any extension to a Cartesian box is made.

@[reducible, inline]

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

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGramSecondaryRatioCode = ((ℕ × ℕ × ℕ) × (ℕ × ℕ) × ℕ × ℕ)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryRatioCode (v : WGramSecondaryBase) : WGramSecondaryRatioCode

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryRatioCode v = ((v.1, v.2.1.1, v.2.2.1), (v.2.1.2.2.natAbs, v.2.1.2.1), v.2.2.2.2.natAbs, v.2.2.2.1)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryRatioBox (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) : Finset WGramSecondaryRatioCode

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryRatioBox K F j = (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleInterval (j 2) ×ˢ Finset.Ioc 0 (F / K.1.1) ×ˢ Finset.Ioc 0 (F / K.1.1)) ×ˢ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.secondaryRatioQuadruples (2 ^ (j 0 + 1)) (2 ^ j 4)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSecondaryRatioBox_card_le (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) : ↑(wGramSecondaryRatioBox K F j).card ≤ ↑(2 ^ j 2) * ↑(F / K.1.1) ^ 2 * (4 * ↑(2 ^ (j 0 + 1)) * ↑(2 ^ j 4) * (1 + Real.log ↑(2 ^ (j 0 + 1))))