Moser Decay Ratio sum le half dim

theorem moserDecayRatio_sum_le_half_dim    (hd : 2 < (d : ℝ)) (n : ℕ) :    Finset.sum (Finset.range n) (fun i => moserDecayRatio d ^ i) ≤ (d : ℝ) / 2 := by  have hq_nonneg : 0 ≤ moserDecayRatio d :=    moserDecayRatio_nonneg (d := d) hd  have hq_lt_one : moserDecayRatio d < 1 :=    moserDecayRatio_lt_one (d := d) hd  have hsumm : Summable (fun i : ℕ => moserDecayRatio d ^ i) :=    summable_geometric_of_lt_one hq_nonneg hq_lt_one  have hsum_le :      Finset.sum (Finset.range n) (fun i => moserDecayRatio d ^ i) ≤        ∑' i : ℕ, moserDecayRatio d ^ i := by    exact hsumm.sum_le_tsum (s := Finset.range n) (by      intro i hi      exact pow_nonneg hq_nonneg i)  refine hsum_le.trans_eq ?_  rw [tsum_geometric_of_lt_one hq_nonneg hq_lt_one, moserDecayRatio]  have hd_ne : (d : ℝ) ≠ 0 := by    exact_mod_cast (NeZero.ne d)  field_simp [hd_ne]  ring