theorem DirichletCharacter.twistedSmoothedPsiClose_aux {q : ℕ} (SmoothingF : ℝ → ℝ) (c₁ : ℝ) (c₁_pos : 0 < c₁) (c₁_lt : c₁ < 1) (c₂ : ℝ) (c₂_pos : 0 < c₂) (c₂_lt : c₂ < 2) (hc₂ : ∀ (ε x : ℝ), ε ∈ Set.Ioo 0 1 → 1 + c₂ * ε ≤ x → Smooth1 SmoothingF ε x = 0) (C : ℝ) (C_eq : C = 6 * (3 * c₁ + c₂)) (ε : ℝ) (ε_pos : 0 < ε) (ε_lt_one : ε < 1) (X : ℝ) (X_pos : 0 < X) (X_gt_three : 3 < X) (X_bound_1 : 1 ≤ X * ε * c₁) (X_bound_2 : 1 ≤ X * ε * c₂) (smooth1BddAbove : ∀ (n : ℕ), 0 < n → Smooth1 SmoothingF ε (↑n / X) ≤ 1) (smooth1BddBelow : ∀ (n : ℕ), 0 < n → 0 ≤ Smooth1 SmoothingF ε (↑n / X)) (smoothIs1 : ∀ (n : ℕ), 0 < n → ↑n ≤ X * (1 - c₁ * ε) → Smooth1 SmoothingF ε (↑n / X) = 1) (smoothIs0 : ∀ (n : ℕ), 1 + c₂ * ε ≤ ↑n / X → Smooth1 SmoothingF ε (↑n / X) = 0) (χ : DirichletCharacter ℂ q) : ‖χ.twistedSmoothedPsi SmoothingF ε X - AnalyticNumberTheory.LargeSieve.lambdaCharacterPrefix ⌊X⌋₊ q χ‖ ≤ 2 * C * ε * X * Real.log X

A termwise (hence twist-safe) version of the transition-band estimate.

theorem DirichletCharacter.twistedSmoothedPsiClose {q : ℕ} (χ : DirichletCharacter ℂ q) {SmoothingF : ℝ → ℝ} (_diffSmoothingF : ContDiff ℝ 1 SmoothingF) (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (SmoothingFnonneg : ∀ x > 0, 0 ≤ SmoothingF x) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1) : ∃ C > 0, ∀ (X : ℝ), 3 < X → ∀ (ε : ℝ), 0 < ε → ε < 1 → 2 < X * ε → ‖χ.twistedSmoothedPsi SmoothingF ε X - AnalyticNumberTheory.LargeSieve.lambdaCharacterPrefix ⌊X⌋₊ q χ‖ ≤ C * ε * X * Real.log X

The smoothed von Mangoldt sum twisted by an arbitrary Dirichlet character is close to the genuine finite character prefix through ⌊X⌋₊. The proof is termwise: ‖χ n‖ ≤ 1 is applied before the two nonnegative transition bands are bounded by SmoothedChebyshevClose_aux.