@[reducible]

def ProbabilityTheory.germSigmaAlgebraZero {Ω : Type u_1} {m : MeasurableSpace Ω} (𝓕 : MeasureTheory.Filtration NNReal m) : MeasurableSpace Ω

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; Blumenthal's 0-1 law states that every such event has probability 0 or 1.

theorem ProbabilityTheory.germSigmaAlgebraZero_eq_iInf {Ω : Type u_1} {m : MeasurableSpace Ω} (𝓕 : MeasureTheory.Filtration NNReal m) : germSigmaAlgebraZero 𝓕 = ⨅ (t : NNReal), ⨅ (_ : t > 0), ↑𝓕 t

Definitional unfolding: germSigmaAlgebraZero 𝓕 equals the indexed infimum ⨅ t > 0, 𝓕 t.

structure ProbabilityTheory.IsBrownianMotion {Ω : Type u_1} {m : MeasurableSpace Ω} {E : Type u_2} [MeasurableSpace E] [AddCommGroup E] [TopologicalSpace E] (B : NNReal → Ω → E) (𝓕 : MeasureTheory.Filtration NNReal m) (μ : MeasureTheory.Measure Ω) (x : E) : Prop

An abstract specification of a Brownian motion B : NNReal → Ω → E started at x ∈ E, adapted to a filtration 𝓕 on (Ω, m, μ). The fields require that μ is a probability measure, B 0 = x almost surely, B is adapted, increments B_t - B_s are independent of 𝓕_s for s < t, each increment has some law on E (the Gaussian distribution in the standard case), and the sample paths t ↦ B_t ω are continuous for a.e. ω.

• isProbabilityMeasure : MeasureTheory.IsProbabilityMeasure μ
• start : ∀ᵐ (ω : Ω) ∂μ, B 0 ω = x
• adapted : MeasureTheory.Adapted 𝓕 fun (t : NNReal) => B t
• indep_incr (s t : NNReal) : s < t → Indep (↑𝓕 s) (MeasurableSpace.comap (fun (ω : Ω) => B t ω - B s ω) inferInstance) μ
• gaussian_incr (s t : NNReal) : s < t → ∃ (ν : MeasureTheory.Measure E), MeasureTheory.Measure.map (fun (ω : Ω) => B t ω - B s ω) μ = ν
• continuous_path : ∀ᵐ (ω : Ω) ∂μ, Continuous fun (t : NNReal) => B t ω

theorem ProbabilityTheory.germSigmaAlgebraZero_le_of_pos {Ω : Type u_1} {m : MeasurableSpace Ω} (𝓕 : MeasureTheory.Filtration NNReal m) {t : NNReal} (ht : 0 < t) : germSigmaAlgebraZero 𝓕 ≤ ↑𝓕 t

For any strictly positive time t, the germ σ-algebra at 0 is contained in 𝓕 t, since 𝓕 t appears as one of the terms in the infimum ⨅ s > 0, 𝓕 s.

theorem ProbabilityTheory.markov_germ_indep_filtration_at {Ω : Type u_2} {m : MeasurableSpace Ω} {E : Type u_3} [MeasurableSpace E] [AddCommGroup E] [TopologicalSpace E] (B : NNReal → Ω → E) (𝓕 : MeasureTheory.Filtration NNReal m) (μ : MeasureTheory.Measure Ω) (x : E) (hBM : IsBrownianMotion B 𝓕 μ x) (s : NNReal) (hs : 0 < s) : Indep (↑𝓕 s) (germSigmaAlgebraZero 𝓕) μ

For Brownian motion, every component 𝓕 s of the filtration (with s > 0) is independent of the germ σ-algebra at 0. This is a Markov-property consequence of the independent-increments property and is the main ingredient in the proof of Blumenthal's 0-1 law.

theorem ProbabilityTheory.germ_sigma_indep_self {Ω : Type u_1} {m : MeasurableSpace Ω} {E : Type u_2} [MeasurableSpace E] [AddCommGroup E] [TopologicalSpace E] (B : NNReal → Ω → E) (𝓕 : MeasureTheory.Filtration NNReal m) (μ : MeasureTheory.Measure Ω) (x : E) (hBM : IsBrownianMotion B 𝓕 μ x) {A : Set Ω} (hA : MeasurableSet A) : IndepSet A A μ

Any event A in the germ σ-algebra at 0 is independent of itself under μ. This is the key intermediate step in the proof of Blumenthal's 0-1 law: since germSigmaAlgebraZero 𝓕 ≤ 𝓕 1 and 𝓕 1 is independent of the germ σ-algebra (by markov_germ_indep_filtration_at), the germ σ-algebra is independent of itself, which forces μ(A) ∈ {0, 1}.

theorem ProbabilityTheory.blumenthal_zero_one {Ω : Type u_1} {m : MeasurableSpace Ω} {E : Type u_2} [MeasurableSpace E] [AddCommGroup E] [TopologicalSpace E] (B : NNReal → Ω → E) (𝓕 : MeasureTheory.Filtration NNReal m) (μ : MeasureTheory.Measure Ω) (x : E) (hBM : IsBrownianMotion B 𝓕 μ x) {A : Set Ω} (hA : MeasurableSet A) : μ A = 0 ∨ μ A = 1

Blumenthal's 0-1 law. If B is a Brownian motion started at x with filtration 𝓕, then every event A in the germ σ-algebra 𝓕_0^+ = ⋂_{t > 0} 𝓕_t has μ(A) ∈ {0, 1} (Durrett, Lecture 36). Proof: by germ_sigma_indep_self, A is independent of itself, so μ(A) = μ(A)².