Prove2Me

Unique arbitrage-free price of an upper barrier claim

Proved
FinancialDerivatives.FD05.barrier_claim_unique_no_arbitrage_price

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

barrier-optionsfd05financial-derivatives

The discounted first-hit path price is exactly the quotation that avoids arbitrage when an upper barrier claim is traded alongside the binomial stock and bank.

Preamble
import Mathlib.Data.Real.Basic
import Definitions.Def_fd03_quotedClaimArbitrage
import Definitions.Def_fd05_upperKnockOutTree
import Definitions.Def_fd05_discountedSurvivalPathPrice
Formal statement
namespace FinancialDerivatives.FD05
open FinancialDerivatives.FD03

theorem barrier_claim_unique_no_arbitrage_price (m : BinomialMarket)
    (N : ℕ) (B : ℝ) (monitor : ℕ → Bool)
    (g : ℝ → ℝ) (quote : ℝ) :
    ¬ quotedClaimArbitrage m N m.initialSpot
        (upperKnockOutTree m B monitor g N 0 m.initialSpot false) quote ↔
      quote = 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