Full-tail payment at the constructed cutoff

The cutoff is always wUniformCutoff M (x ^ η). The rapid-decay order is chosen only in the proof, never by changing this cutoff. The estimate holds for every arithmetic mask, signed weights, and residue, with no SW input.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWNonzeroMode_sub_truncated_eq_full_tail (M : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) : smoothWNonzeroMode M N Q β c a - truncatedWNonzeroMode M H N Q β c a = wMaskedTail M H N Q β c a fun (x : WOriginalTuple) => True

The full tail is exactly the difference between the infinite nonzero mode and its actual finite-frequency truncation.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTail_uniformCutoff_alpha_log_payment (i k j A : ℕ) {η : ℝ} (hη : 0 < η) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M : ℝ), 0 < M → ∀ (S N Q : Finset ℕ), S ⊆ Finset.Ioc 0 ⌊x⌋₊ → N ⊆ Finset.Ioc 0 ⌊x⌋₊ → Q ⊆ Finset.Ioc 0 ⌊x⌋₊ → ∀ (α β c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ) (P : WOriginalTuple → Prop), (∑ m ∈ S, α m ^ 2) * |wMaskedTail M (wUniformCutoff M (x ^ η)) N Q β c a P| ≤ x ^ 2 / Real.log x ^ A

Uniform alpha-squared logarithmic payment of the actual masked tail. All divisor orders may be zero. No relation between M and the supports is needed beyond positivity of M and their common upper endpoint x.