theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wellFactorable_signedError_sq_le_five_small_extracted_kscale {ι : Type u_1} {κ k i j : ℕ} (A : ℕ) {T : ι → ℝ} {N : ι → Finset ℕ} {β : ι → ℕ → ℝ} (hSW : BetaCoprimeSWFamily κ T N β) (hT : ∀ (z : ι), 1 ≤ T z) (hN : ∀ (z : ι), ∀ n ∈ N z, T z ≤ ↑n ∧ ↑n ≤ 2 * T z) (hβ : ∀ (z : ι), ∀ n ∈ N z, |β z n| ≤ ↑((fouvryTau k) n)) {Cscale ε η : ℝ} (hCscale : 1 ≤ Cscale) (hε : 0 < ε) (hη : 0 < η) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (z : ι) (M ν : ℝ), 1 ≤ M → 4 * M * T z = x → ε ≤ ν → ν ≤ 1 / 10 + ε / 10 → T z = x ^ ν → ∀ (S Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → Q ⊆ Finset.Ioc 0 ⌊x ^ ((5 - 5 * ν) / 9 - ε)⌋₊ → ∀ (α c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → SignedWellFactorable j (x ^ ((5 - 5 * ν) / 9 - ε)) c → have R₀ := x ^ c2RExponent ν ε; have S₀ := x ^ c2SExponent ν ε; R₀ * S₀ = x ^ ((5 - 5 * ν) / 9 - ε) ∧ ∃ (γ : ℕ → ℝ) (ζ : ℕ → ℝ), factorSupported R₀ γ ∧ factorSupported S₀ ζ ∧ (∀ (r : ℕ), |γ r| ≤ ↑((fouvryTau j) r)) ∧ (∀ (s : ℕ), |ζ s| ≤ ↑((fouvryTau j) s)) ∧ c = factorConvolution γ ζ ∧ ∀ (a : ℤ), a ≠ 0 → |↑a| ≤ Cscale * x → signedError S (N z) Q α (β z) c a ^ 2 ≤ (8 * ∑ m ∈ S, α m ^ 2) * wMaskedFactorExtractedTruncated M (wUniformCutoff M (x ^ η)) (N z) Q (betaClean (β z) a) (factorConvolution γ (betaLowOmega ζ (highOmegaCutoff x))) γ ζ a (c2FiveSmallMask x η) R₀ S₀ (highOmegaCutoff x) + x ^ 2 / Real.log x ^ A