Large common-modulus payment at the C.2 dyadic scale

The actual beta endpoint is 2 * T when 4 * M * T = x. Both lengths have a positive power lower bound with exponent min ε (min η (1 / 2)). The original sum, zero mode and tail use one identical arbitrary mask. The frequency cutoff is exactly wUniformCutoff M (x ^ η) throughout. The fixed shift scale precedes the eventual threshold and all changing data. The upper bound T ≤ x^(1/9) is used only to deduce sqrt x ≤ M from the eventual inequality 4*x^(1/9+1/2) ≤ x.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.betaClean_wMaskedTruncated_largeDelta_dyadic_kscale (i k j A : ℕ) {ε η Cscale : ℝ} (hε : 0 < ε) (hη : 0 < η) (hCscale : 1 ≤ Cscale) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M T L : ℝ), 1 ≤ M → 1 ≤ T → 1 ≤ L → 4 * M * T = x → x ^ ε ≤ T → T ≤ x ^ (1 / 9) → L ≤ x ^ (5 / 9) → ∀ (S N Q : Finset ℕ), (∀ m ∈ S, M ≤ ↑m ∧ ↑m ≤ 2 * M) → (∀ n ∈ N, T ≤ ↑n ∧ ↑n ≤ 2 * T) → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (α β c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ), |↑a| ≤ Cscale * x → ∀ (P : WOriginalTuple → Prop), (∀ t ∈ wOriginalTuples N Q a, P t → x ^ η < ↑(t.1.1.gcd t.1.2)) → (∑ m ∈ S, α m ^ 2) * |wMaskedTruncated M (wUniformCutoff M (x ^ η)) N Q (betaClean β a) c a P| ≤ x ^ 2 / Real.log x ^ A

Uniform logarithmic payment of every submask of the large common-modulus part of the actual clean truncated W sum. No SW or nondivisibility assumption on the original beta is required, and every divisor order may be zero.