Skip to content

Commit eff781e

Browse files
committed
feat: port Probability.Martingale.Convergence (#5283)
1 parent 33347ef commit eff781e

File tree

2 files changed

+471
-0
lines changed

2 files changed

+471
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2454,6 +2454,7 @@ import Mathlib.Probability.Kernel.MeasurableIntegral
24542454
import Mathlib.Probability.Kernel.WithDensity
24552455
import Mathlib.Probability.Martingale.Basic
24562456
import Mathlib.Probability.Martingale.Centering
2457+
import Mathlib.Probability.Martingale.Convergence
24572458
import Mathlib.Probability.Martingale.OptionalSampling
24582459
import Mathlib.Probability.Martingale.OptionalStopping
24592460
import Mathlib.Probability.Martingale.Upcrossing

0 commit comments

Comments
 (0)