Construct the FD-01 state-price system from positive risk-neutral weights
Definitionfd02_toFD01PriceSystemGiven a two-state market and proof that its unique up weight q lies strictly between zero and one, construct an FD-01 FinitePriceSystem on Bool with positive Arrow-state prices q/R and (1-q)/R and discount factor 1/R. No-arbitrage implies the required two inequalities through separate theorems T12 and T13. The constructor itself does not assume that the derivative price is correct.
import Mathlib.Data.Real.Basic
import Mathlib.Data.Fintype.BigOperators
import Mathlib.Tactic.Ring
import Definitions.Def_fd01_FinitePriceSystem
import Definitions.Def_fd02_TwoStateMarket
import Definitions.Def_fd02_riskNeutralUp
namespace FinancialDerivatives.FD02
/-- Positive two-state martingale weights construct the FD-01 price system. -/
noncomputable def toFD01PriceSystem (m : TwoStateMarket)
(hq0 : 0 < riskNeutralUp m) (hq1 : riskNeutralUp m < 1) :
FinancialDerivatives.FD01.FinitePriceSystem Bool where
statePrice := fun ω => match ω with
| true => riskNeutralUp m / m.growth
| false => (1 - riskNeutralUp m) / m.growth
statePrice_nonneg := by
intro ω
cases ω with
| false =>
exact div_nonneg (sub_nonneg.mpr (le_of_lt hq1)) (le_of_lt m.growth_pos)
| true =>
exact div_nonneg (le_of_lt hq0) (le_of_lt m.growth_pos)
discount := 1 / m.growth
discount_pos := div_pos zero_lt_one m.growth_pos
statePrice_sum := by
simp only [Fintype.sum_bool]
ring
end FinancialDerivatives.FD02Read-back
What the Lean code literally says, in plain math · GPT-6
For any market with real spot , bank growth , and stock factors and , if additionally and , the defined construction gives a finite state-price system on the two Boolean states with state price for true and for false, and discount factor . These state prices are nonnegative (indeed positive), the discount factor is positive, and the sum of the two state prices equals ; the returned object includes proofs of those conditions.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.