OAI/Probability/FreeIsing/Martingales/ContinuousMartingaleVariation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.ContinuousMartingaleVariation.tendsto_integral_weighted_error_sq line 18
2. theorem OAI.Problem367.ContinuousMartingaleVariation.tendsto_integral_weighted_error_sq_of_monotone line 66