One-period market no-arbitrage and risk-neutral probability: bnDiscount_positive
ProvedActuarialValuation.bnDiscount_positiveactuarial-sciencebinomial-financial-marketsformal-verification
Positive riskless accumulation and a positive future cashflow imply a positive current bond 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_bnDiscount
Formal statement
namespace ActuarialValuation theorem bnDiscount_positive (R x : ℝ) (hR : 0 < R) (hx : 0 < x) : 0 < bnDiscount R x := 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.