将期货交易盈利预期表示为公式,并用Lean证明

林一二2024年06月05日 14:05

比如假设有一个波动率变量,以及走不通路径的概率变量,从而对程序不同操作路径分别讨论,最终根据加权得到特定波动率下的预期收益。

  1. 如何落实到概率论的定理上证明正确性
  2. 如何和rust代码结合证明生产代码正确性。

学Lean 我的求知欲

Undefined widget 'supertag-form'

Code
比如假设有一个波动率变量,以及走不通路径的概率变量,从而对程序不同操作路径分别讨论,最终根据加权得到特定波动率下的预期收益。

# 如何落实到概率论的定理上证明正确性
# 如何和rust代码结合证明生产代码正确性。