Explicit self-financing hedge and European option replication: bnPut_zero_above_strike
ProvedActuarialValuation.bnPut_zero_above_strikeactuarial-sciencebinomial-financial-marketsformal-verification
An at-the-money or out-of-the-money put has zero exercise value.
Mathematical relation:
Original derived theorem target; the Lean statement gives the exact conditions and result.
Preamble
import Mathlib.Data.Real.Basic import Mathlib.Algebra.BigOperators.Group.Finset.Basic import Definitions.Def_actuarial_bnPut
Formal statement
namespace ActuarialValuation theorem bnPut_zero_above_strike (s k : ℝ) (h : k ≤ s) : bnPut s k = 0 := by sorry end ActuarialValuation
Source
Original derived actuarial mathematics inspired by Promislow (2015), chapters 20.1–20.11, published book reference https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/; supporting published actuarial reference https://doi.org/10.1016/0304-405X(79)90015-1. The proposed model is rooted in Promislow chapter 20.1–20.11. The target Lean identity is an original derivation, not a verbatim published result. Published source page 339 gives the thematic chapter context, rather than an exact statement of this new formal theorem.
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.