theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteContour_rectangle_vertical_identity {f : ℂ → ℂ} {β α T : ℝ} (hβα : β ≤ α) (hT : 0 ≤ T) (hf : DifferentiableOn ℂ f {s : ℂ | β ≤ s.re ∧ s.re ≤ α ∧ |s.im| ≤ T}) : (∫ (t : ℝ) in -T..T, chen1973VerticalSection f α t) - ∫ (t : ℝ) in -T..T, chen1973VerticalSection f β t = Complex.I * chen1973HorizontalSection f β α T

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteContour_mellinKernel_differentiableAt {x : ℕ} (hx : 3 ≤ x) {s : ℂ} (hs : 0 < s.re) : DifferentiableAt ℂ (chen1973MellinKernel ↑x) s

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteContour_term_differentiableOn {x d : ℕ} (hx : 3 ≤ x) (hd : 1 < d) (χ : PrimitiveCharacter d) {pp : ℕ × ℕ} (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) {T : ℝ} (hzero : ∀ (s : ℂ), chen1973Lemma6Eq21Sigma x ≤ s.re → s.re ≤ chen1973Lemma6Alpha x → |s.im| ≤ T → chen1973Lemma6PrimitiveLValue d s χ ≠ 0) : DifferentiableOn ℂ (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) {s : ℂ | chen1973Lemma6Eq21Sigma x ≤ s.re ∧ s.re ≤ chen1973Lemma6Alpha x ∧ |s.im| ≤ T}

Holomorphy of the actual term, using only nonvanishing on this rectangle.

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteContour_vertical_intervalIntegrable {f : ℂ → ℂ} {β α T v : ℝ} (hT : 0 ≤ T) (hv : v ∈ Set.Icc β α) (hf : ContinuousOn f {s : ℂ | β ≤ s.re ∧ s.re ≤ α ∧ |s.im| ≤ T}) : IntervalIntegrable (chen1973VerticalSection f v) MeasureTheory.volume (-T) T

Every finite vertical section is integrable before Cauchy is applied.

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteContour_horizontal_intervalIntegrable {f : ℂ → ℂ} {β α T t : ℝ} (hβα : β ≤ α) (ht : |t| ≤ T) (hf : ContinuousOn f {s : ℂ | β ≤ s.re ∧ s.re ≤ α ∧ |s.im| ≤ T}) : IntervalIntegrable (fun (v : ℝ) => f (↑v + ↑t * Complex.I)) MeasureTheory.volume β α

Every finite horizontal section is integrable on the genuine rectangle.

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteContour_integral_split {f : ℝ → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (T : ℝ) : ∫ (t : ℝ), f t = ((∫ (t : ℝ) in -T..T, f t) + ∫ (t : ℝ) in Set.Iio (-T), f t) + ∫ (t : ℝ) in Set.Ioi T, f t

Finite middle interval and two open tails, for an actually integrable function.

theorem AnalyticNumberTheory.LargeSieve.Eq21FiniteContour_actualPhi_eq_truncated_with_alpha_tails {x d : ℕ} (hx : 3 ≤ x) (hd : 1 < d) (χ : PrimitiveCharacter d) {pp : ℕ × ℕ} (hp₁ : 0 < pp.1) (hp₂ : 0 < pp.2) {T : ℝ} (hT : 0 ≤ T) (hzero : ∀ (s : ℂ), chen1973Lemma6Eq21Sigma x ≤ s.re → s.re ≤ chen1973Lemma6Alpha x → |s.im| ≤ T → chen1973Lemma6PrimitiveLValue d s χ ≠ 0) : chen1973Lemma6ActualPhi x d χ pp * ↑χ ↑(pp.1 * pp.2) = -(↑(1 / (2 * Real.pi)) * (((∫ (t : ℝ) in -T..T, chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Eq21Sigma x) t) + Complex.I * chen1973HorizontalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Eq21Sigma x) (chen1973Lemma6Alpha x) T + ∫ (t : ℝ) in Set.Iio (-T), chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Alpha x) t) + ∫ (t : ℝ) in Set.Ioi T, chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) (chen1973Lemma6Alpha x) t))

W2: exact signed decomposition of ActualPhi, with BOTH high tails on alpha. No sigma high-tail object or full-height nonvanishing is assumed.