Markov property of processes with independent increments

DefinitionPredecessor of a time in a finite set#✓fully proved

For a finite set \(S \subseteq \mathbb{R}_{\ge 0}\) and \(t \in \mathbb{R}_{\ge 0}\), the predecessor of \(t\) in \(S\) is the largest element of \(S\) strictly below \(t\), or \(0\) if there is no such element.

noncomputable def bmPrev (S : Finset ℝ≥0) (t : ℝ≥0) : ℝ≥0 :=
  (S.filter (· < t)).sup id

Used by 8

Used byTelescoping the centered shifted path over a finite set · Increment over the predecessor interval · Inserting a larger element does not change the predecessor · Predecessor of a new maximum · Measurability of the increments · Measurability of an increment before a given time · Past events factor against grid increments · Telescoping sum of grid increments

DefinitionIncrement over the predecessor interval#✓fully proved

Let \((B_t)_{t \ge 0}\) be a real-valued process on \(\Omega\), let \(s \ge 0\), and let \(S \subset \mathbb{R}_{\ge 0}\) be a finite set. For \(t \ge 0\) let \(t^-\) be the largest element of \(S\) strictly below \(t\), or \(0\) if there is none. The increment at \(t\) is the random variable \(\omega \mapsto B_{s+t}(\omega) - B_{s+t^-}(\omega)\).

noncomputable def bmInc (B : ℝ≥0 → Ω → ℝ) (s : ℝ≥0) (S : Finset ℝ≥0)
    (t : ℝ≥0) (ω : Ω) : ℝ :=
  B (s + t) ω - B (s + bmPrev S t) ω

Uses 1 · Used by 10

Statement usesPredecessor of a time in a finite set

Used byTelescoping the centered shifted path over a finite set · Increment rectangles · Independence of future increments from the present · Measurability of the increments · Measurability of an increment in the increment σ-algebra · Measurability of an increment before a given time · Centered cylinders lie in the increment σ-algebra · Events of a single increment lie in the increment σ-algebra · Past events factor against grid increments · Telescoping sum of grid increments

DefinitionShifted path of a process#✓fully proved

For a real-valued process \((B_t)_{t \ge 0}\) on \(\Omega\) indexed by \(t \in \mathbb{R}_{\ge 0}\) and a time \(s \ge 0\), the shifted path is the map sending \(\omega \in \Omega\) to the path \(t \mapsto B_{s+t}(\omega)\) in \(\mathbb{R}^{\mathbb{R}_{\ge 0}}\).

noncomputable def bmShifted (B : ℝ≥0 → Ω → ℝ) (s : ℝ≥0) : Ω → (ℝ≥0 → ℝ) :=
  fun ω t => B (s + t) ω

Used by 6

Used bySet integrals of the path expectation · Translating the centered future path recovers the shifted path · Conditional expectation of a future path functional · Nonnegative integrals of future path functionals over present events · Bounded integrals of future path functionals over present events · Measurability of the shifted path

DefinitionCentered shifted path#✓fully proved

Let \((B_t)_{t \ge 0}\) be a real-valued process on \(\Omega\) and let \(s \ge 0\). The centered shifted path at time \(s\) sends \(\omega \in \Omega\) to the function \(t \mapsto B_{s+t}(\omega) - B_s(\omega)\) on \(\mathbb{R}_{\ge 0}\).

noncomputable def bmCenteredShift (B : ℝ≥0 → Ω → ℝ) (s : ℝ≥0) :
    Ω → (ℝ≥0 → ℝ) :=
  fun ω t => B (s + t) ω - B s ω

Used by 15

Used byCylinder events of the centered shifted path · Telescoping the centered shifted path over a finite set · Law of the centered shifted path · The process value paired with its centered future path · Bound on the path expectation · Set integrals of the path expectation · Independence of the centered future path from the present · Measurability of the centered shifted path · Measurability of the pair map · The path expectation is measurable in the starting point · Nonnegative translated integrals against the centered law are measurable · Section measures of the centered law are measurable · Centered cylinders lie in the increment σ-algebra · The pair-section identity for measurable sets · The pair identity on cylinder rectangles

DefinitionLaw of the centered shifted path#✓fully proved

Let \((B_t)_{t \ge 0}\) be a real-valued process on a measure space \((\Omega, \mu)\) and let \(s \ge 0\). This is the pushforward of \(\mu\) under the map sending \(\omega \in \Omega\) to the path \(t \mapsto B_{s+t}(\omega) - B_s(\omega)\), a measure on the space of functions \(\mathbb{R}_{\ge 0} \to \mathbb{R}\) with its product σ-algebra.

noncomputable def bmCenteredLaw (B : ℝ≥0 → Ω → ℝ) (μ : Measure Ω) (s : ℝ≥0) :
    Measure (ℝ≥0 → ℝ) :=
  Measure.map (bmCenteredShift B s) μ

Uses 1 · Used by 9

Statement usesCentered shifted path

Used byTime-dependent path expectation · Bound on the path expectation · Set integrals of the path expectation · Nonnegative integrals of future path functionals over present events · The path expectation is measurable in the starting point · Nonnegative translated integrals against the centered law are measurable · Section measures of the centered law are measurable · The pair-section identity for measurable sets · The pair identity on cylinder rectangles

DefinitionTime-dependent path expectation#✓fully proved

Let \(\mu\) be a measure on \(\Omega\), let \((B_t)_{t \ge 0}\) be a real process on \(\Omega\) indexed by \(t \in \mathbb{R}_{\ge 0}\), let \(s \ge 0\), and let \(\nu_s\) be the law under \(\mu\) (the pushforward of \(\mu\)) of the centered shifted path \(\omega \mapsto (t \mapsto B_{s+t}(\omega) - B_s(\omega))\). For a real function \(Y\) on paths \(\mathbb{R}_{\ge 0} \to \mathbb{R}\) and \(x \in \mathbb{R}\), the path expectation is the Bochner integral \(\int Y(t \mapsto x + f(t))\, d\nu_s(f)\), which is \(0\) when the integrand is not integrable.

This value can depend on \(s\); it is the generic time-dependent expectation.

noncomputable def bmPathExpectation (B : ℝ≥0 → Ω → ℝ) (μ : Measure Ω) (s : ℝ≥0)
    (Y : (ℝ≥0 → ℝ) → ℝ) (x : ℝ) : ℝ :=
  ∫ f, Y (fun t => x + f t) ∂(bmCenteredLaw B μ s)

Uses 1 · Used by 5

Statement usesLaw of the centered shifted path

Used byBound on the path expectation · Set integrals of the path expectation · Conditional expectation of a future path functional · Bounded integrals of future path functionals over present events · The path expectation is measurable in the starting point

AbbreviationAdapted real process#✓fully proved

A real-valued process \((B_t)_{t \ge 0}\) on \(\Omega\), indexed by \(t \in \mathbb{R}_{\ge 0}\), is adapted to a filtration \((\mathcal{F}_t)_{t \ge 0}\) when \(B_t\) is \(\mathcal{F}_t\)-measurable for every \(t \ge 0\).

abbrev BmAdapted (B : ℝ≥0 → Ω → ℝ) (ℱ : Filtration ℝ≥0 m0) : Prop :=
  ∀ t, Measurable[ℱ t] (B t)

Used by 14

Used bySet integrals of the path expectation · Independence of the centered future path from the present · Independence of future increments from the present · Conditional expectation of a future path functional · Nonnegative integrals of future path functionals over present events · Bounded integrals of future path functionals over present events · Measurability of the centered shifted path · Measurability of the increments · Measurability of an increment before a given time · Measurability of the pair map · Measurability of the shifted path · Past events factor against grid increments · The pair-section identity for measurable sets · The pair identity on cylinder rectangles

AbbreviationIndependent increments with respect to a filtration#✓fully proved

A real-valued process \((B_t)_{t \ge 0}\) on \(\Omega\) has independent increments with respect to a filtration \((\mathcal{F}_t)_{t \ge 0}\) and a measure \(\mu\) when, for all \(0 \le s \le t\), the σ-algebra generated by \(B_t - B_s\) is independent of \(\mathcal{F}_s\) under \(\mu\).

abbrev BmIndepIncrements (B : ℝ≥0 → Ω → ℝ) (ℱ : Filtration ℝ≥0 m0)
    (μ : Measure Ω) : Prop :=
  ∀ s t : ℝ≥0, s ≤ t →
    Indep (ℱ s) (MeasurableSpace.comap (fun ω => B t ω - B s ω) inferInstance) μ

Used by 9

Used bySet integrals of the path expectation · Independence of the centered future path from the present · Independence of future increments from the present · Conditional expectation of a future path functional · Nonnegative integrals of future path functionals over present events · Bounded integrals of future path functionals over present events · Past events factor against grid increments · The pair-section identity for measurable sets · The pair identity on cylinder rectangles

LemmaMeasurability of the shifted path#✓fully proved

Let \(B = (B_t)_{t \ge 0}\) be a real process on a measurable space \(\Omega\), adapted to a filtration \((\mathcal{F}_t)_{t \ge 0}\) of its σ-algebra, and give the space \(\mathbb{R}^{[0, \infty)}\) of real paths indexed by \(t \ge 0\) the product σ-algebra. For every \(s \ge 0\), the map from \(\Omega\) to \(\mathbb{R}^{[0, \infty)}\) sending \(\omega\) to the path \(t \mapsto B_{s+t}(\omega)\) is measurable.

Each coordinate \(B_{s+t}\) is \(\mathcal{F}_{s+t}\)-measurable, hence measurable.

lemma measurable_bmShifted (hAd : BmAdapted B ℱ) (s : ℝ≥0) :
    Measurable (bmShifted B s)

Uses 2 · Used by 3

Statement usesAdapted real process · Shifted path of a process

Used byConditional expectation of a future path functional · Nonnegative integrals of future path functionals over present events · Bounded integrals of future path functionals over present events

LemmaMeasurability of the centered shifted path#✓fully proved

Let \((\mathcal{F}_t)_{t \ge 0}\) be a filtration on a measurable space \(\Omega\) indexed by \(\mathbb{R}_{\ge 0}\), and let \((B_t)_{t \ge 0}\) be a real-valued process adapted to it (each \(B_t\) is \(\mathcal{F}_t\)-measurable). Then for every \(s \ge 0\) the map \(\omega \mapsto (t \mapsto B_{s+t}(\omega) - B_s(\omega))\) from \(\Omega\) to \(\mathbb{R}^{\mathbb{R}_{\ge 0}}\), with the product σ-algebra, is measurable.

lemma measurable_bmCenteredShift (hAd : BmAdapted B ℱ) (s : ℝ≥0) :
    Measurable (bmCenteredShift B s)

Uses 2 · Used by 3

Statement usesAdapted real process · Centered shifted path

Used byIndependence of the centered future path from the present · Measurability of the pair map · The pair identity on cylinder rectangles

LemmaMeasurability of an increment before a given time#✓fully proved

Let \(B = (B_t)_{t \ge 0}\) be a real process on a measurable space \(\Omega\), adapted to a filtration \((\mathcal{F}_t)_{t \ge 0}\) of its σ-algebra, let \(S\) be a finite set of nonnegative reals and let \(s, t, u \ge 0\). Write \(p_S(t)\) for the largest element of \(S\) strictly below \(t\), or \(0\) if there is none. If \(s + t \le s + u\) and \(s + p_S(t) \le s + u\), then the increment \(B_{s+t} - B_{s+p_S(t)}\) is \(\mathcal{F}_{s+u}\)-measurable.

lemma measurable_bmInc_of_le (hAd : BmAdapted B ℱ) {s u t : ℝ≥0}
    (S : Finset ℝ≥0) (ht : s + t ≤ s + u) (hprev : s + bmPrev S t ≤ s + u) :
    Measurable[ℱ (s + u)] (fun ω => bmInc B s S t ω)

Uses 3 · Used by 1

Statement usesAdapted real process · Increment over the predecessor interval · Predecessor of a time in a finite set

Used byPast events factor against grid increments

LemmaInserting a larger element does not change the predecessor#✓fully proved

For a finite set \(T \subseteq \mathbb{R}_{\ge 0}\) and \(t \in \mathbb{R}_{\ge 0}\), call the largest element of \(T\) strictly below \(t\) (or \(0\) if there is none) the predecessor of \(t\) in \(T\). Let \(S \subseteq \mathbb{R}_{\ge 0}\) be finite and let \(t, a \in \mathbb{R}_{\ge 0}\) with \(t < a\). Then the predecessor of \(t\) in \(S \cup \{a\}\) equals the predecessor of \(t\) in \(S\).

lemma bmPrev_insert_of_lt {a : ℝ≥0} {S' : Finset ℝ≥0} {t : ℝ≥0} (ht : t < a) :
    bmPrev (insert a S') t = bmPrev S' t

Uses 1 · Used by 2

Statement usesPredecessor of a time in a finite set

Used byPast events factor against grid increments · Telescoping sum of grid increments

LemmaPredecessor of a new maximum#✓fully proved

For a finite set \(T \subseteq \mathbb{R}_{\ge 0}\) and \(t \in \mathbb{R}_{\ge 0}\), call the largest element of \(T\) strictly below \(t\) (or \(0\) if there is none) the predecessor of \(t\) in \(T\). Let \(S \subseteq \mathbb{R}_{\ge 0}\) be finite and let \(a \in \mathbb{R}_{\ge 0}\) with \(x < a\) for every \(x \in S\). Then the predecessor of \(a\) in \(S \cup \{a\}\) is the supremum of \(S\) in \(\mathbb{R}_{\ge 0}\), that is, its largest element, or \(0\) if \(S\) is empty.

lemma bmPrev_insert_self {a : ℝ≥0} {S' : Finset ℝ≥0}
    (h : ∀ x ∈ S', x < a) :
    bmPrev (insert a S') a = S'.sup id

Uses 1 · Used by 2

Statement usesPredecessor of a time in a finite set

Used byPast events factor against grid increments · Telescoping sum of grid increments

LemmaPast events factor against grid increments#✓fully proved

Let \(\mu\) be a probability measure and let \((B_t)_{t \ge 0}\) be a real process adapted to a filtration \((\mathcal{F}_t)_{t \ge 0}\) such that \(B_t - B_s\) is independent of \(\mathcal{F}_s\) under \(\mu\) whenever \(s \le t\). Let \(s \in \mathbb{R}_{\ge 0}\) and let \(S \subseteq \mathbb{R}_{\ge 0}\) be finite. For \(t \in S\) let \(\Delta_t = B_{s+t} - B_{s+t^-}\), where \(t^-\) is the largest element of \(S\) strictly below \(t\), or \(0\) if there is none. Then for every family \((C_t)_{t \ge 0}\) of Borel subsets of \(\mathbb{R}\) and every \(A \in \mathcal{F}_s\),

\[\mu\Big(A \cap \bigcap_{t \in S} \{\Delta_t \in C_t\}\Big) = \mu(A)\,\mu\Big(\bigcap_{t \in S} \{\Delta_t \in C_t\}\Big).\]

The proof is induction on \(S\) by its maximum element \(a\): the increment \(\Delta_a\) is independent of \(\mathcal{F}_{s + a^-}\), which contains both \(A\) and the earlier increments.

lemma measure_inter_biInter_bmInc (hAd : BmAdapted B ℱ)
    (hInd : BmIndepIncrements B ℱ μ) [IsProbabilityMeasure μ] (s : ℝ≥0)
    (S : Finset ℝ≥0) (C : ℝ≥0 → Set ℝ) (hC : ∀ t, MeasurableSet (C t))
    (A : Set Ω) (hA : MeasurableSet[ℱ s] A) :
    μ (A ∩ ⋂ t ∈ S, {ω | bmInc B s S t ω ∈ C t})
      = μ A * μ (⋂ t ∈ S, {ω | bmInc B s S t ω ∈ C t})

Uses 7 · Used by 1

Statement usesAdapted real process · Independent increments with respect to a filtration · Increment over the predecessor interval

Proof usesPredecessor of a time in a finite set · Inserting a larger element does not change the predecessor · Predecessor of a new maximum · Measurability of an increment before a given time

Used byIndependence of future increments from the present

LemmaTelescoping sum of grid increments#✓fully proved

Let \((B_t)_{t \ge 0}\) be a family of real functions on \(\Omega\), let \(s \in \mathbb{R}_{\ge 0}\) and let \(S \subseteq \mathbb{R}_{\ge 0}\) be a nonempty finite set. For \(u \in S\) let \(\Delta_u = B_{s+u} - B_{s+u^-}\), where \(u^-\) is the largest element of \(S\) strictly below \(u\), or \(0\) if there is none. Then for every \(\omega \in \Omega\), \(\sum_{u \in S} \Delta_u(\omega) = B_{s + \max S}(\omega) - B_s(\omega)\).

lemma sum_bmInc_eq {s : ℝ≥0} (S : Finset ℝ≥0) (hS : S.Nonempty) (ω : Ω) :
    ∑ u ∈ S, bmInc B s S u ω = B (s + S.sup id) ω - B s ω

Uses 4 · Used by 1

Statement usesIncrement over the predecessor interval

Proof usesPredecessor of a time in a finite set · Inserting a larger element does not change the predecessor · Predecessor of a new maximum

Used byTelescoping the centered shifted path over a finite set

LemmaTelescoping the centered shifted path over a finite set#✓fully proved

Let \((B_t)_{t \ge 0}\) be a real-valued process on \(\Omega\), let \(s \ge 0\), and let \(S \subset \mathbb{R}_{\ge 0}\) be a finite set. For \(u \ge 0\) let \(u^-\) be the largest element of \(S\) strictly below \(u\), or \(0\) if there is none. Then for every \(t \in S\) and every \(\omega \in \Omega\), \(B_{s+t}(\omega) - B_s(\omega) = \sum_{u \in S : u \le t} (B_{s+u}(\omega) - B_{s+u^-}(\omega))\).

lemma bmCentered_eq_sum_bmInc {s : ℝ≥0} (S : Finset ℝ≥0) {t : ℝ≥0} (ht : t ∈ S) (ω : Ω) :
    bmCenteredShift B s ω t
      = ∑ u ∈ S.filter (· ≤ t), bmInc B s S u ω

Uses 4 · Used by 1

Statement usesCentered shifted path · Increment over the predecessor interval

Proof usesPredecessor of a time in a finite set · Telescoping sum of grid increments

Used byCentered cylinders lie in the increment σ-algebra

LemmaMeasurability of the increments#✓fully proved

Let \(B = (B_t)_{t \ge 0}\) be a real process on a measurable space \(\Omega\), adapted to a filtration \((\mathcal{F}_t)_{t \ge 0}\) of its σ-algebra. For every finite set \(S\) of nonnegative reals and all \(s, t \ge 0\), the increment \(B_{s+t} - B_{s+p_S(t)}\) is measurable, where \(p_S(t)\) is the largest element of \(S\) strictly below \(t\), or \(0\) if there is none.

lemma measurable_bmInc (hAd : BmAdapted B ℱ) {s : ℝ≥0} (S : Finset ℝ≥0) (t : ℝ≥0) :
    Measurable fun ω => bmInc B s S t ω

Uses 3 · Used by 1

Statement usesAdapted real process · Increment over the predecessor interval

Proof usesPredecessor of a time in a finite set

Used byIndependence of future increments from the present

DefinitionIncrement rectangles#✓fully proved

Let \((B_t)_{t \ge 0}\) be a real-valued process on \(\Omega\), let \(s \ge 0\), and let \(S \subset \mathbb{R}_{\ge 0}\) be a finite set. For \(t \ge 0\) let \(t^-\) be the largest element of \(S\) strictly below \(t\), or \(0\) if there is none. The increment rectangles are the events \(\bigcap_{t \in S} \{\omega \in \Omega : B_{s+t}(\omega) - B_{s+t^-}(\omega) \in C_t\}\), where each \(C_t \subseteq \mathbb{R}\) is a Borel set.

def bmIncRectangles (B : ℝ≥0 → Ω → ℝ) (s : ℝ≥0) (S : Finset ℝ≥0) :
    Set (Set Ω) :=
  {T | ∃ C : ℝ≥0 → Set ℝ, (∀ t, MeasurableSet (C t)) ∧
    T = ⋂ t ∈ S, {ω | bmInc B s S t ω ∈ C t}}

Uses 1 · Used by 3

Statement usesIncrement over the predecessor interval

Used byσ-algebra of the increments over a finite set · Independence of future increments from the present · Events of a single increment lie in the increment σ-algebra

Definitionσ-algebra of the increments over a finite set#✓fully proved

Let \((B_t)_{t \ge 0}\) be a real-valued process on \(\Omega\), let \(s \ge 0\), and let \(S \subset \mathbb{R}_{\ge 0}\) be a finite set. For \(t \ge 0\) let \(t^-\) be the largest element of \(S\) strictly below \(t\), or \(0\) if there is none. This is the σ-algebra on \(\Omega\) generated by the increment rectangles, the events \(\bigcap_{t \in S} \{\omega \in \Omega : B_{s+t}(\omega) - B_{s+t^-}(\omega) \in C_t\}\) with each \(C_t \subseteq \mathbb{R}\) a Borel set.

@[instance_reducible]
def bmIncSigma (B : ℝ≥0 → Ω → ℝ) (s : ℝ≥0) (S : Finset ℝ≥0) :
    MeasurableSpace Ω :=
  MeasurableSpace.generateFrom (bmIncRectangles B s S)

Uses 1 · Used by 5

Statement usesIncrement rectangles

Used byIndependence of the centered future path from the present · Independence of future increments from the present · Measurability of an increment in the increment σ-algebra · Centered cylinders lie in the increment σ-algebra · Events of a single increment lie in the increment σ-algebra

LemmaEvents of a single increment lie in the increment σ-algebra#✓fully proved

Let \(B = (B_t)_{t \ge 0}\) be a real process on a measurable space \(\Omega\), let \(s \ge 0\) and let \(S\) be a finite set of nonnegative reals. For \(u \ge 0\) let \(p_S(u)\) be the largest element of \(S\) strictly below \(u\), or \(0\) if there is none, and let \(\Delta_u = B_{s+u} - B_{s+p_S(u)}\). Let \(\mathcal{G}_S\) be the σ-algebra on \(\Omega\) generated by the sets \(\bigcap_{u \in S} \{\omega : \Delta_u(\omega) \in E_u\}\) for families \((E_u)_{u \ge 0}\) of measurable subsets of \(\mathbb{R}\). Then for every \(t \in S\) and every measurable \(D \subseteq \mathbb{R}\), the event \(\{\omega : \Delta_t(\omega) \in D\}\) belongs to \(\mathcal{G}_S\).

lemma measurableSet_bmInc_preimage {s : ℝ≥0} (S : Finset ℝ≥0) {t : ℝ≥0} (ht : t ∈ S)
    {D : Set ℝ} (hD : MeasurableSet D) :
    MeasurableSet[bmIncSigma B s S] {ω | bmInc B s S t ω ∈ D}

Uses 3 · Used by 1

Statement usesIncrement over the predecessor interval · σ-algebra of the increments over a finite set

Proof usesIncrement rectangles

Used byMeasurability of an increment in the increment σ-algebra

LemmaMeasurability of an increment in the increment σ-algebra#✓fully proved

Let \((B_t)_{t \ge 0}\) be a real-valued process on \(\Omega\), let \(s \ge 0\), and let \(S \subseteq \mathbb{R}_{\ge 0}\) be finite; for \(t \in S\) let \(t^-\) be the largest element of \(S\) strictly below \(t\), or \(0\) if there is none. Then for every \(t \in S\), the increment \(\omega \mapsto B_{s+t}(\omega) - B_{s+t^-}(\omega)\) is measurable with respect to the σ-algebra generated by the events \(\bigcap_{u \in S} \{B_{s+u} - B_{s+u^-} \in C_u\}\), where every \(C_u \subseteq \mathbb{R}\) is Borel.

lemma measurable_bmInc_incSigma {s : ℝ≥0} (S : Finset ℝ≥0) {t : ℝ≥0} (ht : t ∈ S) :
    Measurable[bmIncSigma B s S] (fun ω => bmInc B s S t ω)

Uses 3 · Used by 1

Statement usesIncrement over the predecessor interval · σ-algebra of the increments over a finite set

Proof usesEvents of a single increment lie in the increment σ-algebra

Used byCentered cylinders lie in the increment σ-algebra

LemmaIndependence of future increments from the present#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \((\mathcal{F}_t)_{t \ge 0}\) be a filtration indexed by \(\mathbb{R}_{\ge 0}\), and let \((B_t)_{t \ge 0}\) be a real-valued process that is adapted (each \(B_t\) is \(\mathcal{F}_t\)-measurable) and has independent increments (for \(u \le t\), the increment \(B_t - B_u\) is independent of \(\mathcal{F}_u\) under \(\mu\)). For a finite set \(S \subseteq \mathbb{R}_{\ge 0}\) and \(t \in S\), let \(t^-\) be the largest element of \(S\) strictly below \(t\), or \(0\) if there is none. Then for every \(s \ge 0\) and every finite \(S \subseteq \mathbb{R}_{\ge 0}\), \(\mathcal{F}_s\) is independent under \(\mu\) of the σ-algebra generated by the events \(\bigcap_{t \in S} \{B_{s+t} - B_{s+t^-} \in C_t\}\), where every \(C_t \subseteq \mathbb{R}\) is Borel.

lemma indep_bmIncSigma (hAd : BmAdapted B ℱ) (hInd : BmIndepIncrements B ℱ μ)
    [IsProbabilityMeasure μ] (s : ℝ≥0) (S : Finset ℝ≥0) :
    Indep (ℱ s) (bmIncSigma B s S) μ

Uses 7 · Used by 1

Statement usesAdapted real process · Independent increments with respect to a filtration · σ-algebra of the increments over a finite set

Proof usesIncrement over the predecessor interval · Increment rectangles · Measurability of the increments · Past events factor against grid increments

Used byIndependence of the centered future path from the present

DefinitionCylinder events of the centered shifted path#✓fully proved

Let \((B_t)_{t \ge 0}\) be a real-valued process on \(\Omega\) and let \(s \ge 0\). The centered cylinders at time \(s\) are the events \(\bigcap_{t \in S} \{\omega \in \Omega : B_{s+t}(\omega) - B_s(\omega) \in C_t\}\), where \(S \subset \mathbb{R}_{\ge 0}\) is a finite set and each \(C_t \subseteq \mathbb{R}\) is a Borel set.

def bmCenteredCylinders (B : ℝ≥0 → Ω → ℝ) (s : ℝ≥0) : Set (Set Ω) :=
  {T | ∃ (S : Finset ℝ≥0) (C : ℝ≥0 → Set ℝ), (∀ t, MeasurableSet (C t)) ∧
    T = ⋂ t ∈ S, {ω | bmCenteredShift B s ω t ∈ C t}}

Uses 1 · Used by 1

Statement usesCentered shifted path

Used byIndependence of the centered future path from the present

LemmaCentered cylinders lie in the increment σ-algebra#✓fully proved

Let \(B = (B_t)_{t \ge 0}\) be a real process on a measurable space \(\Omega\), let \(s \ge 0\) and let \(S\) be a finite set of nonnegative reals. For \(u \ge 0\) let \(p_S(u)\) be the largest element of \(S\) strictly below \(u\), or \(0\) if there is none, and let \(\Delta_u = B_{s+u} - B_{s+p_S(u)}\). Let \(\mathcal{G}_S\) be the σ-algebra on \(\Omega\) generated by the sets \(\bigcap_{u \in S} \{\omega : \Delta_u(\omega) \in E_u\}\) for families \((E_u)_{u \ge 0}\) of measurable subsets of \(\mathbb{R}\). Then for every family \((C_t)_{t \ge 0}\) of measurable subsets of \(\mathbb{R}\), the set \(\bigcap_{t \in S} \{\omega : B_{s+t}(\omega) - B_s(\omega) \in C_t\}\) belongs to \(\mathcal{G}_S\).

lemma measurableSet_bmCentered_cylinder {s : ℝ≥0} (S : Finset ℝ≥0) (C : ℝ≥0 → Set ℝ)
    (hC : ∀ t, MeasurableSet (C t)) :
    MeasurableSet[bmIncSigma B s S]
      (⋂ t ∈ S, {ω | bmCenteredShift B s ω t ∈ C t})

Uses 5 · Used by 1

Statement usesCentered shifted path · σ-algebra of the increments over a finite set

Proof usesTelescoping the centered shifted path over a finite set · Increment over the predecessor interval · Measurability of an increment in the increment σ-algebra

Used byIndependence of the centered future path from the present

LemmaEvaluation events are measurable#✓fully proved

For every \(t \in \mathbb{R}_{\ge 0}\) and every Borel set \(D \subseteq \mathbb{R}\), the set of paths \(f : \mathbb{R}_{\ge 0} \to \mathbb{R}\) with \(f(t) \in D\) is measurable for the product σ-algebra on the space of all such paths.

lemma measurableSet_pi_eval_preimage {t : ℝ≥0} {D : Set ℝ} (hD : MeasurableSet D) :
    MeasurableSet {f : ℝ≥0 → ℝ | f t ∈ D}

Used by 3

Used byIndependence of the centered future path from the present · The pair identity on cylinder rectangles · Cylinder rectangles generate the product σ-algebra

LemmaIndependence of the centered future path from the present#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \((\mathcal{F}_t)_{t \ge 0}\) be a filtration indexed by \(\mathbb{R}_{\ge 0}\), and let \((B_t)_{t \ge 0}\) be a real-valued process that is adapted (each \(B_t\) is \(\mathcal{F}_t\)-measurable) and has independent increments (for \(u \le t\), the increment \(B_t - B_u\) is independent of \(\mathcal{F}_u\) under \(\mu\)). Then for every \(s \ge 0\), \(\mathcal{F}_s\) is independent under \(\mu\) of the σ-algebra generated by the centered shifted path \(\omega \mapsto (t \mapsto B_{s+t}(\omega) - B_s(\omega))\), where the path space \(\mathbb{R}^{\mathbb{R}_{\ge 0}}\) carries the product σ-algebra.

lemma indep_bmCenteredShift (hAd : BmAdapted B ℱ) (hInd : BmIndepIncrements B ℱ μ)
    [IsProbabilityMeasure μ] (s : ℝ≥0) :
    Indep (ℱ s) (MeasurableSpace.comap (bmCenteredShift B s) inferInstance) μ

Uses 9 · Used by 1

Statement usesAdapted real process · Independent increments with respect to a filtration · Centered shifted path

Proof usesCylinder events of the centered shifted path · σ-algebra of the increments over a finite set · Independence of future increments from the present · Centered cylinders lie in the increment σ-algebra · Evaluation events are measurable · Measurability of the centered shifted path

Used byThe pair identity on cylinder rectangles

DefinitionCylinder sets of path space#✓fully proved

The collection of sets of paths \(f : \mathbb{R}_{\ge 0} \to \mathbb{R}\) of the form \(\bigcap_{t \in S} \{f : f(t) \in C_t\}\), where \(S \subseteq \mathbb{R}_{\ge 0}\) is a finite set and each \(C_t\) is a measurable subset of \(\mathbb{R}\).

def bmPathCylinders : Set (Set (ℝ≥0 → ℝ)) :=
  {T | ∃ (S : Finset ℝ≥0) (C : ℝ≥0 → Set ℝ), (∀ t, MeasurableSet (C t)) ∧
    T = ⋂ t ∈ S, {f | f t ∈ C t}}

Used by 3

Used byPath cylinders form a π-system · Measurable rectangles lie in the σ-algebra of cylinder rectangles · Cylinders generate the product σ-algebra on path space

LemmaPath cylinders form a π-system#✓fully proved

Consider the subsets of \(\mathbb{R}^{\mathbb{R}_{\ge 0}}\) of the form \(\bigcap_{t \in S} \{f : f(t) \in C_t\}\), where \(S \subseteq \mathbb{R}_{\ge 0}\) is finite and every \(C_t \subseteq \mathbb{R}\) is Borel. They form a π-system: whenever two of them have nonempty intersection, the intersection is again of this form.

lemma isPiSystem_bmPathCylinders : IsPiSystem bmPathCylinders

Uses 1 · Used by 1

Statement usesCylinder sets of path space

Used byMeasurable rectangles lie in the σ-algebra of cylinder rectangles

LemmaCylinders generate the product σ-algebra on path space#✓fully proved

The product σ-algebra on the space of paths \(f : \mathbb{R}_{\ge 0} \to \mathbb{R}\) equals the σ-algebra generated by the cylinders, the sets \(\{f : f(t) \in C_t \text{ for all } t \in S\}\) with \(S\) a finite subset of \(\mathbb{R}_{\ge 0}\) and \((C_t)_{t \ge 0}\) a family of Borel subsets of \(\mathbb{R}\).

lemma pi_eq_generateFrom_bmPathCylinders :
    (inferInstance : MeasurableSpace (ℝ≥0 → ℝ))
      = MeasurableSpace.generateFrom bmPathCylinders

Uses 1 · Used by 1

Statement usesCylinder sets of path space

Used byMeasurable rectangles lie in the σ-algebra of cylinder rectangles

DefinitionRectangles of a Borel set and a path cylinder#✓fully proved

Write \(\mathbb{R}^{\mathbb{R}_{\ge 0}}\) for the space of functions \(\mathbb{R}_{\ge 0} \to \mathbb{R}\). These are the subsets of \(\mathbb{R} \times \mathbb{R}^{\mathbb{R}_{\ge 0}}\) of the form \(U \times \{f : f(t) \in V_t \text{ for all } t \in S\}\), where \(U \subseteq \mathbb{R}\) is a Borel set, \(S \subset \mathbb{R}_{\ge 0}\) is a finite set, and each \(V_t \subseteq \mathbb{R}\) is a Borel set.

def bmCylRectangles : Set (Set (ℝ × (ℝ≥0 → ℝ))) :=
  {T | ∃ (U : Set ℝ) (S : Finset ℝ≥0) (V : ℝ≥0 → Set ℝ), MeasurableSet U ∧
    (∀ t, MeasurableSet (V t)) ∧ T = U ×ˢ ⋂ t ∈ S, {f | f t ∈ V t}}

Used by 4

Used byRectangles of a Borel set and a path cylinder form a π-system · Measurable rectangles lie in the σ-algebra of cylinder rectangles · The pair-section identity for measurable sets · Cylinder rectangles generate the product σ-algebra

LemmaRectangles of a Borel set and a path cylinder form a π-system#✓fully proved

Consider the subsets of \(\mathbb{R} \times \mathbb{R}^{\mathbb{R}_{\ge 0}}\) of the form \(U \times \bigcap_{t \in S} \{f \in \mathbb{R}^{\mathbb{R}_{\ge 0}} : f(t) \in V_t\}\), where \(U \subseteq \mathbb{R}\) is Borel, \(S \subseteq \mathbb{R}_{\ge 0}\) is finite and every \(V_t \subseteq \mathbb{R}\) is Borel. They form a π-system: whenever two of them have nonempty intersection, the intersection is again of this form.

lemma isPiSystem_bmCylRectangles : IsPiSystem bmCylRectangles

Uses 1 · Used by 1

Statement usesRectangles of a Borel set and a path cylinder

Used byThe pair-section identity for measurable sets

LemmaMeasurable rectangles lie in the σ-algebra of cylinder rectangles#✓fully proved

Let \(U \subseteq \mathbb{R}\) be a Borel set and let \(V\) be a set of paths \(f : \mathbb{R}_{\ge 0} \to \mathbb{R}\) that is measurable for the product σ-algebra. Then \(U \times V\) belongs to the σ-algebra on \(\mathbb{R} \times (\mathbb{R}_{\ge 0} \to \mathbb{R})\) generated by the cylinder rectangles, the sets \(U' \times \{f : f(t) \in C_t \text{ for all } t \in S\}\) with \(U'\) Borel, \(S\) a finite subset of \(\mathbb{R}_{\ge 0}\) and \((C_t)_{t \ge 0}\) a family of Borel sets.

This is Dynkin's theorem applied to the cylinder π-system on path space.

lemma mem_generateFrom_bmCylRectangles {V : Set (ℝ≥0 → ℝ)} (hV : MeasurableSet V)
    (U : Set ℝ) (hU : MeasurableSet U) :
    MeasurableSet[MeasurableSpace.generateFrom bmCylRectangles] (U ×ˢ V)

Uses 4 · Used by 1

Statement usesRectangles of a Borel set and a path cylinder

Proof usesCylinder sets of path space · Path cylinders form a π-system · Cylinders generate the product σ-algebra on path space

Used byCylinder rectangles generate the product σ-algebra

LemmaCylinder rectangles generate the product σ-algebra#✓fully proved

The product σ-algebra on \(\mathbb{R} \times (\mathbb{R}_{\ge 0} \to \mathbb{R})\), where the path space carries its product σ-algebra, equals the σ-algebra generated by the cylinder rectangles, the sets \(U \times \{f : f(t) \in V_t \text{ for all } t \in S\}\) with \(U\) Borel, \(S\) a finite subset of \(\mathbb{R}_{\ge 0}\) and \((V_t)_{t \ge 0}\) a family of Borel subsets of \(\mathbb{R}\).

lemma prod_eq_generateFrom_bmCylRectangles :
    (inferInstance : MeasurableSpace (ℝ × (ℝ≥0 → ℝ)))
      = MeasurableSpace.generateFrom bmCylRectangles

Uses 3 · Used by 1

Statement usesRectangles of a Borel set and a path cylinder

Proof usesEvaluation events are measurable · Measurable rectangles lie in the σ-algebra of cylinder rectangles

Used byThe pair-section identity for measurable sets

DefinitionThe process value paired with its centered future path#✓fully proved

For a real process \((B_t)_{t \ge 0}\) on \(\Omega\) indexed by \(t \in \mathbb{R}_{\ge 0}\) and a time \(s \ge 0\), this is the map \(\Omega \to \mathbb{R} \times \mathbb{R}^{\mathbb{R}_{\ge 0}}\) sending \(\omega\) to the pair consisting of \(B_s(\omega)\) and the path \(t \mapsto B_{s+t}(\omega) - B_s(\omega)\).

noncomputable def bmPair (B : ℝ≥0 → Ω → ℝ) (s : ℝ≥0) : Ω → ℝ × (ℝ≥0 → ℝ) :=
  fun ω => (B s ω, bmCenteredShift B s ω)

Uses 1 · Used by 5

Statement usesCentered shifted path

Used byTranslating the centered future path recovers the shifted path · Nonnegative integrals of future path functionals over present events · Measurability of the pair map · The pair-section identity for measurable sets · The pair identity on cylinder rectangles

DefinitionTranslating a path by a constant#✓fully proved

The map sending a pair \((x, f)\), with \(x \in \mathbb{R}\) and \(f : \mathbb{R}_{\ge 0} \to \mathbb{R}\), to the path \(t \mapsto x + f(t)\).

noncomputable def bmPhi : ℝ × (ℝ≥0 → ℝ) → (ℝ≥0 → ℝ) :=
  fun p t => p.1 + p.2 t

Used by 3

Used byTranslating the centered future path recovers the shifted path · Nonnegative integrals of future path functionals over present events · Translation of paths is measurable

LemmaMeasurability of the pair map#✓fully proved

Let \(B = (B_t)_{t \ge 0}\) be a real process on a measurable space \(\Omega\), adapted to a filtration \((\mathcal{F}_t)_{t \ge 0}\) of its σ-algebra, and give the space \(\mathbb{R}^{[0, \infty)}\) of real paths indexed by \(t \ge 0\) the product σ-algebra. For every \(s \ge 0\), the map from \(\Omega\) to \(\mathbb{R} \times \mathbb{R}^{[0, \infty)}\) sending \(\omega\) to the pair of \(B_s(\omega)\) and the centered shifted path \(t \mapsto B_{s+t}(\omega) - B_s(\omega)\) is measurable.

lemma measurable_bmPair (hAd : BmAdapted B ℱ) (s : ℝ≥0) :
    Measurable (bmPair B s)

Uses 4 · Used by 1

Statement usesAdapted real process · The process value paired with its centered future path

Proof usesCentered shifted path · Measurability of the centered shifted path

Used byThe pair-section identity for measurable sets

LemmaTranslation of paths is measurable#✓fully proved

Give the space \(\mathbb{R}^{[0, \infty)}\) of real paths indexed by \(t \ge 0\) the product σ-algebra. The map from \(\mathbb{R} \times \mathbb{R}^{[0, \infty)}\) to \(\mathbb{R}^{[0, \infty)}\) sending \((x, f)\) to the path \(t \mapsto x + f(t)\) is measurable.

lemma measurable_bmPhi : Measurable bmPhi

Uses 1 · Used by 3

Statement usesTranslating a path by a constant

Used byNonnegative integrals of future path functionals over present events · The path expectation is measurable in the starting point · Nonnegative translated integrals against the centered law are measurable

LemmaTranslating the centered future path recovers the shifted path#✓fully proved

For a real process \((B_t)_{t \ge 0}\) on \(\Omega\) indexed by \(t \in \mathbb{R}_{\ge 0}\), a time \(s \ge 0\) and \(\omega \in \Omega\), translating the centered shifted path \(t \mapsto B_{s+t}(\omega) - B_s(\omega)\) by the constant \(B_s(\omega)\) gives the shifted path \(t \mapsto B_{s+t}(\omega)\).

lemma bmPhi_bmPair (s : ℝ≥0) (ω : Ω) :
    bmPhi (bmPair B s ω) = bmShifted B s ω

Uses 3 · Used by 1

Statement usesThe process value paired with its centered future path · Translating a path by a constant · Shifted path of a process

Used byNonnegative integrals of future path functionals over present events

LemmaSection measures of the centered law are measurable#✓fully proved

Let \(B = (B_t)_{t \ge 0}\) be a real process on a probability space \((\Omega, \mu)\), let \(s \ge 0\), and let \(\nu_s\) be the law of the centered shifted path \(t \mapsto B_{s+t} - B_s\) on the space \(\mathbb{R}^{[0, \infty)}\) of real paths indexed by \(t \ge 0\), with its product σ-algebra. For every measurable set \(T \subseteq \mathbb{R} \times \mathbb{R}^{[0, \infty)}\), the function \(x \mapsto \nu_s(\{f : (x, f) \in T\})\) from \(\mathbb{R}\) to \([0, \infty]\) is measurable.

lemma measurable_section_bmCenteredLaw [IsProbabilityMeasure μ] {s : ℝ≥0}
    {T : Set (ℝ × (ℝ≥0 → ℝ))} (hT : MeasurableSet T) :
    Measurable fun x : ℝ => bmCenteredLaw B μ s {f | (x, f) ∈ T}

Uses 2 · Used by 2

Statement usesLaw of the centered shifted path

Proof usesCentered shifted path

Used byNonnegative integrals of future path functionals over present events · The pair-section identity for measurable sets

LemmaThe pair identity on cylinder rectangles#✓fully proved

Let \(\mu\) be a probability measure and let \((B_t)_{t \ge 0}\) be a real process adapted to a filtration \((\mathcal{F}_t)_{t \ge 0}\) such that \(B_t - B_s\) is independent of \(\mathcal{F}_s\) under \(\mu\) whenever \(s \le t\). Fix \(s \in \mathbb{R}_{\ge 0}\), let \(W^s\) be the centered shifted path \(t \mapsto B_{s+t} - B_s\) and let \(\nu_s\) be its law under \(\mu\). Let \(U \subseteq \mathbb{R}\) be Borel, let \(S \subseteq \mathbb{R}_{\ge 0}\) be finite, let \((V_t)_{t \ge 0}\) be Borel subsets of \(\mathbb{R}\), and let \(R = U \times \{f : f(t) \in V_t \text{ for all } t \in S\}\). Then for every \(A \in \mathcal{F}_s\),

\[\mu\big(A \cap \{(B_s, W^s) \in R\}\big) = \int_A \nu_s\big(\{f : (B_s(\omega), f) \in R\}\big)\,d\mu(\omega).\]

The left side factors by the independence of \(W^s\) from \(\mathcal{F}_s\), and the section on the right is empty unless \(B_s(\omega) \in U\).

lemma pair_section_rectangle (hAd : BmAdapted B ℱ)
    (hInd : BmIndepIncrements B ℱ μ) [IsProbabilityMeasure μ] (s : ℝ≥0)
    (U : Set ℝ) (hU : MeasurableSet U) (S : Finset ℝ≥0) (V : ℝ≥0 → Set ℝ)
    (hV : ∀ t, MeasurableSet (V t)) (A : Set Ω) (hA : MeasurableSet[ℱ s] A) :
    μ (A ∩ bmPair B s ⁻¹' (U ×ˢ ⋂ t ∈ S, {f | f t ∈ V t}))
      = ∫⁻ ω in A, bmCenteredLaw B μ s
          {f | (B s ω, f) ∈ U ×ˢ ⋂ t ∈ S, {f | f t ∈ V t}} ∂μ

Uses 8 · Used by 1

Statement usesAdapted real process · Independent increments with respect to a filtration · Law of the centered shifted path · The process value paired with its centered future path

Proof usesCentered shifted path · Independence of the centered future path from the present · Evaluation events are measurable · Measurability of the centered shifted path

Used byThe pair-section identity for measurable sets

LemmaThe pair-section identity for measurable sets#✓fully proved

Let \(\mu\) be a probability measure and let \((B_t)_{t \ge 0}\) be a real process adapted to a filtration \((\mathcal{F}_t)_{t \ge 0}\) such that \(B_t - B_s\) is independent of \(\mathcal{F}_s\) under \(\mu\) whenever \(s \le t\). Fix \(s \in \mathbb{R}_{\ge 0}\), let \(W^s\) be the centered shifted path \(t \mapsto B_{s+t} - B_s\) and let \(\nu_s\) be its law under \(\mu\). Then for every set \(T \subseteq \mathbb{R} \times (\mathbb{R}_{\ge 0} \to \mathbb{R})\) that is measurable for the product σ-algebra and every \(A \in \mathcal{F}_s\),

\[\mu\big(A \cap \{(B_s, W^s) \in T\}\big) = \int_A \nu_s\big(\{f : (B_s(\omega), f) \in T\}\big)\,d\mu(\omega).\]

The proof is Dynkin's theorem over cylinder rectangles.

lemma pair_section_lintegral (hAd : BmAdapted B ℱ)
    (hInd : BmIndepIncrements B ℱ μ) [IsProbabilityMeasure μ] (s : ℝ≥0)
    {T : Set (ℝ × (ℝ≥0 → ℝ))} (hT : MeasurableSet T) (A : Set Ω)
    (hA : MeasurableSet[ℱ s] A) :
    μ (A ∩ bmPair B s ⁻¹' T)
      = ∫⁻ ω in A, bmCenteredLaw B μ s {f | (B s ω, f) ∈ T} ∂μ

Uses 11 · Used by 1

Statement usesAdapted real process · Independent increments with respect to a filtration · Law of the centered shifted path · The process value paired with its centered future path

Proof usesCentered shifted path · Rectangles of a Borel set and a path cylinder · Rectangles of a Borel set and a path cylinder form a π-system · Measurability of the pair map · Section measures of the centered law are measurable · The pair identity on cylinder rectangles · Cylinder rectangles generate the product σ-algebra

Used byNonnegative integrals of future path functionals over present events

LemmaNonnegative translated integrals against the centered law are measurable#✓fully proved

Let \(B = (B_t)_{t \ge 0}\) be a real process on a probability space \((\Omega, \mu)\), let \(s \ge 0\), and let \(\nu_s\) be the law of the centered shifted path \(t \mapsto B_{s+t} - B_s\) on the space \(\mathbb{R}^{[0, \infty)}\) of real paths indexed by \(t \ge 0\), with its product σ-algebra. For every measurable \(Y : \mathbb{R}^{[0, \infty)} \to [0, \infty]\), the function \(x \mapsto \int Y(x + g) \, d\nu_s(g)\) on \(\mathbb{R}\) is measurable, where \(x + g\) is the path \(t \mapsto x + g(t)\).

lemma measurable_lintegral_bmPhi [IsProbabilityMeasure μ] {s : ℝ≥0}
    {Y : (ℝ≥0 → ℝ) → ENNReal} (hY : Measurable Y) :
    Measurable fun x : ℝ => ∫⁻ g, Y (fun t => x + g t) ∂(bmCenteredLaw B μ s)

Uses 3 · Used by 2

Statement usesLaw of the centered shifted path

Proof usesCentered shifted path · Translation of paths is measurable

Used bySet integrals of the path expectation · Nonnegative integrals of future path functionals over present events

LemmaNonnegative integrals of future path functionals over present events#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \((\mathcal{F}_t)_{t \ge 0}\) be a filtration indexed by \(\mathbb{R}_{\ge 0}\), and let \((B_t)_{t \ge 0}\) be a real-valued process that is adapted (each \(B_t\) is \(\mathcal{F}_t\)-measurable) and has independent increments (for \(u \le t\), the increment \(B_t - B_u\) is independent of \(\mathcal{F}_u\) under \(\mu\)). Fix \(s \ge 0\) and let \(\nu_s\) be the law under \(\mu\) of the centered shifted path \(\omega \mapsto (t \mapsto B_{s+t}(\omega) - B_s(\omega))\) on \(\mathbb{R}^{\mathbb{R}_{\ge 0}}\) with the product σ-algebra. Then for every measurable \(Y : \mathbb{R}^{\mathbb{R}_{\ge 0}} \to [0, \infty]\) and every \(A \in \mathcal{F}_s\),

\[\int_A Y\big((B_{s+t}(\omega))_{t \ge 0}\big) \, d\mu(\omega) = \int_A \int Y\big(t \mapsto B_s(\omega) + g(t)\big) \, d\nu_s(g) \, d\mu(\omega),\]

where all integrals are Lebesgue integrals of \([0, \infty]\)-valued functions.

lemma independent_increments_lintegral_shift (hAd : BmAdapted B ℱ)
    (hInd : BmIndepIncrements B ℱ μ) [IsProbabilityMeasure μ] (s : ℝ≥0)
    {Y : (ℝ≥0 → ℝ) → ENNReal} (hY : Measurable Y) (A : Set Ω)
    (hA : MeasurableSet[ℱ s] A) :
    ∫⁻ ω in A, Y (bmShifted B s ω) ∂μ
      = ∫⁻ ω in A, (∫⁻ g, Y (fun t => B s ω + g t) ∂(bmCenteredLaw B μ s)) ∂μ

Uses 12 · Used by 1

Statement usesAdapted real process · Independent increments with respect to a filtration · Law of the centered shifted path · Shifted path of a process

Proof usesThe process value paired with its centered future path · Translating a path by a constant · Translating the centered future path recovers the shifted path · Translation of paths is measurable · Measurability of the shifted path · Nonnegative translated integrals against the centered law are measurable · Section measures of the centered law are measurable · The pair-section identity for measurable sets

Used bySet integrals of the path expectation

LemmaThe path expectation is measurable in the starting point#✓fully proved

Let \(B = (B_t)_{t \ge 0}\) be a real process on a probability space \((\Omega, \mu)\), let \(s \ge 0\), and let \(\nu_s\) be the law of the centered shifted path \(t \mapsto B_{s+t} - B_s\) on the space \(\mathbb{R}^{[0, \infty)}\) of real paths indexed by \(t \ge 0\), with its product σ-algebra. For every measurable \(Y : \mathbb{R}^{[0, \infty)} \to \mathbb{R}\), the function \(x \mapsto \int Y(x + f) \, d\nu_s(f)\) on \(\mathbb{R}\) is measurable, where \(x + f\) is the path \(t \mapsto x + f(t)\).

lemma measurable_bmPathExpectation [IsProbabilityMeasure μ] {s : ℝ≥0}
    {Y : (ℝ≥0 → ℝ) → ℝ} (hY : Measurable Y) :
    Measurable fun x : ℝ => bmPathExpectation B μ s Y x

Uses 4 · Used by 1

Statement usesTime-dependent path expectation

Proof usesLaw of the centered shifted path · Centered shifted path · Translation of paths is measurable

Used byConditional expectation of a future path functional

LemmaBound on the path expectation#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \((B_t)_{t \ge 0}\) be a real process on \(\Omega\) indexed by \(t \in \mathbb{R}_{\ge 0}\), let \(s \ge 0\), and let \(\nu_s\) be the law under \(\mu\) of the path \(\omega \mapsto (t \mapsto B_{s+t}(\omega) - B_s(\omega))\). If \(Y\) is a measurable real function on paths \(\mathbb{R}_{\ge 0} \to \mathbb{R}\) with \(|Y(p)| \le C\) for every path \(p\), then for every \(x \in \mathbb{R}\) the path expectation \(E_s Y(x) = \int Y(t \mapsto x + f(t))\, d\nu_s(f)\) satisfies \(|E_s Y(x)| \le C\).

lemma bmPathExpectation_bound [IsProbabilityMeasure μ] {s : ℝ≥0} {Y : (ℝ≥0 → ℝ) → ℝ}
    (hY : Measurable Y) {C : ℝ} (hYb : ∀ p, |Y p| ≤ C) (x : ℝ) :
    |bmPathExpectation B μ s Y x| ≤ C

Uses 3 · Used by 1

Statement usesTime-dependent path expectation

Proof usesLaw of the centered shifted path · Centered shifted path

Used byConditional expectation of a future path functional

LemmaSet integrals of the path expectation#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \((\mathcal{F}_t)_{t \ge 0}\) be a filtration of the σ-algebra of \(\Omega\) indexed by \(\mathbb{R}_{\ge 0}\), and let \((B_t)_{t \ge 0}\) be a real process such that each \(B_t\) is \(\mathcal{F}_t\)-measurable and, for all \(u \le t\), the increment \(B_t - B_u\) is independent of \(\mathcal{F}_u\) under \(\mu\). Let \(s \ge 0\), let \(Y\) be a measurable real function on paths \(\mathbb{R}_{\ge 0} \to \mathbb{R}\) with \(|Y(p)| \le C\) for every path \(p\), and let \(A \in \mathcal{F}_s\). Write \(\nu_s\) for the law under \(\mu\) of \(\omega \mapsto (t \mapsto B_{s+t}(\omega) - B_s(\omega))\), \(E_s Y(x) = \int Y(t \mapsto x + f(t))\, d\nu_s(f)\) for \(x \in \mathbb{R}\), and \(\theta_s \omega\) for the shifted path \(t \mapsto B_{s+t}(\omega)\). Then

\[ \int_A E_s Y(B_s(\omega))\, d\mu(\omega) = \int_A Y^+(\theta_s \omega)\, d\mu(\omega) - \int_A Y^-(\theta_s \omega)\, d\mu(\omega), \]

where \(Y^+ = \max(Y, 0)\), \(Y^- = \max(-Y, 0)\), and each integral on the right is the integral of a nonnegative function, taken in \([0, \infty]\) and then converted to a real number.

lemma bmPathExpectation_setIntegral (hAd : BmAdapted B ℱ)
    (hInd : BmIndepIncrements B ℱ μ) [IsProbabilityMeasure μ] (s : ℝ≥0)
    {Y : (ℝ≥0 → ℝ) → ℝ} (hY : Measurable Y) {C : ℝ} (hYb : ∀ p, |Y p| ≤ C)
    (A : Set Ω) (hA : MeasurableSet[ℱ s] A) :
    ∫ ω in A, bmPathExpectation B μ s Y (B s ω) ∂μ
      = (∫⁻ ω in A, ENNReal.ofReal (Y (bmShifted B s ω)) ∂μ).toReal
        - (∫⁻ ω in A, ENNReal.ofReal (-Y (bmShifted B s ω)) ∂μ).toReal

Uses 8 · Used by 1

Statement usesAdapted real process · Independent increments with respect to a filtration · Time-dependent path expectation · Shifted path of a process

Proof usesLaw of the centered shifted path · Centered shifted path · Nonnegative integrals of future path functionals over present events · Nonnegative translated integrals against the centered law are measurable

Used byBounded integrals of future path functionals over present events

LemmaBounded integrals of future path functionals over present events#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \((\mathcal{F}_t)_{t \ge 0}\) be a filtration indexed by \(\mathbb{R}_{\ge 0}\), and let \((B_t)_{t \ge 0}\) be a real-valued process that is adapted (each \(B_t\) is \(\mathcal{F}_t\)-measurable) and has independent increments (for \(u \le t\), the increment \(B_t - B_u\) is independent of \(\mathcal{F}_u\) under \(\mu\)). Fix \(s \ge 0\) and let \(\nu_s\) be the law under \(\mu\) of the centered shifted path \(\omega \mapsto (t \mapsto B_{s+t}(\omega) - B_s(\omega))\) on \(\mathbb{R}^{\mathbb{R}_{\ge 0}}\) with the product σ-algebra. Let \(Y : \mathbb{R}^{\mathbb{R}_{\ge 0}} \to \mathbb{R}\) be measurable with \(|Y(p)| \le C\) for every path \(p\), for some real \(C\), and for \(x \in \mathbb{R}\) put \(\Phi_s(x) = \int Y(t \mapsto x + f(t)) \, d\nu_s(f)\). Then for every \(A \in \mathcal{F}_s\),

\[\int_A Y\big((B_{s+t}(\omega))_{t \ge 0}\big) \, d\mu(\omega) = \int_A \Phi_s(B_s(\omega)) \, d\mu(\omega).\]

lemma independent_increments_setIntegral (hAd : BmAdapted B ℱ)
    (hInd : BmIndepIncrements B ℱ μ) [IsProbabilityMeasure μ] (s : ℝ≥0)
    {Y : (ℝ≥0 → ℝ) → ℝ} (hY : Measurable Y) {C : ℝ} (hYb : ∀ p, |Y p| ≤ C)
    (A : Set Ω) (hA : MeasurableSet[ℱ s] A) :
    ∫ ω in A, Y (bmShifted B s ω) ∂μ
      = ∫ ω in A, bmPathExpectation B μ s Y (B s ω) ∂μ

Uses 6 · Used by 1

Statement usesAdapted real process · Independent increments with respect to a filtration · Time-dependent path expectation · Shifted path of a process

Proof usesSet integrals of the path expectation · Measurability of the shifted path

Used byConditional expectation of a future path functional

LemmaConditional expectation of a future path functional#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\), let \((\mathcal{F}_t)_{t \ge 0}\) be a filtration indexed by \(\mathbb{R}_{\ge 0}\), and let \((B_t)_{t \ge 0}\) be a real-valued process that is adapted (each \(B_t\) is \(\mathcal{F}_t\)-measurable) and has independent increments (for \(u \le t\), the increment \(B_t - B_u\) is independent of \(\mathcal{F}_u\) under \(\mu\)). Fix \(s \ge 0\) and let \(\nu_s\) be the law under \(\mu\) of the centered shifted path \(\omega \mapsto (t \mapsto B_{s+t}(\omega) - B_s(\omega))\) on \(\mathbb{R}^{\mathbb{R}_{\ge 0}}\) with the product σ-algebra. Let \(Y : \mathbb{R}^{\mathbb{R}_{\ge 0}} \to \mathbb{R}\) be measurable with \(|Y(p)| \le C\) for every path \(p\), for some real \(C\), and for \(x \in \mathbb{R}\) put \(\Phi_s(x) = \int Y(t \mapsto x + f(t)) \, d\nu_s(f)\). Then, \(\mu\)-almost everywhere,

\[\mathbb{E}_\mu\big[\, Y\big((B_{s+t})_{t \ge 0}\big) \bigm| \mathcal{F}_s \big] = \Phi_s(B_s).\]

The function \(\Phi_s\) is computed from the law of the increments after time \(s\), so it may depend on \(s\).

lemma independent_increments_condExp (hAd : BmAdapted B ℱ)
    (hInd : BmIndepIncrements B ℱ μ) [IsProbabilityMeasure μ] (s : ℝ≥0)
    {Y : (ℝ≥0 → ℝ) → ℝ} (hY : Measurable Y) {C : ℝ} (hYb : ∀ p, |Y p| ≤ C) :
    μ[fun ω => Y (bmShifted B s ω) | ℱ s] =ᵐ[μ]
      fun ω => bmPathExpectation B μ s Y (B s ω)

Uses 8

Statement usesAdapted real process · Independent increments with respect to a filtration · Time-dependent path expectation · Shifted path of a process

Proof usesBound on the path expectation · Bounded integrals of future path functionals over present events · The path expectation is measurable in the starting point · Measurability of the shifted path

48 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.