Kadiri.zeroImagDyadicShellMassBoundSource_of_count_bound

theorem zeroImagDyadicShellMassBoundSource_of_count_bound    (hsrc : zeroImagDyadicShellCountBoundSource) :    zeroImagDyadicShellMassBoundSource := by  rcases hsrc with ⟨C, hC_nonneg, hcount⟩  refine ⟨C, hC_nonneg, ?_⟩  intro k  have hmass := zeroHeightDyadicShellMass_le_count_inv_sq k  have hcountk := hcount k  have hsq_nonneg : 0 ≤ (((2 : ℝ) ^ k)⁻¹) ^ (2 : ℕ) := sq_nonneg _  have hmul :      (Nat.card {rho : NontrivialZeros // zeroHeightDyadicShell k rho} : ℝ) *          (((2 : ℝ) ^ k)⁻¹) ^ (2 : ℕ) ≤        (C * ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k)) *          (((2 : ℝ) ^ k)⁻¹) ^ (2 : ℕ) := by    exact mul_le_mul_of_nonneg_right hcountk hsq_nonneg  have hpow_ne : (2 : ℝ) ^ k ≠ 0 := pow_ne_zero k (by norm_num)  have hcancel :      (C * ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k)) *          (((2 : ℝ) ^ k)⁻¹) ^ (2 : ℕ) =        C * ((k + 1 : ℕ) : ℝ) * ((2 : ℝ)⁻¹) ^ k := by    rw [← inv_pow]    field_simp [hpow_ne]    rw [mul_assoc, ← mul_pow]    norm_num  exact hmass.trans (hcancel ▸ hmul)