One-period market no-arbitrage and risk-neutral probability: bnProb_zero_at_down
ProvedActuarialValuation.bnProb_zero_at_downactuarial-sciencebinomial-financial-marketsformal-verification
At the lower gross return boundary, the up-state martingale probability collapses to zero.
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_bnRiskNeutralProb
Formal statement
namespace ActuarialValuation theorem bnProb_zero_at_down (u d : ℝ) (hud : u ≠ d) : bnRiskNeutralProb u d d = 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.