Explicit discounted knock-out path-sum price

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_historySpot
import Definitions.Def_fd05_firstUpperHit
import Definitions.Def_fd05_historyWeight

namespace FinancialDerivatives.FD05
open FinancialDerivatives.FD03

/-- Independent finite-path expectation with zero value on hit histories. -/
noncomputable def discountedSurvivalPathPrice (m : BinomialMarket) (N : ℕ)
    (B : ℝ) (monitor : ℕ → Bool) (g : ℝ → ℝ) : ℝ := by
  classical
  exact (m.growth ^ N)⁻¹ *
    Finset.univ.sum (fun ω : Fin N → Bool =>
      historyWeight m (List.ofFn ω) *
        (if N < firstUpperHit m N B monitor (List.ofFn ω)
         then g (historySpot m (List.ofFn ω)) else 0))

end FinancialDerivatives.FD05