MAIN GOAL: absorbing, path-sum and knock-in/out valuation identities

Proved

FinancialDerivatives.FD05.barrier_first_hit_valuation

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

barrier-optionsfd05financial-derivatives

The central theorem derives a first-hit absorbing recursion, its discounted full-path expectation and the exact price complementarity of matched knock-in and knock-out contracts.

Preamble

import Mathlib.Data.Real.Basic
import Definitions.Def_fd05_upperKnockOutTree
import Definitions.Def_fd05_upperKnockInTree
import Definitions.Def_fd05_upperAbsorbingValue
import Definitions.Def_fd05_discountedSurvivalPathPrice
import Definitions.Def_fd05_vanillaTerminalTree
import Definitions.Def_fd03_europeanValue

Formal statement

namespace FinancialDerivatives.FD05
open FinancialDerivatives.FD03

theorem barrier_first_hit_valuation (m : BinomialMarket) (N : ℕ)
    (B : ℝ) (monitor : ℕ → Bool) (g : ℝ → ℝ) :
    (upperAbsorbingValue m B monitor g N 0 m.initialSpot false =
      europeanValue m N
        (upperKnockOutTree m B monitor g N 0 m.initialSpot false)) ∧
    (europeanValue m N
      (upperKnockOutTree m B monitor g N 0 m.initialSpot false) =
      discountedSurvivalPathPrice m N B monitor g) ∧
    (europeanValue m N
      (upperKnockInTree m B monitor g N 0 m.initialSpot false) +
      europeanValue m N
        (upperKnockOutTree m B monitor g N 0 m.initialSpot false) =
      europeanValue m N (vanillaTerminalTree m N g)) := 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