If it looks like a duck...

Stream: Brownian motion

[Rémy Degenne]

We will soon have a completely formalized definition of an object that we call Brownian motion on $\mathbb{R}_+$, and we have some of its properties. How do we make sure that it is actually a Brownian motion?
So what characterization should we use, and what properties are we missing for that characterization?

[Rémy Degenne]

It would be nice to show that our Brownian has independent increments.

[Peter Pfaffelhuber]

We know that $(X_s, X_t)$ for $0 \leq s < t$ has a multinomial normal distribution with expectation 0 and covariance matrix $\left(\begin{matrix} s & s \\ s & t\end{matrix}\right)$. Let us write $\left( \begin{matrix}X_s \\ X_t - X_s \end{matrix}\right) = \left( \begin{matrix} 1 & 0 \\ -1 & 1 \end{matrix}\right) \left(\begin{matrix}X_s \\ X_t \end{matrix}\right)$. By some theorem which we have already shown this means that $(X_s, X_t - X_s)$ as a linear transformation of a multinomial distribution is again multinomial norman with expectation 0 and covariance $\left( \begin{matrix}1 & 0 \\ -1 & 1 \end{matrix} \right)\left(\begin{matrix} s & s \\ s & t\end{matrix}\right)\left( \begin{matrix}1 & -1 \\ 0 & 1 \end{matrix} \right) = \left( \begin{matrix}s & 0 \\ 0 & t-s \end{matrix} \right)$. This shows that $X_s$ and $X_t - X_s$ are uncorrelated, hence independent.

[Peter Pfaffelhuber]

For more than two timepoints it may be more involved...

[Peter Pfaffelhuber]

From the result on two timepoints, it should be straight-forward to show that Brownian Motion is a martingale: $E[X_t | \mathcal F_s] = E[X_s - X_t - X_s | \mathcal F_s] = X_s + E[X_t - X_s | F_s] = X_s + E[X_t - X_s] = X_s.$

[Peter Pfaffelhuber]

Also, $E[X_t^2 - t - X_s^2 + s| \mathcal F_s] = E[(X_t - X_s)^2 + 2X_s(X_t - X_s) - t + s | \mathcal F_s] = E[(X_t - X_s)^2] + 2 X_s E[X_t - X_s] - (t - s) = 0$, showing that $(X_t^2 - t)_{t\geq 0}$ is a martingale.

[Etienne Marion]

Update on this: In #134 (quite messy right now), I defined an IsBrownian X P predicate. It means that under P, X has the right finite-dimensional distributions, and X is almost-surely continuous. I managed to prove that an almost-surely continuous process with independent increments such that for any t, X t has law gaussianReal 0 t is Brownian in the sense of this predicate.

[Rémy Degenne]

Nice! Of course at some point we will want to know that independent increments and continuous paths imply that the process has Gaussian laws, such that those conditions are enough to be Brownian, but proving that fact requires the CLT, which we don't have yet.

[Joris van Winden]

Hello! I am a grad student in analysis/probability (will defend soon) and am interested to contribute to the project.

As a warm-up, I formalized a proof which states that a Brownian motion is a martingale (with respect to its natural filtration). Would it be worthwhile to turn this into a PR?

[Rémy Degenne]

Yes, please open a PR! This is a nice result, that we definitely would like to have in the project.

[Joris van Winden]

Here is the PR #359

There was no definition of a 'filtered Brownian motion' or 'F-Brownian motion' yet, but since this definition is common in the literature (see e.g. Kallenberg p. 305) I added a class for this (and proved that a Brownian motion is filtered w.r.t its natural filtration). However, I am not sure if this is actually the best way to encode this fact.

[Joris van Winden]

Would there be an interest in having the law of the iterated logarithm (for Brownian motion) formalized in the project? I have just managed to prove the upper bound (assuming the appropriate tail bound for the supremum of the BM) by following Kallenberg Theorem 14.18.

[David Ledvinka]

Yes this would be good! I actually mentioned this as a potential next step in my Lean Together talk on the project.

[Joris van Winden]

Okay, then I will start working on the lower bound. Will the talk be uploaded online somewhere?

[Rémy Degenne]

On youtube, next week

[Joris van Winden]

I have now fully formalized the law of the iterated logarithm, as given by the following statement:

variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsProbabilityMeasure P]
variable (X : ℝ≥0 → Ω → ℝ) [hX : ProbabilityTheory.IsBrownian X P]

lemma IsBrownian.iterated_logarithm (h_meas : ∀ t, Measurable (X t)) :
    ∀ᵐ ω ∂P, limsup (fun t ↦ (X t ω) / (2 * t * (t : ℝ).log.log).sqrt : ℝ≥0 → EReal) atTop = 1

The proof is not entirely sorry-free since it relies on the following unproven lemmas:

lemma IsBrownian.reflection {X t} {c : ℝ} (hX : IsBrownian X P) (ht : 0 < t) (hc : 0 ≤ c)
    : P.real {ω | c ≤ ⨆ s ≤ t, (X s ω).toEReal} = 2 * P.real {ω | c ≤ X t ω} :=
  sorry -- needs strong Markov property

lemma IsStandardGaussian.tail {X} (hX : HasLaw X (gaussianReal 0 1) P) :
    Asymptotics.IsEquivalent atTop (fun x ↦ P.real {ω | x ≤ X ω})
    (fun x ↦ 1 / x * (-1/2 * x ^ 2).exp) := by
  sorry -- todo

The first lemma is the law of reflection, which is a direct consequence of the strong Markov property (which is not in the project yet). The second lemma is a classical asymptotic for the standard Gaussian cdf, which I could not locate in mathlib.

If there is interest in having these statements included in the project, I can start cleaning up the proof (currently it is ~300 lines) and eventually make a PR.

[Joris van Winden]

Using the time inversion formula, I think the non-differentiability of Brownian motion can now be deduced as a consequence (although this certainly does not require the full strength of the theorem).