Exact reindexing of the remaining IV.3 section

The signed dyadic rectangle, the five prefix caps and the Lemma 7 cell are retained. The only varying restrictions are an explicit interval and coprimalities. This does not yet freeze the small-root phase or pay for the residue classes needed in an application of the progression bound.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionFixedGrid (x : ℝ) (N : Finset ℕ) (S : ℝ) (r n₁ n₂ s : ℕ) (h : ℤ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) : Prop

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionFixedGrid x N S r n₁ n₂ s h j cap positive c = (Nat.log 2 h.natAbs = j 0 ∧ Nat.log 2 n₁ = j 2 ∧ Nat.log 2 r = j 3 ∧ Nat.log 2 s = j 4 ∧ h.natAbs ≤ cap 0 ∧ n₁ ≤ cap 2 ∧ r ≤ cap 3 ∧ s ≤ cap 4 ∧ decide (0 < h) = positive ∧ LiLiuPrereqFouvry.CoprimePartition.cell (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimePairBound N S) (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeOrder x) (LiLiuPrereqFouvry.CoprimePartition.matrixColor (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimePairBound N S) (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wCoprimeOrder x) (n₂, n₁ * s)) = c)

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionGridLower (M Z : ℝ) (K : WExtractedKey) (r s : ℕ) (h : ℤ) (j : Fin 5 → ℕ) : ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionGridLower M Z K r s h j = max (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionLower M Z K r s h) (2 ^ j 1)

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionGridUpper (R S : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) : ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionGridUpper R S K j cap = min (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionUpper R S K) (min (cap 1) (2 ^ (j 1 + 1) - 1))

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionCarrier (N : Finset ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (r n₁ n₂ s : ℕ) (h : ℤ) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) : Finset ℕ

A filter of an explicitly given interval, with no hidden membership test. Every condition apart from wKSectionCoprime is fixed on the section.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionCarrier N a x η R S M Z K r n₁ n₂ s h b j cap positive c = {k ∈ Finset.Icc (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionGridLower M Z K r s h j) (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionGridUpper R S K j cap) | MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionFixedSupport N a x η R S K r n₁ n₂ s ∧ 2 ^ b ≤ h.natAbs ∧ h.natAbs < 2 ^ (b + 1) ∧ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionFixedGrid x N S r n₁ n₂ s h j cap positive c ∧ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionCoprime K a r n₁ s k}

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionSlice (U : Finset (WExtractedTuple × ℤ)) (r n₁ n₂ s : ℕ) (h : ℤ) : Finset (WExtractedTuple × ℤ)

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionSlice U r n₁ n₂ s h = {t ∈ U | t.1.1.2.1 = r ∧ (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuple (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal t.1)).n₁ = n₁ ∧ (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuple (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal t.1)).n₂ = n₂ ∧ t.1.1.2.2 = s ∧ t.2 = h}

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionTuple_mem_filtered_iff {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {a : ℤ} {x η R S M Z : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) (hM : 0 < M) (hZ : 0 < Z) {K : WExtractedKey} {r n₁ n₂ s k : ℕ} {h : ℤ} {b : ℕ} (hf : wKSectionFixedCanonical K r n₁ n₂ s) (hΔ : 0 < K.2) (hΔ' : 0 < wKSectionDeltaPrime K) (he : K.2 * wKSectionDeltaPrime K = K.1.2.2.1 * K.1.2.2.2.2) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) : wKSectionTuple K r n₁ n₂ s h k ∈ wCoprimeFiber x N S (wAnalyticPrefix (wAnalyticDyadicBlock (wExtractedKeyFiber (wFloorCutoff M Z) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) j positive) cap) c ↔ k ∈ wKSectionCarrier N a x η R S M Z K r n₁ n₂ s h b j cap positive c

The actual coprime-cell/dyadic/prefix membership has no further varying restrictions beyond the displayed arithmetic carrier.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wKSectionSlice {A : Type u_1} [AddCommMonoid A] {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {a : ℤ} {x η R S M Z : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) (hM : 0 < M) (hZ : 0 < Z) {K : WExtractedKey} {r n₁ n₂ s : ℕ} {h : ℤ} {b : ℕ} (hf : wKSectionFixedCanonical K r n₁ n₂ s) (hΔ : 0 < K.2) (hΔ' : 0 < wKSectionDeltaPrime K) (he : K.2 * wKSectionDeltaPrime K = K.1.2.2.1 * K.1.2.2.2.2) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (F : WExtractedTuple × ℤ → A) : ∑ t ∈ wKSectionSlice (wCoprimeFiber x N S (wAnalyticPrefix (wAnalyticDyadicBlock (wExtractedKeyFiber (wFloorCutoff M Z) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) j positive) cap) c) r n₁ n₂ s h, F t = ∑ k ∈ wKSectionCarrier N a x η R S M Z K r n₁ n₂ s h b j cap positive c, F (wKSectionTuple K r n₁ n₂ s h k)

Exact summed reindexing of real original tuples, for arbitrary additive weights. In particular the small-root product and both signed coefficients may be inserted without changing any domain condition.