theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticGridWeight_variation_bound_kscale {Cscale M T x Z y : ℝ} (hCscale : 1 ≤ Cscale) (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| ≤ Cscale * 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) : LiLiuPrereqFouvry.Rectangle.variation (wAnalyticBoxLo j) (wAnalyticBoxHi j) (wAnalyticGridWeight K j positive a (M * y)) ≤ wAnalyticVariationConstant (Cscale * Z)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticDyadicWeightedBlock_norm_le_prefix_kscale {Cscale M T x Z y : ℝ} (hCscale : 1 ≤ Cscale) (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| ≤ Cscale * x) (β c₁ γ ζ : ℕ → ℝ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) (b : ℕ) (K : WExtractedKey) (j : Fin 5 → ℕ) (positive : Bool) : have U := wExtractedKeyFiber (wFloorCutoff M Z) N Q a P R S ξ b K; ‖wAnalyticDyadicWeightedBlock U K j positive β c₁ γ ζ a (M * y)‖ ≤ wBlockAmplitude K j * wAnalyticVariationConstant (Cscale * Z) * wAnalyticBlockPrefixMax (wAnalyticDyadicBlock U j positive) j β c₁ γ ζ a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedFloorKeyExponential_norm_le_prefixes_kscale {Cscale M T x Z y : ℝ} (hCscale : 1 ≤ Cscale) (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| ≤ Cscale * x) (β c₁ γ ζ : ℕ → ℝ) (P : WOriginalTuple → Prop) (R S ξ : ℝ) (b : ℕ) (K : WExtractedKey) : ‖wExtractedKeyExponential (wFloorCutoff M Z) N Q β c₁ γ ζ a P R S ξ b K (M * y)‖ ≤ wAnalyticVariationConstant (Cscale * Z) * wAnalyticKeyPrefixMajorant (wExtractedKeyFiber (wFloorCutoff M Z) N Q a P R S ξ b K) K β c₁ γ ζ a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wAnalyticVariationConstant_kscale {Cscale Z : ℝ} (hC : 1 ≤ Cscale) (hZ : 0 ≤ Z) : wAnalyticVariationConstant (Cscale * Z) ≤ Cscale ^ 5 * wAnalyticVariationConstant Z

A fixed enlargement of the residue only adds a fixed fifth-power variation cost.