Skip to content

Doob's upcrossing inequality for Countable and NNReal #361

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
WojciechCzernous wants to merge 10 commits into
base: master
Choose a base branch
from
Open

Doob's upcrossing inequality for Countable and NNReal #361

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
f440802
upcrossing inequality for Countable and NNReal (squashed)
WojciechCzernous Apr 24, 2026
0b2a467
fix: Adapted → StronglyAdapted after Mathlib rename (2026-01-13)
WojciechCzernous Apr 24, 2026
fbd0deb
style: clear all warnings in Upcrossing.lean
WojciechCzernous Apr 24, 2026
a590a2d
fix: convert to module/public import format
WojciechCzernous Apr 24, 2026
d0a81c1
fix: expose Upcrossing declarations in module mode
WojciechCzernous Apr 24, 2026
34dd104
refactor: simplify coercion handling for upcrossings and introduce Fi…
WojciechCzernous Apr 27, 2026
261c541
refactor: remove unused strict monotonicity lemmas in Upcrossing.lean
WojciechCzernous Apr 27, 2026
44a77e2
refactor: simplify strict monotonicity handling in upcrossingSequence…
WojciechCzernous Apr 27, 2026
676e028
refactor: streamline simp usage in upperCrossingTimeLT lemmas
WojciechCzernous Apr 27, 2026
c22261b
refactor: enhance documentation for Doob's upcrossing inequality and …
WojciechCzernous Apr 27, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions BrownianMotion.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,5 +62,6 @@ public import BrownianMotion.StochasticIntegral.QuadraticVariation
public import BrownianMotion.StochasticIntegral.SimpleProcess
public import BrownianMotion.StochasticIntegral.SquareIntegrable
public import BrownianMotion.StochasticIntegral.UniformIntegrable
public import BrownianMotion.StochasticIntegral.Upcrossing
public import BrownianMotion.Verso.Brownian
public import BrownianMotion.Verso.Processes
Loading
Loading