Prove2Me

Pathwise monotonicity when monitoring dates are added

Proved
FinancialDerivatives.FD05.upperKnockOutTree_antitone_monitor

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

barrier-optionsfd05financial-derivatives

Adding observation dates can only extinguish additional histories of a nonnegative upper knock-out claim.

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

theorem upperKnockOutTree_antitone_monitor (m : BinomialMarket)
    (N : ℕ) (B : ℝ) (M₁ M₂ : ℕ → Bool) (g : ℝ → ℝ)
    (hM : ∀ t : ℕ, M₁ t = true → M₂ t = true)
    (hg : ∀ S : ℝ, 0 ≤ g S) :
    payoffTreeLe N
      (upperKnockOutTree m B M₂ g N 0 m.initialSpot false)
      (upperKnockOutTree m B M₁ g N 0 m.initialSpot false) := 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