Kadiri.weighted_zeroImagSquareTail_summable

theorem weighted_zeroImagSquareTail_summable :    Summable (fun ρ : NontrivialZeros ↦      ((riemannZeta.order (ρ : ℂ) : ℤ) : ℝ) * zeroImagSquareTail ρ) := by  classical  have hhigh : Summable (fun ρ : {ρ : NontrivialZeros // 1 ≤ |(ρ : ℂ).im|} ↦      ((riemannZeta.order ((ρ.1 : NontrivialZeros) : ℂ) : ℤ) : ℝ) *        zeroImagSquareTail ρ.1) := by    have h := weighted_shell_sigma_summable.comp_injective      highZeroToDyadicShell_injective    simpa [Function.comp_def, highZeroToDyadicShell] using h  have hlow_set : ({ρ : NontrivialZeros | ¬ 1 ≤ |(ρ : ℂ).im|} :      Set NontrivialZeros).Finite := by    apply Set.Finite.subset nontrivialZeros_abs_im_lt_one_finite    intro ρ hρ    rw [Set.mem_setOf_eq] at hρ ⊢    exact lt_of_not_ge hρ  haveI : Finite {ρ : NontrivialZeros // ¬ 1 ≤ |(ρ : ℂ).im|} :=    Set.finite_coe_iff.mpr hlow_set  have hlow : Summable (fun ρ : {ρ : NontrivialZeros // ¬ 1 ≤ |(ρ : ℂ).im|} ↦      ((riemannZeta.order ((ρ.1 : NontrivialZeros) : ℂ) : ℤ) : ℝ) *        zeroImagSquareTail ρ.1) := Summable.of_finite  exact (summable_subtype_and_compl    (s := {ρ : NontrivialZeros | 1 ≤ |(ρ : ℂ).im|})).mp ⟨hhigh, hlow⟩