BKLNW_app.bklnw_eq_A_9

@[blueprint  "bklnw-eq_A_9"  (title := "Equation (A.9)")  (statement := /-- We have  $$ \sum_{|\gamma| < T} \frac{x^{\rho-1}}{\rho}  = \Sigma_1 + \Sigma_2 $$ -/)  (proof := /-- Follows directly from the definitions  of Σ₁ and Σ₂. -/)  (latexEnv := "sublemma")  (discussion := 750)]theorem bklnw_eq_A_9 (x T δ : ℝ) (hδ1 : 0 ≤ δ) (hδ2 : δ ≤ 1) :    riemannZeta.zeroes_sum (Set.Icc 0 1)      (Set.Ioo (-T) T) (fun ρ ↦ x ^ (ρ - 1) / ρ) =    Sigma₁ x T δ + Sigma₂ x T δ := by  set I₁ : Set ℝ := Set.Ico 0 (1 - δ)  set I₂ : Set ℝ := Set.Icc (1 - δ) 1  set J  : Set ℝ := Set.Ioo (-T) T  set g  : ℂ → ℂ := fun ρ ↦ (x ^ (ρ - 1) / ρ) * (riemannZeta.order ρ)  change ∑' ρ : riemannZeta.zeroes_rect (Set.Icc 0 1) J, g ρ = _  have hI : Set.Icc 0 1 = I₁ ∪ I₂ := (Set.Ico_union_Icc_eq_Icc    (sub_nonneg_of_le hδ2) (sub_le_self 1 hδ1)).symm  have hdisj : Disjoint (riemannZeta.zeroes_rect I₁ J) (riemannZeta.zeroes_rect I₂ J) :=    riemannZeta.zeroes_rect_disjoint₁ I₁ I₂ J      (Set.disjoint_left.2 fun _ hx1 hx2 ↦ not_le.2 hx1.2 hx2.1)  have hfin : (riemannZeta.zeroes_rect (Set.Icc 0 1) J).Finite := by    rw [riemannZeta.zeroes_rect_eq]    refine (riemannZeta.zeroes_on_Compact_finite' ?_).subset      (Set.inter_subset_inter (Set.inter_subset_inter_right _        (Set.preimage_mono Set.Ioo_subset_Icc_self)) le_rfl)    exact Complex.equivRealProdCLM.toHomeomorph.isClosedEmbedding.isCompact_preimage      (isCompact_Icc.prod isCompact_Icc)  rw [hI, ← riemannZeta.zeroes_rect_union] at hfin ⊢  refine Summable.tsum_union_disjoint hdisj ?_ ?_  · exact (hfin.subset Set.subset_union_left).summable g  · exact (hfin.subset Set.subset_union_right).summable g