比如假设有一个波动率变量，以及走不通路径的概率变量，从而对程序不同操作路径分别讨论，最终根据加权得到特定波动率下的预期收益。
- 如何落实到概率论的定理上证明正确性
- 如何和rust代码结合证明生产代码正确性。
如 果 我 们 设 置 的 执 ⾏ 价 格 等 于 远 期 价 格 ， 那 么 为 了 模 仿 该 远 期 头 ⼨ ， 初 始 的 净 贴 ⽔ 必 定 等 于 0 。 在 这 种 情 况 下 ， 看 跌 期 权 贴 ⽔ 与 看 涨 期 权 贴 ⽔ 必 定 相 等 。 看 跌 - 看 涨 期 权 平 价 我 们 可 以 通 过 下 ⾯ 这 句 话 来 概 括 这 个 论 证 ， 使 ⽤ 期 权 买 ⼈ 指 数 的 净 成 本 必 定 等 于 使 ⽤ 远 期 合约 买 ⼊ 指 数 的 净 成 本 。 如 果 在 0 时 刻 ， 我 们 签 订 ⼀ 个 远 期 多 头 头 ⼨ ， 那 么 在 到 期 ⽇ 了 时 刻 ， 我 们 就有 以 F 0,t 的 远 期 价 格 购 买 指 数 的 义 务 。 在 未 来 购 买 指 数 的 现 值 就 是 远 期 价 格 的 现 值 （ P V （ F 0,t ） ） 。 如果取而代之，我们通过在今天买入一份看涨期权并卖出一份看跌期权以保证在未来购买指数的价格，那么成本的现值就是买入看涨期权与卖出看跌期权所支付的净期权贴水（Call（K，T）- Put（K，T））加上执行价格的现值（PV(K)）。（记号“Call(K,T)”和“Put (K,T)”表示执行价格为K而离到期日还有时间T的期权贴水。）
令以上两种方法的t时刻指数购买成本相等，可以得到 PV(Fo,τ) = [Call(K,T) - Put(K,T)] + PV(K)
我们可以把其改写为 Call(K,T) - Put(K,T) = PV(Fo,τ - K) (3-1)
简单地说，执行价格的指数购买方式所产生的议价成分的现值（式（3-1）的右侧）必定被初始的净期权贴水所抵补（式（3-1）的左侧）。式（3-1）就是著名的看涨 - 看跌期权平价（put - call parity）关系，是期权中最重要的关系之一。
将以上内容形式化为 Lean4
注意给出一个计算用的函数，然后给出证明，为了证明，你需要先定义一些引理，或使用现有的 Call Put PV 的定义，然后把『令 以 上 两 种 ⽅ 法 的 1 时 刻 指 数 购 买 成 本 相 等』作为一个假设引入。注意使用 Lean4 的语法，小心不使用 Lean3 的旧语法。
Undefined widget 'supertag-form'