Kadiri.zeroImagSquareTailSummable_of_crude_majorant

theorem zeroImagSquareTailSummable_of_crude_majorant :    zeroImagSquareTailSummable := by  obtain ⟨E, hE0, hE⟩ := zetaCountingDyadic_abs_N_le_geometric  obtain ⟨A, D, hA0, hD0, hcountN⟩ :=    zeroImagDyadicCumulativeCountByNWithZeroHeightSource_of_conj_and_positive_height_zero_free  refine zeroImagSquareTailSummable_of_cumulative_count_le    (g := fun k => A * (E * 3 ^ k) + D) ?_ (fun k => ?_)  · have hterm : ∀ k : ℕ,        A * E * (3 / 4 : ℝ) ^ k + D * ((4 : ℝ)⁻¹) ^ k =          (A * (E * 3 ^ k) + D) * (((2 : ℝ) ^ k)⁻¹) ^ (2 : ℕ) := by      intro k      have h4 : (((2 : ℝ) ^ k)⁻¹) ^ (2 : ℕ) = ((4 : ℝ)⁻¹) ^ k := by        rw [inv_pow, ← pow_mul, mul_comm k 2, pow_mul, ← inv_pow]        norm_num      have h34 : ((3 : ℝ) / 4) ^ k = 3 ^ k * ((4 : ℝ)⁻¹) ^ k := by        rw [← mul_pow]        norm_num      rw [h4, h34]      ring    exact (((summable_geometric_of_lt_one (by norm_num)      (by norm_num : (3 / 4 : ℝ) < 1)).mul_left (A * E)).add      ((summable_geometric_of_lt_one (by norm_num)        (by norm_num : ((4 : ℝ)⁻¹) < 1)).mul_left D)).congr hterm  · exact (hcountN k).trans      (add_le_add (mul_le_mul_of_nonneg_left (hE k) hA0) le_rfl)