Kadiri.zeroHeightDyadicShellMass_le_count_inv_sq

lemma zeroHeightDyadicShellMass_le_count_inv_sq (k : ℕ) :    zeroHeightDyadicShellMass k ≤      (Nat.card {rho : NontrivialZeros // zeroHeightDyadicShell k rho} : ℝ) *        (((2 : ℝ) ^ k)⁻¹) ^ (2 : ℕ) := by  classical  haveI : Finite {rho : NontrivialZeros // zeroHeightDyadicShell k rho} :=    Set.finite_coe_iff.mpr (nontrivialZeros_dyadic_shell_finite k)  letI := Fintype.ofFinite {rho : NontrivialZeros // zeroHeightDyadicShell k rho}  unfold zeroHeightDyadicShellMass  rw [tsum_fintype]  calc    (∑ rho : {rho : NontrivialZeros // zeroHeightDyadicShell k rho},        zeroImagSquareTail rho.1)        ≤ ∑ _rho : {rho : NontrivialZeros // zeroHeightDyadicShell k rho},            (((2 : ℝ) ^ k)⁻¹) ^ (2 : ℕ) := by          exact Finset.sum_le_sum fun rho _ =>            zeroImagSquareTail_le_dyadic_inv_sq rho.2    _ = (Nat.card {rho : NontrivialZeros // zeroHeightDyadicShell k rho} : ℝ) *          (((2 : ℝ) ^ k)⁻¹) ^ (2 : ℕ) := by          simp [Nat.card_eq_fintype_card]