Concrete normalized slow-phase parameters on actual dyadic W blocks

The parameter bound is derived from a member of the actual floor-retained carrier. It therefore applies to the entire continuous normalized rectangle without mistaking an arbitrary key-box member for positive canonical data.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.normalizedWeight_eq_fourierChar (A B : ℝ) (v : Fin 5 → ℝ) : LiLiuPrereqFouvry.SlowFactor.normalizedWeight A B v = ↑(v 1 * v 3 * v 4)⁻¹ * ↑(Real.fourierChar (A * v 0 / (v 1 * v 3 * v 4) + B * v 0 / (v 1 * v 2 * v 3 * v 4)))

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wBlockAmplitude (K : WExtractedKey) (j : Fin 5 → ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wBlockAmplitude K j = (↑K.D * 2 ^ j 1 * 2 ^ j 3 * 2 ^ j 4)⁻¹

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wBlockPhaseA (K : WExtractedKey) (j : Fin 5 → ℕ) (positive : Bool) (u : ℝ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wBlockPhaseA K j positive u = (-if positive = true then 1 else -1) * 2 ^ j 0 * u / (↑K.D * 2 ^ j 1 * 2 ^ j 3 * 2 ^ j 4)

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

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wBlockPhaseB K j positive a = (if positive = true then 1 else -1) * 2 ^ j 0 * ↑a / (2 ^ j 2 * 2 ^ j 1 * 2 ^ j 3 * 2 ^ j 4 * ↑K.D')

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticWeight_eq_normalized_block {U : Finset (WExtractedTuple × ℤ)} {j : Fin 5 → ℕ} {positive : Bool} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock U j positive) (K : WExtractedKey) (a : ℤ) (u : ℝ) : have v := wGCDTuple (wExtractedOriginal t.1); wAnalyticWeight K.D K.D' a u ↑t.2 ↑v.k₁ ↑v.n₁ ↑t.1.1.2.1 ↑t.1.1.2.2 = ↑(wBlockAmplitude K j) * LiLiuPrereqFouvry.SlowFactor.normalizedWeight (wBlockPhaseA K j positive u) (wBlockPhaseB K j positive a) (wAnalyticUnitCoordinates j t)

Exact transport to the concrete weight whose mixed derivatives and rectangular increments have been proved, including the frequency sign.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wBlockPhase_abs (K : WExtractedKey) (j : Fin 5 → ℕ) (positive : Bool) (hD : 0 < K.D) (hD' : 0 < K.D') (u : ℝ) (a : ℤ) : |wBlockPhaseA K j positive u| + |wBlockPhaseB K j positive a| = 2 ^ j 0 * (|u| / (↑K.D * 2 ^ j 1 * 2 ^ j 3 * 2 ^ j 4) + |↑a| / (2 ^ j 2 * 2 ^ j 1 * 2 ^ j 3 * 2 ^ j 4 * ↑K.D'))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicBlock_parameter_budget {M T x Z y : ℝ} (hM : 0 < M) (hT : 0 < T) (hZ : 0 ≤ Z) (hx : x = 4 * M * T) (hy : y ∈ Set.Icc (1 / 2) 3) {N Q : Finset ℕ} (hN : ∀ n ∈ N, T ≤ ↑n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} (ha : |↑a| ≤ x) {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {j : Fin 5 → ℕ} {positive : Bool} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber (wFloorCutoff M Z) N Q a P R S ξ b K) j positive) : |wBlockPhaseA K j positive (M * y)| + |wBlockPhaseB K j positive a| ≤ 112 * Z

The actual large-residue assumptions bound the two reference coefficients by 112 Z, independently of every changing arithmetic parameter. The continuous normalized weight may now be estimated on all of [1,2]^5, keeping its own explicit coordinate constants.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicBlock_mixedDeriv_bound {M T x Z y : ℝ} (hM : 0 < M) (hT : 0 < T) (hZ : 0 ≤ Z) (hx : x = 4 * M * T) (hy : y ∈ Set.Icc (1 / 2) 3) {N Q : Finset ℕ} (hN : ∀ n ∈ N, T ≤ ↑n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} (ha : |↑a| ≤ x) {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {j : Fin 5 → ℕ} {positive : Bool} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber (wFloorCutoff M Z) N Q a P R S ξ b K) j positive) (js : List (Fin 5)) (hjs : js.Nodup) (v : Fin 5 → ℝ) (hv : ∀ (i : Fin 5), 1 ≤ v i ∧ v i ≤ 2) : ‖LiLiuPrereqFouvry.SlowFactor.mixedDeriv js (LiLiuPrereqFouvry.SlowFactor.normalizedWeight (wBlockPhaseA K j positive (M * y)) (wBlockPhaseB K j positive a)) v‖ ≤ 64 * (6 + 2 * Real.pi) ^ 5 * (1 + 112 * Z) ^ 5

The actual source parameters now satisfy the full five-variable mixed-derivative bound, not an assumed derivative or variation estimate.