Prove2Me

Raising the upper barrier cannot create a hit

Proved
FinancialDerivatives.FD05.upperTouch_antitone_barrier

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

barrier-optionsfd05financial-derivatives

Every observed hit of a higher upper barrier is also a hit of any lower upper barrier.

Preamble
import Mathlib.Data.Real.Basic
import Definitions.Def_fd05_upperTouch
Formal statement
namespace FinancialDerivatives.FD05

theorem upperTouch_antitone_barrier (B₁ B₂ S : ℝ)
    (monitor : ℕ → Bool) (t : ℕ) (hB : B₁ ≤ B₂)
    (h : upperTouch B₂ S monitor t = true) :
    upperTouch B₁ S monitor t = true := 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