How to write finite sums with infinite index types

Big sum

import data.pfun

open nat

class bounded (p : ℕ → Prop) :=
  (ubound : ℕ)
  (only_below : ∀ i > ubound, ¬ p i)

export bounded (only_below)

instance bounded_lt {k : ℕ} : bounded (λ n, n < k) :=
  { ubound := k
  , only_below := by intros ; simp [not_lt_of_gt,*] }

instance bounded_le {k : ℕ} : bounded (λ n, n ≤ k) :=
  { ubound := k
  , only_below := by intros ; simp [not_le_of_gt,*] }

instance bounded_and {p q : ℕ → Prop} [bounded p] : bounded (λ n, p n ∧ q n) :=
  { ubound := bounded.ubound p
  , only_below := by { intros, apply mt and.left, apply only_below _ H, }  }

instance bounded_and' {p q : ℕ → Prop} [bounded q] : bounded (λ n, p n ∧ q n) :=
  { ubound := bounded.ubound q
  , only_below := by { intros, apply mt and.right, apply only_below _ H, }  }

instance bounded_or {p q : ℕ → Prop} [bounded p] [bounded q] : bounded (λ n, p n ∨ q n) :=
  { ubound := max (bounded.ubound p) (bounded.ubound q)
  , only_below :=
    by { intros,
         apply not_or
         ; apply only_below
         ; apply lt_of_le_of_lt _ H
         ; simp [le_max_left,le_max_right], }  }


def roption.mk' {α} (p : Prop) (x : α) := roption.mk p $ λ _, x

infix ` ▻ `:30 := roption.mk'

variables {α : Type*}

instance decidable_dom {p : ℕ → Prop} [dec : decidable_pred p] {f : ℕ → α} :
  decidable_pred (pfun.dom (λ i, p i ▻ f i)) :=
dec

instance bounded_dom {p : ℕ → Prop} [bounded p] {f : ℕ → α} :
  bounded (pfun.dom (λ i, p i ▻ f i)) :=
 { ubound := bounded.ubound p
 , only_below := only_below }

variables [has_zero α] [has_add α]

def sum_aux (f : ℕ →. α) [bounded f.dom] [decidable_pred f.dom] : ℕ → α
 | 0 := 0
 | (succ n) :=
sum_aux n +
if h : n ∈ f.dom
  then (f n).get h
  else 0

def sum' (f : ℕ →. α) [bounded f.dom] [decidable_pred f.dom] : α :=
sum_aux f (succ $ bounded.ubound f.dom)

#check @sum' ℕ
#check sum' (λ i, i < 10 ▻ i^2)

notation `ΣΣ ` binder `, ` r:(scoped p, p) := sum' r

def even (n : ℕ) : Prop := n % 2 = 0

#check ΣΣ i, i ≥ 3 ∧ i < 21 ▻ i^2