Kadiri.zeroImagDyadicNPrimeToNSource_of_order_summable

theorem zeroImagDyadicNPrimeToNSource_of_order_summable    (hsum : zeroImagDyadicNOrderSummableSource) :    zeroImagDyadicNPrimeToNSource := by  classical  refine ⟨1, by norm_num, ?_⟩  intro k  let T : ℝ := (2 : ℝ) ^ (k + 1)  let Crit := riemannZeta.zeroes_rect (.Ioo (0 : ℝ) 1) (.Ioo 0 T)  let All := riemannZeta.zeroes_rect (.univ : Set ℝ) (.Ioo 0 T)  have hcrit_finite : Finite Crit := by    exact Set.finite_coe_iff.mpr (zeroes_rect_Ioo_critical_positive_height_finite T)  letI : Fintype Crit := Fintype.ofFinite Crit  let inc : Crit ↪ All := {    toFun := fun rho =>      ⟨(rho : ℂ), Set.mem_univ _, rho.property.2.1, rho.property.2.2⟩    inj' := fun rho eta h => by      exact Subtype.ext (by simpa using congrArg Subtype.val h)  }  let fAll : All → ℝ := fun rho => (riemannZeta.order (rho : ℂ) : ℝ)  have hsumAll : Summable fAll := by    dsimp [fAll, All, T]    simpa [T] using hsum k  have hnonnegAll : ∀ rho : All, 0 ≤ fAll rho := by    intro rho    have horder : (0 : ℤ) ≤ riemannZeta.order (rho : ℂ) := by      exact le_of_lt (riemannZeta_order_pos_positiveHeightZero rho)    change 0 ≤ ((riemannZeta.order (rho : ℂ) : ℤ) : ℝ)    exact_mod_cast horder  have hNprime_eq :      riemannZeta.N' 0 T =        ∑ rho : Crit, (riemannZeta.order (rho : ℂ) : ℝ) := by    unfold riemannZeta.N' riemannZeta.zeroes_sum    rw [tsum_fintype]    simp [Crit]  have hN_eq :      riemannZeta.N T = ∑' rho : All, fAll rho := by    unfold riemannZeta.N riemannZeta.zeroes_sum    simp [All, fAll]  have hpartial :      (∑ rho : Crit, (riemannZeta.order (rho : ℂ) : ℝ)) ≤        ∑' rho : All, fAll rho := by    have hmap :        (∑ rho : Crit, (riemannZeta.order (rho : ℂ) : ℝ)) =          ∑ rho ∈ Finset.univ.map inc, fAll rho := by      simp [inc, fAll]    rw [hmap]    exact Summable.sum_le_tsum (Finset.univ.map inc)      (fun rho _ => hnonnegAll rho) hsumAll  have hNprime_nonneg : 0 ≤ riemannZeta.N' 0 T := by    rw [hNprime_eq]    exact Finset.sum_nonneg fun rho _ => by      have horder : (0 : ℤ) ≤ riemannZeta.order (rho : ℂ) := by        exact le_of_lt (riemannZeta_order_pos_positiveHeightZero (inc rho))      change 0 ≤ ((riemannZeta.order (rho : ℂ) : ℤ) : ℝ)      exact_mod_cast horder  have hN_nonneg : 0 ≤ riemannZeta.N T := by    rw [hN_eq]    exact tsum_nonneg hnonnegAll  have hNprime_le_N : riemannZeta.N' 0 T ≤ riemannZeta.N T := by    rw [hNprime_eq, hN_eq]    exact hpartial  calc    |riemannZeta.N' 0 ((2 : ℝ) ^ (k + 1))| = riemannZeta.N' 0 T := by      dsimp [T]      exact abs_of_nonneg hNprime_nonneg    _ ≤ riemannZeta.N T := hNprime_le_N    _ = |riemannZeta.N T| := (abs_of_nonneg hN_nonneg).symm    _ = 1 * |riemannZeta.N ((2 : ℝ) ^ (k + 1))| := by      dsimp [T]      ring