Exact Boolean upper-touch characterisation
ProvedFinancialDerivatives.FD05.upperTouch_iffbarrier-optionsfd05financial-derivatives
An upper touch occurs if and only if this time is monitored and the observed stock is at or above the barrier.
Preamble
import Mathlib.Data.Real.Basic import Definitions.Def_fd05_upperTouch
Formal statement
namespace FinancialDerivatives.FD05
theorem upperTouch_iff (B S : ℝ) (monitor : ℕ → Bool) (t : ℕ) :
upperTouch B S monitor t = true ↔
monitor t = true ∧ B ≤ 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.