Brownian Motion Marginal Law

Proved

LevyStochCalc.Brownian.BrownianMotion.hasLaw_eval_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concavevendored-levystochcalc

This is a marginal-law statement for a real Brownian motion.

Let $(\Omega,\mathcal F,P)$ be a probability space, let $W$ be a BrownianMotion under $P$ , and let $t\in[0,\infty)$ be represented as an NNReal. Then the random variable $\omega\mapsto W_t(\omega)$ has the centered Gaussian law with variance $t$ :

\operatorname{Law}_P(W_t)=\mathcal N(0,t).

Here gaussianReal 0 t denotes the Gaussian probability measure with mean $0$ and variance parameter $t$ . The result includes the case $t=0$ , where the law is concentrated at $0$ .

This provides the one-time marginal required when relating the library's Brownian-motion construction to Mathlib's Brownian-motion predicates.

Original Lean declaration header

Within namespace LevyStochCalc.Brownian.BrownianMotion. Shown in its original module context. Proof omitted.

theorem hasLaw_eval (W : BrownianMotion P) (t : ℝ≥0) :
    HasLaw (W.W (t : ℝ)) (gaussianReal 0 t) P

Module navigation

Module: LevyStochCalc/Brownian/MathlibBridge.

Definition modules: LevyStochCalc/Brownian/Construction.

Previous: iIndep_of_indep_biSup_lt · Next: hasIndepIncrements.

Source excerpt, lines 68–69 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_MathlibBridge

/-
Copyright (c) 2026 Christian Garry. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Garry
-/
-- Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (upstream path LevyStochCalc/Brownian/MathlibBridge.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory
open scoped NNReal
universe u
variable {Ω : Type u} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]

Formal statement


theorem LevyStochCalc.Brownian.BrownianMotion.hasLaw_eval_readable (W : BrownianMotion P) (t : ℝ≥0) :
    HasLaw (W.W (t : ℝ)) (gaussianReal 0 t) P := by sorry

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Brownian/MathlibBridge.lean#L67-L85 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Brownian.MathlibBridge`, declaration `LevyStochCalc.Brownian.BrownianMotion.hasLaw_eval`; the repository is private at upload time). Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (Apache-2.0; upstream copyright notice retained in the Lean text).

View graph