Blumenthal zero–one law

DefinitionGerm sigma-algebra at time zero#✓fully proved

The germ σ-algebra at 0 of a filtration 𝓕 indexed by NNReal, defined as the intersection ⨅_{t > 0} 𝓕_t. For Brownian motion this is the 𝓕_0^+ σ-algebra of events observable "immediately after" time 0. Ported verbatim from v1/Atlas/TheoryOfProbability/code/Blumenthal01.lean.

@[reducible]
def germSigmaAlgebraZero {Ω : Type*} {m : MeasurableSpace Ω} (𝓕 : Filtration NNReal m) :
    MeasurableSpace Ω :=
  ⨅ t > (0 : NNReal), 𝓕 t

Used by 2

Used byGerm sigma-algebra lies in every positive-time level · Germ sigma-algebra of the natural filtration

StructureContinuous process with independent increments#✓fully proved

A continuous process B : NNReal → Ω → E with independent increments, started at x and adapted to 𝓕. The measure is a probability measure, B 0 = x a.e., each increment after s is independent of 𝓕 s, and a.e. paths are continuous. These are the five meaningful fields of the archived v1 specification; its tautological pushforward-law field is omitted. No Gaussian-law or stationary-increment condition is encoded.

structure IsContinuousIndependentIncrementProcess
    {Ω : Type*} {m : MeasurableSpace Ω} {E : Type*}
    [MeasurableSpace E] [AddCommGroup E] [TopologicalSpace E]
    (B : NNReal → Ω → E) (𝓕 : Filtration NNReal m) (μ : Measure Ω) (x : E) : Prop where
  isProbabilityMeasure : IsProbabilityMeasure μ
  start : ∀ᵐ ω ∂μ, B 0 ω = x
  adapted : Adapted 𝓕 (fun t => B t)
  indep_incr : ∀ s t : NNReal, s < t →
    Indep (𝓕 s) (MeasurableSpace.comap (fun ω => B t ω - B s ω) inferInstance) μ
  continuous_path : ∀ᵐ ω ∂μ, Continuous (fun t : NNReal => B t ω)

Used by 3

Used byCoordinates of a continuous independent-increment process are measurable · Natural filtration is the smallest adapted filtration · Blumenthal zero-one law

TheoremCoordinates of a continuous independent-increment process are measurable#✓fully proved

Each coordinate of the adapted continuous process is measurable.

theorem IsContinuousIndependentIncrementProcess.measurable
    {Ω : Type*} {m : MeasurableSpace Ω} {E : Type*}
    [MeasurableSpace E] [AddCommGroup E] [TopologicalSpace E]
    {B : NNReal → Ω → E} {𝓕 : Filtration NNReal m} {μ : Measure Ω} {x : E}
    (hBM : IsContinuousIndependentIncrementProcess B 𝓕 μ x) (t : NNReal) :
    Measurable (B t)

Uses 1 · Used by 1

Statement usesContinuous process with independent increments

Used byBlumenthal zero-one law

DefinitionNatural filtration of a process#✓fully proved

The natural filtration of a process: 𝓕^nat_t = σ(B_u : u ≤ t). Unlike Mathlib's Filtration.natural, this is built from measurability rather than strong measurability, which is all that is available from adaptedness.

def naturalFiltration {Ω : Type*} {m : MeasurableSpace Ω} {E : Type*} [MeasurableSpace E]
    (B : NNReal → Ω → E) (hB : ∀ t, Measurable (B t)) : Filtration NNReal m where
  seq t := ⨆ (u : NNReal) (_ : u ≤ t), MeasurableSpace.comap (B u) inferInstance
  mono' := by
    intro a b hab
    show (⨆ (u : NNReal) (_ : u ≤ a), MeasurableSpace.comap (B u) inferInstance) ≤ _
    apply iSup₂_le
    intro u hu
    exact le_iSup_of_le u (le_iSup_of_le (le_trans hu hab) le_rfl)
  le' t := by
    show (⨆ (u : NNReal) (_ : u ≤ t), MeasurableSpace.comap (B u) inferInstance) ≤ _
    apply iSup₂_le
    intro u hu
    exact measurable_iff_comap_le.mp (hB u)

Used by 4

Used byProcess is measurable for its natural filtration at later times · Natural filtration is the smallest adapted filtration · Germ sigma-algebra of the natural filtration · Blumenthal zero-one law

DefinitionGerm sigma-algebra of the natural filtration#✓fully proved

The germ σ-algebra of the natural filtration of B.

@[instance_reducible]
def naturalGerm {Ω : Type*} {m : MeasurableSpace Ω} {E : Type*} [MeasurableSpace E]
    (B : NNReal → Ω → E) (hB : ∀ t, Measurable (B t)) : MeasurableSpace Ω :=
  germSigmaAlgebraZero (naturalFiltration B hB)

Uses 2 · Used by 1

Statement usesGerm sigma-algebra at time zero · Natural filtration of a process

Used byBlumenthal zero-one law

TheoremProcess is measurable for its natural filtration at later times#✓fully proved

Each B u is measurable with respect to the natural filtration at any later time t.

theorem measurable_naturalFiltration {Ω : Type*} {m : MeasurableSpace Ω} {E : Type*}
    [MeasurableSpace E] {B : NNReal → Ω → E} (hB : ∀ t, Measurable (B t)) {t u : NNReal}
    (hu : u ≤ t) : Measurable[naturalFiltration B hB t] (B u)

Uses 1 · Used by 1

Statement usesNatural filtration of a process

Used byBlumenthal zero-one law

TheoremNatural filtration is the smallest adapted filtration#✓fully proved

The natural filtration is contained in any filtration to which B is adapted.

theorem naturalFiltration_le {Ω : Type*} {m : MeasurableSpace Ω} {E : Type*}
    [MeasurableSpace E] [AddCommGroup E] [TopologicalSpace E]
    {B : NNReal → Ω → E} {𝓕 : Filtration NNReal m} {μ : Measure Ω} {x : E}
    (hBM : IsContinuousIndependentIncrementProcess B 𝓕 μ x)
    (hB : ∀ t, Measurable (B t)) (t : NNReal) :
    naturalFiltration B hB t ≤ 𝓕 t

Uses 2 · Used by 1

Statement usesContinuous process with independent increments · Natural filtration of a process

Used byBlumenthal zero-one law

TheoremGerm sigma-algebra lies in every positive-time level#✓fully proved

The germ σ-algebra is contained in every positive-time component of the filtration.

theorem germ_le_of_pos {Ω : Type*} {m : MeasurableSpace Ω} (𝓕 : Filtration NNReal m)
    {t : NNReal} (ht : 0 < t) : germSigmaAlgebraZero 𝓕 ≤ 𝓕 t

Uses 1 · Used by 1

Statement usesGerm sigma-algebra at time zero

Used byBlumenthal zero-one law

TheoremBlumenthal zero-one law#✓fully proved

Every event in the natural germ of a continuous process with independent increments and a deterministic a.e. initial value has probability 0 or 1. This general form includes the classical Brownian natural-filtration law.

theorem zero_one_naturalGerm
    {Ω : Type*} {m : MeasurableSpace Ω} {E : Type*} [MeasurableSpace E] [AddCommGroup E]
    [PseudoMetricSpace E] [BorelSpace E] [SecondCountableTopology E] [ContinuousAdd E]
    [ContinuousSub E]
    {B : NNReal → Ω → E} {𝓕 : Filtration NNReal m} {μ : Measure Ω} {x : E}
    (hBM : IsContinuousIndependentIncrementProcess B 𝓕 μ x) (hB : ∀ t, Measurable (B t))
    {A : Set Ω} (hA : MeasurableSet[naturalGerm B hB] A) :
    μ A = 0 ∨ μ A = 1

Uses 7

Statement usesContinuous process with independent increments · Germ sigma-algebra of the natural filtration

Proof usesCoordinates of a continuous independent-increment process are measurable · Germ sigma-algebra lies in every positive-time level · Process is measurable for its natural filtration at later times · Natural filtration of a process · Natural filtration is the smallest adapted filtration

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.