Infinite independent increments

Stream: Brownian motion

[Joris van Winden]

I am formalizing the law of the iterated logarithm (currently working on the lower bound), and I have arrived at a point where I need to show that the variables n ↦ X (c ^ (n + 1)) ω - X (c ^ n) ω are independent. This turns out to be annoying since HasIndepIncrements only gives independence for a finite index set.

My question is the following: was it a deliberate choice to formulate HasIndepIncrements in terms of finite index sets? It seems that the alternative definition

def HasIndepIncrements' [Preorder T] [Sub E] [MeasurableSpace E] (X : T → Ω → E)
    (P : Measure Ω := by volume_tac) : Prop :=
  ∀ t : ℕ → T, Monotone t →
    iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P

is mathematically equivalent and disposes with the Fin n type.

[Rémy Degenne]

@Etienne Marion

[Etienne Marion]

That does seem like a good idea! I went with Fin because that is the way I have always seen it defined in textbooks, but I actually was quite annoyed having to deal with Fin, so if your definition works well we should definitely go with it. I am guessing you might have to rework some proofs in the BrownianMotion file though. If you don't want to deal with that I'd say you can introduce your definition while leaving the old one and we can get rid of it later.

[Joris van Winden]

Okay! Then I will give it a go to see if any unexpected problems turn up with the alternative definition.

[Joris van Winden]

For now I have managed to prove the expected equivalence:

lemma HasIndepIncrements.infinite_increments [Preorder T] [Sub E] [MeasurableSpace E]
    (X : T → Ω → E) (P : Measure Ω := by volume_tac) [IsProbabilityMeasure P] :
    HasIndepIncrements X P ↔ ∀ t : ℕ → T, Monotone t →
      iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P

I needed the typeclass [IsProbabilityMeasure P] in order to apply iIndepFun.of_subsingleton.

[Joris van Winden]

I have opened #377 to introduce the relevant lemmas.