Square-root payment of both section-length contributions

The second term is kept even when span/q exceeds D'. No lower bound such as H*s≥n is used. The local k is cancelled under the square root only after multiplication by the original reciprocal amplitude.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directNormalization_sqrt_frequency {A H B : ℝ} (hA : 0 < A) (hHB : H ≤ A * B) : A⁻¹ * √H ≤ √B / √A

Square-root frequency normalization, with the remaining local denominator.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directNormalization_sqrt_length {D Dprime k r s q span H B : ℝ} (hD : 0 < D) (hk : 0 < k) (hr : 0 < r) (hs : 0 < s) (hq : 0 < q) (hDp : 0 ≤ Dprime) (hspan : 0 ≤ span) (hH : H ≤ D * k * r * s * B) (hspanK : span ≤ 2 * k) : (D * k * r * s)⁻¹ * √H * √(Dprime + span / q) ≤ √B * (√Dprime / √(D * k * r * s) + √2 / √(D * r * s * q))

Two distinct section-length monomials after square-root normalization.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directNormalization_floor_sqrt_length {M T x Z : ℝ} (hM : 0 < M) (hT : 0 < T) (hZ : 0 ≤ Z) (hx : x = 4 * M * T) {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 (wFloorCutoff M Z) N Q a P R S ξ b K) j positive) (cap : Fin 5 → ℕ) (L : WGramLabel) (hq : 0 < wGramModulus L) : wBlockAmplitude K j * √(2 ^ j 0) * √(↑K.D' + ↑(wGramSpan R S M Z K j cap L) / ↑(wGramModulus L)) ≤ √(32 * Z * T / x) * (√↑K.D' / √(↑K.D * 2 ^ j 1 * 2 ^ j 3 * 2 ^ j 4) + √2 / √(↑K.D * 2 ^ j 3 * 2 ^ j 4 * ↑(wGramModulus L)))

The two-term root payment at the actual retained floor frequency. The free Gram label only supplies its original positive modulus and span; its phase/gcd/remaining energy factors are not asserted to be bounded here.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.directNormalization_floor_fullLevel_monomial {M T x Z L R S : ℝ} (hM : 0 < M) (hT : 0 < T) (hZ : 0 ≤ Z) (hx : x = 4 * M * T) (hL : 0 ≤ L) (hR : 0 ≤ R) (hS : 0 ≤ S) {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {a : ℤ} {P : WOriginalTuple → Prop} {ξ : ℝ} {b : ℕ} {K : WExtractedKey} {j : Fin 5 → ℕ} {positive : Bool} {t : WExtractedTuple × ℤ} (ht : t ∈ wAnalyticDyadicBlock (wExtractedKeyFiber (wFloorCutoff M Z) N (Finset.Ioc 0 ⌊L⌋₊) a P R S ξ b K) j positive) (p u v w : ℝ) (hp : 0 ≤ p) (hp1 : p ≤ 1) (hu : 0 ≤ p + u - 1) (hv : 0 ≤ p + v - 1) (hw : 0 ≤ p + w - 1) : wBlockAmplitude K j * (2 ^ j 0) ^ p * (2 ^ j 1) ^ u * (2 ^ j 3) ^ v * (2 ^ j 4) ^ w ≤ (32 * Z * T / x) ^ p * L ^ (p + u - 1) * R ^ (p + v - 1) * S ^ (p + w - 1)

A fully connected full-level corollary: first pay the local reciprocal, then enlarge only the resulting nonnegative coordinate exponents.