Positive coordinates for five-variable partial summation

The frequency sign is kept separate. Coordinate cutoffs select genuine rectangular prefixes of the actual arithmetic carrier; they do not erase compatibility, residue, low-omega, or original-support conditions.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticCoordinates (t : WExtractedTuple × ℤ) : Fin 5 → ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticCoordinates t = ![t.2.natAbs, (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuple (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal t.1)).k₁, (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuple (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal t.1)).n₁, t.1.1.2.1, t.1.1.2.2]

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticCoordinates_pos {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {t : WExtractedTuple × ℤ} (ht : t ∈ wExtractedKeyFiber H N Q a P R S ξ b K) (i : Fin 5) : 0 < wAnalyticCoordinates t i

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wDyadicScale (n : ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wDyadicScale n = 2 ^ Nat.log 2 n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wDyadicScale_pos (n : ℕ) : 0 < wDyadicScale n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wDyadicScale_bounds {n : ℕ} (hn : 0 < n) : wDyadicScale n ≤ ↑n ∧ ↑n < 2 * wDyadicScale n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wDyadicScale_normalized {n : ℕ} (hn : 0 < n) : ↑n / wDyadicScale n ∈ Set.Icc 1 2

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicKey (t : WExtractedTuple × ℤ) : Fin 5 → ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicKey t i = Nat.log 2 (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticCoordinates t i)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticPrefix (T : Finset (WExtractedTuple × ℤ)) (v : Fin 5 → ℕ) : Finset (WExtractedTuple × ℤ)

Prefixes are taken in all five analytic variables, with the original fiber and its arithmetic masks still present.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticPrefix T v = {t ∈ T | ∀ (i : Fin 5), MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticCoordinates t i ≤ v i}

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticPrefixSum (T : Finset (WExtractedTuple × ℤ)) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (v : Fin 5 → ℕ) : ℂ

The correct arithmetic sum left after removing only the slow weight.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticPrefixSum T β c₁ γ ζ a v = ∑ t ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticPrefix T v, ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedCoefficient β c₁ γ ζ t.1) * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedArithmeticPhase a t.2 t.1

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicBlock (T : Finset (WExtractedTuple × ℤ)) (j : Fin 5 → ℕ) (positive : Bool) : Finset (WExtractedTuple × ℤ)

Fix the sign as well as dyadic sizes before passing to a positive continuous rectangle. false denotes the negative frequency branch.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicBlock T j positive = {t ∈ T | MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicKey t = j ∧ decide (0 < t.2) = positive}

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicBlock_bounds {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {j : Fin 5 → ℕ} {positive : Bool} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber H N Q a P R S ξ b K) j positive) (i : Fin 5) : 2 ^ j i ≤ ↑(wAnalyticCoordinates t i) ∧ ↑(wAnalyticCoordinates t i) < 2 * 2 ^ j i

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicBlock_frequency {T : Finset (WExtractedTuple × ℤ)} {j : Fin 5 → ℕ} {positive : Bool} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock T j positive) : ↑t.2 = (if positive = true then 1 else -1) * ↑(wAnalyticCoordinates t 0)

The original signed integer frequency is recovered from its positive coordinate and its sign, including all unit-frequency cases.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticUnitCoordinates (j : Fin 5 → ℕ) (t : WExtractedTuple × ℤ) : Fin 5 → ℝ

Every point of a nonempty dyadic block lies in the full positive unit rectangle used by the smooth-weight estimate.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticUnitCoordinates j t i = ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticCoordinates t i) / 2 ^ j i

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticUnitCoordinates_mem {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {j : Fin 5 → ℕ} {positive : Bool} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber H N Q a P R S ξ b K) j positive) (i : Fin 5) : wAnalyticUnitCoordinates j t i ∈ Set.Icc 1 2

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wAnalyticDyadicBlocks {A : Type u_1} [AddCommMonoid A] (T : Finset (WExtractedTuple × ℤ)) (F : WExtractedTuple × ℤ → A) : ∑ t ∈ T, F t = ∑ j ∈ Finset.image wAnalyticDyadicKey T, (∑ t ∈ wAnalyticDyadicBlock T j true, F t + ∑ t ∈ wAnalyticDyadicBlock T j false, F t)

An exact finite partition into signed dyadic rectangles. Repeated coordinate values, including different n₂ values, retain multiplicity.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticCoordinateBound (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) : ℕ

A scale bound for the actual coordinates, including retained frequency, derived without replacing the carrier by an arbitrary rectangular set.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticCoordinateBound H N Q a P R S ξ = max (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedMaxFrequency H N Q a P R S ξ) (max (Q.sup id) (N.sup id))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticCoordinates_le_bound {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {t : WExtractedTuple × ℤ} (ht : t ∈ wExtractedKeyFiber H N Q a P R S ξ b K) (i : Fin 5) : wAnalyticCoordinates t i ≤ wAnalyticCoordinateBound H N Q a P R S ξ

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicKey_image_card_le (T : Finset (WExtractedTuple × ℤ)) (B : ℕ) (hB : ∀ t ∈ T, ∀ (i : Fin 5), wAnalyticCoordinates t i ≤ B) : (Finset.image wAnalyticDyadicKey T).card ≤ (Nat.log 2 B + 1) ^ 5

An explicit polynomial in logarithms pays all five dyadic coordinates. The existing fixed frequency shell can only reduce this coarse count.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyFiber_dyadic_card_le {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) (b : ℕ) (K : WExtractedKey) : (Finset.image wAnalyticDyadicKey (wExtractedKeyFiber H N Q a P R S ξ b K)).card ≤ (Nat.log 2 (wAnalyticCoordinateBound H N Q a P R S ξ) + 1) ^ 5