Right-continuous filtration

Stream: Brownian motion

[Etienne Marion]

Ok so before going further I just want to check if the definition I got based on #Brownian motion > Tasks and claims @ 💬 looks sensible.

import Mathlib

open Topology Filter MeasureTheory

variable {Ω ι : Type*} {m : MeasurableSpace Ω}

variable [PartialOrder ι] [TopologicalSpace ι]

open scoped Classical in
noncomputable def rightCont (𝓕 : Filtration ι m) : Filtration ι m where
  seq i := if (𝓝[>] i).NeBot then ⨅ j > i, 𝓕 j else 𝓕 i
  mono' i j hij := by
    simp only [gt_iff_lt]
    split_ifs with hi hj hj
    · exact le_iInf₂ fun k hkj ↦ iInf₂_le k (hij.trans_lt hkj)
    · obtain rfl | hj := eq_or_ne j i
      · contradiction
      · have : i < j := lt_of_le_of_ne hij hj.symm
        exact iInf₂_le j this
    · exact le_iInf₂ fun k hk ↦ 𝓕.mono (hij.trans hk.le)
    · exact 𝓕.mono hij
  le' i := by
    split_ifs with hi
    · obtain ⟨j, hj⟩ := (frequently_gt_nhds i).exists
      exact iInf₂_le_of_le j hj (𝓕.le j)
    · exact 𝓕.le i

Compared to the "usual" one which only required Preorder ι, this requires PartialOrder ι and TopologicalSpace ι. This looks like reasonable assumptions to me, but I want to be sure others agree. In particular a filtration which is not indexed by a partial order seems weird, because as the space of measurable spaces is a partial order, we would get i ≤ j -> j ≤ i -> 𝓕 i = 𝓕 j, even though i ≠ j.

[Etienne Marion]

If I was more confident in order theory I would even say that if iota is a preorder we can factor the filtration through the quotient map from iota to its induced partial order.

[Etienne Marion]

Similarly I don't see how we wouldn't consider a topological space in practice, and as this is all about continuity it seems sensible to have a TopologicalSpace assumption.

[Rémy Degenne]

That definition looks good to me. In all applications we should have a linear order with the order topology, so I would no worry too much about Preorder vs PartialOrder.

[Sébastien Gouëzel]

I'm not sure it is a good idea to require a topological space instance: you could phrase it either by endowing the space with the order topology in the course of the definition, or replacing the (𝓝[>] i).NeBot condition with there exists j > i with Ioo i j = emptyset.

[Sébastien Gouëzel]

Except that my condition is not good when a point is maximal...

[Etienne Marion]

Suppose I endow iota with the order topology inside the definition. Then if I also assume iota has the order topology in some statement, I think I would need to rewrite using topology_eq_generate_intervals? This sounds a bit cumbersome to me.

[Etienne Marion]

Why do you think it's not a good idea to require a topological space instance?

[Sébastien Gouëzel]

Because it's not really relevant for the definition: it will only make sense if you have a topology and this topology happens to be the order topology. Which means your definition will in fact not depend on the topology, so why have it as a useless argument?
If you define it without topology, you could still have the lemma saying that, if iota has a topology which is the order topology, then rightCont 𝓕 i = if (𝓝[>] i).NeBot then ⨅ j > i, 𝓕 j else 𝓕 i. Then using this lemma you could use the definition just as you would using the current definition, but additionally whenever you write down rightCont 𝓕 i Lean doesn't need to go and fetch the topology on iota, so it's more economical.

[Kexing Ying]

Sébastien Gouëzel said:

Except that my condition is not good when a point is maximal...

I'd like to remark that our current definition of localizing sequence is also not ideal if there exists a maximal point: If the time index has a max element, then a localizing sequence should converge to that point instead currently Tendsto (τ · ω) atTop (𝓝 ⊤)

[Etienne Marion]

#207 is ready.