Brownian motion preprint

Stream: Brownian motion

[Rémy Degenne]

The preprint about the formalization of Brownian motion is now online: https://arxiv.org/abs/2511.20118

[Sébastien Gouëzel]

Rémy Degenne said:

The preprint about the formalization of Brownian motion is now online: https://arxiv.org/abs/2511.20118

Page 24, Line 1, $(X_t, X_t)$ should be $(X_s, X_t)$.

[Rémy Degenne]

Thanks!

[Sébastien Gouëzel]

Do you really need metric instead of pseudo-metric in the second part of Theorem 4.20? I thought a recent discussion on Zulip showed it was not necessary?

[Rémy Degenne]

To get a modification in the sense of equality, you need it. Not to get a modification in the sense of distance zero. We did not add that discussion to the paper, but perhaps we should.

[Notification Bot]

6 messages were moved here from #Brownian motion > Status of the project by Rémy Degenne.

[Rémy Degenne]

And I should finish my PR implementing that.

[Sébastien Gouëzel]

Can't you get a modification in the sense of equality in the following way? You start from X_t, you modify it to X'_t which is Hölder, and for all t you have dist (X_t) (X'_t) = 0 with probability one. Then define Y_t to be equal to X_t if dist (X_t) (X'_t) = 0, and to X'_t otherwise. You have dist Y_t X'_t = 0 everywhere, so Y_t is Hölder continuous as X'_t is, but moreover for each t you have Y_t = X_t a.e. Maybe there's an issue with measurability?

[Rémy Degenne]

That works. There is no measurability issue. We definitely need to update that preprint then.

import Mathlib

open MeasureTheory

lemma exists_modification_of_edist_modification {T Ω E : Type*} {mΩ : MeasurableSpace Ω}
    {P : Measure Ω} [PseudoEMetricSpace E] [MeasurableSpace E] [BorelSpace E]
    {X Y : T → Ω → E} (hXY : ∀ t, Measurable[_, borel (E × E)] (fun ω ↦ (X t ω, Y t ω)))
    (h_edist : ∀ t, ∀ᵐ ω ∂P, edist (X t ω) (Y t ω) = 0) :
    ∃ Z : T → Ω → E, (∀ t, Measurable (Z t)) ∧ (∀ t ω, edist (Z t ω) (Y t ω) = 0) ∧
      ∀ t, X t =ᵐ[P] Z t := by
  let A t := {ω | edist (X t ω) (Y t ω) = 0}
  have hA_meas t : MeasurableSet (A t) := by
    borelize (E × E)
    refine MeasurableSet.preimage (measurableSet_singleton 0) ?_
    refine StronglyMeasurable.measurable ?_
    exact continuous_edist.stronglyMeasurable.comp_measurable (hXY t)
  let Z t ω := if ω ∈ A t then X t ω else Y t ω
  have hZ_meas t : Measurable (Z t) := by
    borelize E
    refine Measurable.ite (hA_meas t) ?_ ?_
    · exact (measurable_fst.mono prod_le_borel_prod le_rfl).comp (hXY t)
    · exact (measurable_snd.mono prod_le_borel_prod le_rfl).comp (hXY t)
  refine ⟨Z, hZ_meas, fun t ω ↦ ?_, fun t ↦ ?_⟩
  · simp only [Set.mem_setOf_eq, Z, A]
    split_ifs with hω
    · simp [hω]
    · simp
  · filter_upwards [h_edist t] with ω hω
    simp [Z, A, hω]

The lemma requires measurability of pairs, but we have that in our case.

[Sébastien Gouëzel]

I'm not even sure you need the measurability of pairs: in the previous discussion, I argued that if F is measurable and G satisfies dist (F x) (G x) = 0 everywhere, then G is measurable. You could apply that to F = Y t and G = Z t.

[Rémy Degenne]

I'm using the measurability of pairs to get measurability of ω ↦ edist (X t ω) (Y t ω), for measurability of the dist=0 event.

[Sébastien Gouëzel]

Sure. My impression is that you don't need the measurability of the dist = 0 event if you organize the proof differently as I sketched.

[Rémy Degenne]

Oh but you mean that I don't need that event to be measurable at all. Right.

[Rémy Degenne]

I finished implementing that change (and switching from equalities to distances everywhere) in https://github.com/RemyDegenne/brownian-motion/pull/300. Now that PR has PseudoEMetricSpace E for all the main results.
Thanks @Sébastien Gouëzel !