Alive contract settles its terminal reward
ProvedFinancialDerivatives.FD05.upperAbsorbingValue_alive_maturitybarrier-optionsfd05financial-derivatives
At alive maturity, an untriggered upper-barrier contract pays precisely the specified terminal reward.
Preamble
import Mathlib.Data.Real.Basic import Definitions.Def_fd05_upperAbsorbingValue import Definitions.Def_fd05_upperTouch
Formal statement
namespace FinancialDerivatives.FD05
open FinancialDerivatives.FD03
theorem upperAbsorbingValue_alive_maturity (m : BinomialMarket)
(B : ℝ) (monitor : ℕ → Bool) (g : ℝ → ℝ)
(t : ℕ) (S : ℝ) (h : upperTouch B S monitor t = false) :
upperAbsorbingValue m B monitor g 0 t S false = g S := by sorry
end FinancialDerivatives.FD05Source
Wilmott, Howison and Dewynne (1995), The Mathematics of Financial Derivatives, Chapter 12, pp. 206–212. Rigorous finite-binomial first-hit analogue.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.