Doob's upcrossing inequality for Countable and NNReal - #361

Open

WojciechCzernous wants to merge 10 commits into

RemyDegenne:masterfrom

WojciechCzernous:MCT-Wojciech

Commits on Apr 27, 2026

refactor: simplify coercion handling for upcrossings and introduce Finset.orderBotOfBotMem helper

WojciechCzernous
and
Copilot
committed
34dd104
refactor: remove unused strict monotonicity lemmas in Upcrossing.lean

WojciechCzernous
and
Copilot
committed
261c541
refactor: simplify strict monotonicity handling in upcrossingSequenceENat theorems

WojciechCzernous
and
Copilot
committed
44a77e2
refactor: streamline simp usage in upperCrossingTimeLT lemmas

WojciechCzernous
and
Copilot
committed
676e028
refactor: enhance documentation for Doob's upcrossing inequality and proof outline

WojciechCzernous
and
Copilot
committed
c22261b