Explicit first-touch discounted rebate sum

import Mathlib.Data.Real.Basic
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Fintype.Pi
import Mathlib.Algebra.BigOperators.Group.Finset.Defs
import Definitions.Def_fd03_BinomialMarket
import Definitions.Def_fd05_firstUpperHit
import Definitions.Def_fd05_historyWeight

namespace FinancialDerivatives.FD05
open FinancialDerivatives.FD03

/-- Discount each rebate from its actual monitored first-hit time. -/
noncomputable def discountedFirstHitRebatePrice (m : BinomialMarket)
    (N : ℕ) (B : ℝ) (monitor : ℕ → Bool) (Z : ℝ) : ℝ := by
  classical
  exact Finset.univ.sum (fun ω : Fin N → Bool =>
    historyWeight m (List.ofFn ω) *
      (if firstUpperHit m N B monitor (List.ofFn ω) ≤ N
       then Z / m.growth ^ (firstUpperHit m N B monitor (List.ofFn ω))
       else 0))

end FinancialDerivatives.FD05