Prove2Me

Self-financing hedge attaining upper barrier first-hit value

Proved
FinancialDerivatives.FD05.barrier_claim_replicating_hedge

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

barrier-optionsfd05financial-derivatives

A full-history upper knock-out claim can be replicated by a self-financing stock-bank hedge whose initial capital is the explicit discounted first-hit valuation.

Preamble
import Mathlib.Data.Real.Basic
import Definitions.Def_fd03_HedgeTree
import Definitions.Def_fd03_SelfFinancing
import Definitions.Def_fd03_hedgeTerminalPays
import Definitions.Def_fd03_hedgeWealth
import Definitions.Def_fd05_upperKnockOutTree
import Definitions.Def_fd05_discountedSurvivalPathPrice
Formal statement
namespace FinancialDerivatives.FD05
open FinancialDerivatives.FD03

theorem barrier_claim_replicating_hedge (m : BinomialMarket)
    (N : ℕ) (B : ℝ) (monitor : ℕ → Bool) (g : ℝ → ℝ) :
    ∃ hedge : HedgeTree N,
      SelfFinancing m N m.initialSpot hedge ∧
      hedgeTerminalPays N hedge (upperKnockOutTree m B monitor g N 0 m.initialSpot false) ∧
      hedgeWealth m N m.initialSpot hedge =
        discountedSurvivalPathPrice m N B monitor 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