Prove2Me

FD-04 monitored-list touch equals FD-05 first-hit event

Proved
FinancialDerivatives.FD05.FD04_upperBarrierTouched_iff_firstUpperHit

by WillR · Oct 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

barrier-optionsfd05financial-derivatives

FD-04's Boolean any-touch predicate on observed stock prices is equivalent to FD-05's finite first-hit time being at or before maturity.

Preamble
import Mathlib.Data.Real.Basic
import Definitions.Def_fd04_upperBarrierTouched
import Definitions.Def_fd05_monitoredSpots
import Definitions.Def_fd05_firstUpperHit
Formal statement
namespace FinancialDerivatives.FD05
open FinancialDerivatives.FD03

open FinancialDerivatives.FD04

theorem FD04_upperBarrierTouched_iff_firstUpperHit
    (m : BinomialMarket) (N : ℕ) (B : ℝ)
    (monitor : ℕ → Bool) (steps : List Bool) :
    upperBarrierTouched B (monitoredSpots m N monitor steps) = true ↔
      firstUpperHit m N B monitor steps ≤ N := by sorry

end FinancialDerivatives.FD05
Source
Wilmott, Howison and Dewynne (1995), The Mathematics of Financial Derivatives, Chapter 12, pp. 206–212. Rigorous finite-binomial first-hit analogue.
Human review

  • Endorsed by Shuze Chen · Oct 28, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 28, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph