Measurability and separability in Kolmogorov-Chentsov

Stream: Brownian motion

[Rémy Degenne]

Our Kolmogorov-Chentsov theorem is weaker than the one presented in the Krätschmer-Urusov paper in one way: to get the existence of a continuous path modification of the process X : T → Ω → E, we assume separability of E (it is also stronger in other ways: we allow pseudo metric spaces for T and E).
The issue is in the proof of ProbabilityTheory.exists_modification_holder_aux', in which we use separability for two things:

• proving that a few distances are (strongly) measurable by proving measurability of both random variables involved. We can probably just be more careful and work only with distances, and use the strong measurability of distances that we get from the IsKolmogorovProcess assumption,
• using tendstoInMeasure_of_tendsto_ae_of_stronglyMeasurable, to get convergence in probability from a.e. convergence. That one requires all random variables to be strongly measurable, and we use Measurable.stronglyMeasurable to get that (we have strong measurability of the distances, but we only have measurability of the processes). This lemma requires separability. I investigated this for a bit and it looks like we might be able to modify the whole Egorov file to use the strong measurability of distances as hypothesis instead of strong measurability of the processes. By the way that would be the second time we change that file in this project, as we already extended it from metric to extended metric spaces.

I'm attempting the Egorov modification. I'm tagging @David Ledvinka who also wanted to try and remove the separability assumption.

[Rémy Degenne]

Using strongly measurable distances in the Egorov file was actually pretty easy: #30604
Now let's see if we can remove the other uses of separability.

[David Ledvinka]

I did some preliminary work on this today and had a similar conclusion on the first point but did not think of the second. I have a full proof of ProbabilityTheory.exists_modification_holder_aux if one can prove Y is also a Kolmogorov process (without using that X a.e equals Y since I use that in the proof). Its not clear that is easy/doable though. There is also measurable_limUnder which currently relies on separability.

[David Ledvinka]

A few of the uses that got flagged were easily removable by realizing that one of the haves had an unnecessary assumption. I made a draft PR but having some weird difference with the toolchain (its telling me there is a difference when there does not appear to be)

[David Ledvinka]

I just undrafted it: https://github.com/RemyDegenne/brownian-motion/pull/164

not sure whats going on with the toolchain difference thing but if its an issue you can just copy paste and PR yourself

[David Ledvinka]

So assuming I understand what your modification does then we just need a proof of Measurable (Y t) which does not use separability (which currently depends on measurable_limUnder which does use separability)

[Rémy Degenne]

My modification replaces the need for strong measurability of the processes at https://github.com/RemyDegenne/brownian-motion/blob/ffece15d17640299909ad0a3edc8b573c0847539/BrownianMotion/Continuity/KolmogorovChentsov.lean#L630C1-L632C1 by measurability of the distances from Y (u n) to Y t. We still need to prove that, but that looks feasible (those distances are limits of distances between some X s, which are measurable).

[Rémy Degenne]

I managed to deal with the measurability of limUnder: my progress is at https://github.com/RemyDegenne/brownian-motion/pull/166
There is still a sorry for the measurability of the distance between Y (u n) and Y t, and then several other places where separability is used in the next lemmas.

[David Ledvinka]

Proof of the sorry in ProbabilityTheory.exists_modification_holder_aux

lemma limUnder_prod {α β X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    [Nonempty X] [Nonempty Y] [T2Space X] [T2Space Y] {f : Filter α} {f' : Filter β}
    [NeBot f] [NeBot f'] {g : α → X} {g' : β → Y}
    (h₁ : ∃ x, Tendsto g f (𝓝 x)) (h₂ : ∃ x', Tendsto g' f' (𝓝 x')) :
    limUnder (f ×ˢ f') (fun x ↦ (g x.1, g' x.2)) = (limUnder f g, limUnder f' g') := by
  rw [Filter.Tendsto.limUnder_eq]
  rw [nhds_prod_eq]
  apply Filter.Tendsto.prodMk
  · refine Tendsto.comp ?_ tendsto_fst
    · rw[← Filter.limUnder_eq_iff (f := f)]; exact h₁
  · refine Tendsto.comp ?_ tendsto_snd
    · rw[← Filter.limUnder_eq_iff (f := f')]; exact h₂

have hY_pair s t : Measurable[_, borel (E × E)] (fun ω ↦ (Y s ω, Y t ω)) := by
  borelize (E × E)
  simp only [Dense.extend, IsDenseInducing.extend, Y]
  have : @NeBot (Subtype T') (comap Subtype.val (𝓝 s)) := by
    apply IsDenseInducing.comap_nhds_neBot (Dense.isDenseInducing_val hT'_dense)
  have : @NeBot (Subtype T') (comap Subtype.val (𝓝 t)) := by
     apply IsDenseInducing.comap_nhds_neBot (Dense.isDenseInducing_val hT'_dense)
  conv =>
    enter [1, ω]
    rw [← limUnder_prod]
    rfl
    tactic => exact hX'_tendsto s ω
    tactic => exact hX'_tendsto t ω
  let f (x : T' × T') (ω : Ω) := (X' x.1 ω, X' x.2 ω)
  apply measurable_limUnder_of_exists_tendsto (f := f)
  intro ω
  obtain ⟨c₀, h₀⟩ := hX'_tendsto s ω
  obtain ⟨c₁, h₁⟩ := hX'_tendsto t ω
  use (c₀,c₁)
  unfold f
  rw [nhds_prod_eq]
  apply Filter.Tendsto.prodMk
  · exact h₀.comp tendsto_fst
  · exact h₁.comp tendsto_snd
  unfold f
  intro i
  have : (fun ω ↦ (X' (↑i.1) ω, X' (↑i.2) ω))
      = fun ω ↦ if ω ∈ A then (X i.1 ω, X i.2 ω) else (x₀, x₀) := by
    ext ω <;> by_cases hω : ω ∈ A <;> simp [X', hω]
  rw [this]
  exact Measurable.ite hA (hX.measurablePair i.1 i.2) measurable_const

[David Ledvinka]

Very messy and should be cleaned/golfed but gives a complete proof of ProbabilityTheory.exists_modification_holder_aux. I think the sorrys in the other lemmas should be provable using a similar idea.

[David Ledvinka]

I have to stop for now so feel free to do whatever with it, will pick back up either tonight or tomorrow

[Rémy Degenne]

Very nice! Something similar should work in the next lemmas, but for that we need to modify the statements to remember that the modifications we build are limits of X. I'll work on it in the next few hours

[Rémy Degenne]

Done. The PR https://github.com/RemyDegenne/brownian-motion/pull/166 has a fully separability-free proof. It took me ages to find the right formulation of the hypotheses "the modifications we build are limits of X". What we want is that if X and Y are processes such that (X i, Y j) is measurable for all i, j, then our proof applies only transformations in a class such that if X', Y' are the results, then (X' i, Y' j) is still measurable. The question is what that class is. I settled on this:

/-- Process where we replace the values for `ω` outside of `A` with a constant value. -/
noncomputable
def indicatorProcess (X : T → Ω → E) (A : Set Ω) : T → Ω → E :=
  haveI := Classical.decPred (· ∈ A)
  fun t ω ↦ if ω ∈ A then X t ω else hE.some

def IsLimitOfIndicator (Y X : T → Ω → E) (P : Measure Ω) (U : Set T) : Prop :=
  ∃ (A : Set Ω), MeasurableSet A ∧
    (∀ᵐ ω ∂P, ω ∈ A) ∧
    (∀ t ∈ U, ∀ ω ∈ A, ∃ c, Tendsto (fun t' : denseCountable T ↦ X t' ω)
      (comap Subtype.val (𝓝 t)) (𝓝 c)) ∧
    ∀ t ω, Y t ω = if t ∈ U then dense_denseCountable.extend
      (fun t' : denseCountable T ↦ indicatorProcess X A t' ω) t else hE.some

lemma IsLimitOfIndicator.measurable_pair {Y X Z X' : T → Ω → E} {U₁ U₂ : Set T}
    (hX : ∀ t, Measurable (X t)) (hX' : ∀ t, Measurable (X' t))
    (hX_pair : ∀ i j, Measurable[_, borel (E × E)] fun ω ↦ (X i ω, X' j ω))
    (hY : IsLimitOfIndicator Y X P U₁) (hZ : IsLimitOfIndicator Z X' P U₂)
    (s t : T) :
    Measurable[_, borel (E × E)] (fun ω ↦ (Y s ω, Z t ω)) := by

(denseCountable T is a dense countable subset of T, which is second-countable: we are fighting over separability of E, not T)
That's the property of being an indicator over time of a limit of an indicator over the measurable space. It's certainly ad hoc for the proof at hand, but we can show that all the modifications we build satisfy that property, and we can use measurability of pairs everywhere.

The other big change in the PR is that before we were building modifications on the whole space (and suffered through subtype hell at one point, but not too much) and to make my life easier I modified the code to allow building modifications on an open subset.

That effort to remove separability was a remarkable example of the kind of approximation that you can get away with on paper but not formally: when we build several modifications of the process and then combine them, we can't apply the main theorem as it is stated ("there exists a measurable modification with Hölder paths"), or we don't know that we will have measurable pairs. What we use is actually a property of the particular modification that is built in the proof of the theorem, and the fact that the ways we combine them preserve that property.
Of course all of that is not needed if the way you prove the measurability is by writing "it can be shown by standard arguments that this random process satisfies [the measurability condition]".

[Etienne Marion]

That's great :tada:! I notice that you can rephrase the last part of IsLimitOfIndicator with Y = indicatorProcess (dense_denseCountable.extend ...) U, but I don't know if that's useful.