OAI/Probability/SKValue/Control/ControlPayoffConvex.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SKValue.controlPayoff_convexline 27 - lemma
OAI.SKValue.phi_convexline 58 - lemma
OAI.SKValue.brownian_increment_memLpline 72 - lemma
OAI.SKValue.brownian_increment_secondline 76 - lemma
OAI.SKValue.brownian_increment_abs_boundline 88 - lemma
OAI.SKValue.phi_terminal_boundline 99