Cover Image

Formalization of Brownian motion in Lean

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Degenne, Rémy, Ledvinka, David, Marion, Etienne, Pfaffelhuber, Peter
Format:	Preprint
Published:	2025
Subjects:	Probability
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Markov kernels in Mathlib's probability library
by: Degenne, Rémy
Published: (2025)

Large-scale behavior of the partial duplication random graph
by: Hermann, Felix, et al.
Published: (2014)

The partial duplication random graph with edge deletion
by: Hermann, Felix, et al.
Published: (2019)

A Formalization of the Ionescu-Tulcea Theorem in Mathlib
by: Marion, Etienne
Published: (2025)

Optimal strategies in the all-heads coin game
by: Pfaffelhuber, Peter
Published: (2026)

On the distribution of the time-integral of the geometric Brownian motion
by: Nandori, Peter, et al.
Published: (2022)

Additive martingales of the branching Brownian motion
by: Chataignier, Louis
Published: (2024)

On the slow points of fractional Brownian motion
by: Khoshnevisan, Davar, et al.
Published: (2026)

Wellposedness and averaging principle for conditional distribution dependent SDEs driven by standard Brownian motions and fractional Brownian motions
by: Tan, Li, et al.
Published: (2025)

Quasi-stationarity of the Dyson Brownian motion with collisions
by: Guillin, Arnaud, et al.
Published: (2025)

Parameter estimation of integrated fractional Brownian motion
by: Mastrogiovanni, Marco, et al.
Published: (2025)

Edge homogenization of Dyson Brownian motion and applications
by: Landon, Benjamin, et al.
Published: (2025)

Uniform in time modulus of continuity of Brownian motion
by: Chevallier, Julien
Published: (2023)

Markov processes forced on a subspace by a large drift, with applications to population genetics
by: Adeosun, Samuel Ayomide, et al.
Published: (2026)

Tanaka formula for SDEs driven by fractional Brownian motion
by: Sottinen, Tommi, et al.
Published: (2025)

Time reversal of reflected Brownian motion with Poissonian resetting
by: Colantoni, Fausto, et al.
Published: (2025)

Fine properties of fractional Brownian motions on Wiener space
by: Li, Jiawei, et al.
Published: (2018)

On the tightness of the maximum of branching Brownian motion in random environment
by: Černý, Jiří, et al.
Published: (2022)

Invariance properties of Brownian motion via Lie's symmetries
by: Dehò, Susanna, et al.
Published: (2026)

Intermittency of geometric Brownian motion on $ \textbf{SL}(n) $
by: Kuzgun, Sefika, et al.
Published: (2026)

High-dimensional limits for reflected Brownian motion in the orthant
by: Atar, Rami
Published: (2026)

Fluctuations of the additive martingales related to super-Brownian motion
by: Yang, Ting
Published: (2024)

$p$-Brownian motion and the $p$-Laplacian
by: Barbu, Viorel, et al.
Published: (2024)

Resetting Dyson Brownian motion
by: Biroli, Marco, et al.
Published: (2025)

On the theory of relativistic Brownian motion
by: Kurianovich, E. A., et al.
Published: (2024)

Extension of a theorem of Wschebor to free and matrix Brownian motions
by: Donati-Martin, Catherine, et al.
Published: (2025)

Brownian motion and stochastic areas on complex full flag manifolds
by: Baudoin, Fabrice, et al.
Published: (2025)

Stochastic Volterra integral equations driven by $ G $-Brownian motion
by: Zhao, Bingru, et al.
Published: (2025)

Quadratic BSDEs with double constraints driven by G-Brownian motion
by: He, Wei, et al.
Published: (2025)

Birth-death processes are time-changed Feller's Brownian motions
by: Li, Liping
Published: (2024)

A Mimicking Theorem for processes driven by fractional Brownian motion
by: Hu, Kevin, et al.
Published: (2024)

Small deviation for the mutual intersection local time of Brownian motions
by: Chen, Xia, et al.
Published: (2024)

Brownian motion conditioned to have restricted $L_2$-norm
by: Aurzada, Frank, et al.
Published: (2023)

Asymptotic behaviors of subcritical branching killed Brownian motion with drift
by: Hou, Haojie, et al.
Published: (2024)

Long range voter models and dynamical fractional Brownian motion
by: Drogin, Reuben
Published: (2023)

Lévy's martingale characterization and reflection principle of $G$-Brownian motion
by: Hu, Mingshang, et al.
Published: (2018)

Large deviation principle for fractional Brownian motion with respect to capacity
by: Li, Jiawei, et al.
Published: (2018)

Large time behaviour for the semigroup of the kinetic Brownian motion in the plane
by: Bénéfice, Magalie, et al.
Published: (2026)

Markov branching processes with disasters: extinction, survival and duality to p-jump processes
by: Hermann, F., et al.
Published: (2018)

Maximal inequalities for bifractional Brownian motion
by: Rao, B. L. S. Prakasa
Published: (2024)