Actual arithmetic prefixes after five-variable partial summation

The original finite fiber remains inside every prefix, including its coupled frequency cutoff and arithmetic masks. Only the concrete smooth factor is differenced; no assertion that a prefix is an arithmetic progression is made.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticBoxLo (j : Fin 5 → ℕ) : Fin 5 → ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticBoxLo j i = 2 ^ j i

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticBoxHi (j : Fin 5 → ℕ) : Fin 5 → ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticBoxHi j i = 2 * 2 ^ j i

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticGridWeight (K : WExtractedKey) (j : Fin 5 → ℕ) (positive : Bool) (a : ℤ) (u : ℝ) (v : Fin 5 → ℕ) : ℂ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticGridWeight K j positive a u v = LiLiuPrereqFouvry.SlowFactor.normalizedWeight (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wBlockPhaseA K j positive u) (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wBlockPhaseB K j positive a) fun (i : Fin 5) => ↑(v i) / 2 ^ j i

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticBlockPrefixMax (B : Finset (WExtractedTuple × ℤ)) (j : Fin 5 → ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticBlockPrefixMax B j β c₁ γ ζ a = LiLiuPrereqFouvry.Rectangle.coordinatePrefixMax (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticBoxLo j) (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticBoxHi j) B MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticCoordinates fun (t : MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WExtractedTuple × ℤ) => ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedCoefficient β c₁ γ ζ t.1) * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedArithmeticPhase a t.2 t.1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticBlockPrefixMax_nonneg (B : Finset (WExtractedTuple × ℤ)) (j : Fin 5 → ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) : 0 ≤ wAnalyticBlockPrefixMax B j β c₁ γ ζ a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticPrefixSum_eq_coordinatePrefix (B : Finset (WExtractedTuple × ℤ)) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (cap : Fin 5 → ℕ) : wAnalyticPrefixSum B β c₁ γ ζ a cap = LiLiuPrereqFouvry.Rectangle.coordinatePrefix B wAnalyticCoordinates (fun (t : WExtractedTuple × ℤ) => ↑(wExtractedCoefficient β c₁ γ ζ t.1) * wExtractedArithmeticPhase a t.2 t.1) cap

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticPrefixSum_norm_le_max (B : Finset (WExtractedTuple × ℤ)) (j : Fin 5 → ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (cap : Fin 5 → ℕ) (hcap : cap ∈ LiLiuPrereqFouvry.Rectangle.box (wAnalyticBoxLo j) (wAnalyticBoxHi j)) : ‖wAnalyticPrefixSum B β c₁ γ ζ a cap‖ ≤ wAnalyticBlockPrefixMax B j β c₁ γ ζ a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticBlockPrefixMax_attained (B : Finset (WExtractedTuple × ℤ)) (j : Fin 5 → ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) : ∃ cap ∈ LiLiuPrereqFouvry.Rectangle.box (wAnalyticBoxLo j) (wAnalyticBoxHi j), wAnalyticBlockPrefixMax B j β c₁ γ ζ a = ‖wAnalyticPrefixSum B β c₁ γ ζ a cap‖

The finite maximum is attained by an actual arithmetic rectangular prefix, even when the underlying block is empty.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicWeightedBlock (U : Finset (WExtractedTuple × ℤ)) (K : WExtractedKey) (j : Fin 5 → ℕ) (positive : Bool) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (u : ℝ) : ℂ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicWeightedBlock U K j positive β c₁ γ ζ a u = ∑ t ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicBlock U j positive, have v := MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDTuple (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedOriginal t.1); ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedCoefficient β c₁ γ ζ t.1) * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedArithmeticPhase a t.2 t.1 * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticWeight K.D K.D' a u ↑t.2 ↑v.k₁ ↑v.n₁ ↑t.1.1.2.1 ↑t.1.1.2.2

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicWeightedBlock_eq_normalized (U : Finset (WExtractedTuple × ℤ)) (K : WExtractedKey) (j : Fin 5 → ℕ) (positive : Bool) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (u : ℝ) : wAnalyticDyadicWeightedBlock U K j positive β c₁ γ ζ a u = ↑(wBlockAmplitude K j) * ∑ t ∈ wAnalyticDyadicBlock U j positive, wAnalyticGridWeight K j positive a u (wAnalyticCoordinates t) * (↑(wExtractedCoefficient β c₁ γ ζ t.1) * wExtractedArithmeticPhase a t.2 t.1)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyExponential_eq_dyadicWeightedBlocks {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) (H : ℕ → ℕ → ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) (b : ℕ) (K : WExtractedKey) (u : ℝ) : have U := wExtractedKeyFiber H N Q a P R S ξ b K; wExtractedKeyExponential H N Q β c₁ γ ζ a P R S ξ b K u = ∑ j ∈ Finset.image wAnalyticDyadicKey U, (wAnalyticDyadicWeightedBlock U K j true β c₁ γ ζ a u + wAnalyticDyadicWeightedBlock U K j false β c₁ γ ζ a u)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicBlock_coordinates_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) : wAnalyticCoordinates t ∈ LiLiuPrereqFouvry.Rectangle.box (wAnalyticBoxLo j) (wAnalyticBoxHi j)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicWeightedBlock_norm_le_variation {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) (H : ℕ → ℕ → ℕ) (β c₁ γ ζ : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) (b : ℕ) (K : WExtractedKey) (j : Fin 5 → ℕ) (positive : Bool) (u : ℝ) : have U := wExtractedKeyFiber H N Q a P R S ξ b K; ‖wAnalyticDyadicWeightedBlock U K j positive β c₁ γ ζ a u‖ ≤ wBlockAmplitude K j * LiLiuPrereqFouvry.Rectangle.variation (wAnalyticBoxLo j) (wAnalyticBoxHi j) (wAnalyticGridWeight K j positive a u) * wAnalyticBlockPrefixMax (wAnalyticDyadicBlock U j positive) j β c₁ γ ζ a