Skip to content

Commit 33347ef

Browse files
committed
feat: port Probability.Martingale.Upcrossing (#5281)
1 parent dbae2f1 commit 33347ef

File tree

3 files changed

+889
-1
lines changed

3 files changed

+889
-1
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2456,6 +2456,7 @@ import Mathlib.Probability.Martingale.Basic
24562456
import Mathlib.Probability.Martingale.Centering
24572457
import Mathlib.Probability.Martingale.OptionalSampling
24582458
import Mathlib.Probability.Martingale.OptionalStopping
2459+
import Mathlib.Probability.Martingale.Upcrossing
24592460
import Mathlib.Probability.Notation
24602461
import Mathlib.Probability.ProbabilityMassFunction.Basic
24612462
import Mathlib.Probability.ProbabilityMassFunction.Constructions

0 commit comments

Comments
 (0)