Maturity-equivalent payoff for an immediate first-hit rebate

import Mathlib.Data.Real.Basic
import Definitions.Def_fd03_BinomialMarket
import Definitions.Def_fd03_PayoffTree
import Definitions.Def_fd03_constantPayoffTree
import Definitions.Def_fd05_upperTouch

namespace FinancialDerivatives.FD05
open FinancialDerivatives.FD03

/-- On first touch at t, carry Z forward by the remaining bank growth. -/
noncomputable def upperFirstHitRebateTree (m : BinomialMarket) (B : ℝ)
    (monitor : ℕ → Bool) (Z : ℝ) :
    (n : ℕ) → ℕ → ℝ → PayoffTree n
  | 0, t, S =>
      .leaf (if upperTouch B S monitor t then Z else 0)
  | n + 1, t, S =>
      if upperTouch B S monitor t
      then constantPayoffTree (n + 1) (Z * m.growth ^ (n + 1))
      else .branch
        (upperFirstHitRebateTree m B monitor Z n (t + 1) (S * m.up))
        (upperFirstHitRebateTree m B monitor Z n (t + 1) (S * m.down))

end FinancialDerivatives.FD05