structure TheoryOfProbability3.DecreasingFiltration (Ω : Type u_2) (m0 : MeasurableSpace Ω) : Type u_2

A decreasing filtration on (Ω, m0) is a sequence of sub-σ-algebras ℱ n ⊆ m0 that is antitone in n (i.e. ℱ 0 ⊇ ℱ 1 ⊇ ℱ 2 ⊇ ⋯). This is the natural index structure for backwards martingales, where conditioning σ-algebras shrink as n → ∞.

• seq : ℕ → MeasurableSpace Ω
• antitone' : Antitone ↑self
• le' (n : ℕ) : ↑self n ≤ m0

@[implicit_reducible]

instance TheoryOfProbability3.instCoeFunDecreasingFiltrationForallNatMeasurableSpace {Ω : Type u_1} {m0 : MeasurableSpace Ω} : CoeFun (DecreasingFiltration Ω m0) fun (x : DecreasingFiltration Ω m0) => ℕ → MeasurableSpace Ω

Allow a DecreasingFiltration to be applied as a function ℕ → MeasurableSpace Ω via its underlying sequence seq.

@[reducible]

def TheoryOfProbability3.DecreasingFiltration.tailAlgebra {Ω : Type u_1} {m0 : MeasurableSpace Ω} (ℱ : DecreasingFiltration Ω m0) : MeasurableSpace Ω

The tail σ-algebra of a decreasing filtration ℱ, defined as the intersection ⨅ n, ℱ n. This is the σ-algebra of events that lie in every ℱ n, i.e. the limit as the filtration shrinks.

theorem TheoryOfProbability3.DecreasingFiltration.tailAlgebra_le {Ω : Type u_1} {m0 : MeasurableSpace Ω} (ℱ : DecreasingFiltration Ω m0) : ℱ.tailAlgebra ≤ m0

The tail σ-algebra of a decreasing filtration is contained in the ambient σ-algebra m0.

theorem TheoryOfProbability3.DecreasingFiltration.tailAlgebra_le_seq {Ω : Type u_1} {m0 : MeasurableSpace Ω} (ℱ : DecreasingFiltration Ω m0) (n : ℕ) : ℱ.tailAlgebra ≤ ↑ℱ n

The tail σ-algebra is contained in every component ℱ n of the filtration.

structure TheoryOfProbability3.IsBackwardsMartingale {Ω : Type u_1} {m0 : MeasurableSpace Ω} (M : ℕ → Ω → ℝ) (ℱ : DecreasingFiltration Ω m0) (μ : MeasureTheory.Measure Ω) : Prop

A backwards martingale with respect to a decreasing filtration ℱ and measure μ is a process M : ℕ → Ω → ℝ such that M 0 is integrable, each M n is ℱ n-strongly measurable, and M n = μ[M 0 | ℱ n] μ-a.e. Equivalently, E(M n | ℱ n+1) = M n+1 for all n (with the filtration shrinking as n grows). This corresponds to the setting of Durrett's backwards martingale convergence theorem: X_{-∞} = lim_{n → -∞} X_n exists a.s. and in L¹.

• integrable_zero : MeasureTheory.Integrable (M 0) μ
• adapted (n : ℕ) : MeasureTheory.StronglyMeasurable (M n)
• condExp_ae_eq (n : ℕ) : M n =ᵐ[μ] μ[M 0 | ↑ℱ n]

theorem TheoryOfProbability3.IsBackwardsMartingale.integrable {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {M : ℕ → Ω → ℝ} {ℱ : DecreasingFiltration Ω m0} (hM : IsBackwardsMartingale M ℱ μ) (n : ℕ) : MeasureTheory.Integrable (M n) μ

Every term M n of a backwards martingale is integrable, since it is μ-a.e. equal to the integrable conditional expectation μ[M 0 | ℱ n].

theorem TheoryOfProbability3.IsBackwardsMartingale.uniformIntegrable {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {M : ℕ → Ω → ℝ} {ℱ : DecreasingFiltration Ω m0} (hM : IsBackwardsMartingale M ℱ μ) : MeasureTheory.UniformIntegrable M 1 μ

A backwards martingale is uniformly integrable in L¹: this follows from the standard fact that the family of conditional expectations {μ[M 0 | ℱ n]} of a single integrable function M 0 is uniformly integrable.

theorem TheoryOfProbability3.condExp_antitone_limit_eq {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (g : Ω → ℝ) (m : ℕ → MeasurableSpace Ω) (hm_le : ∀ (n : ℕ), m n ≤ m0) (hg : MeasureTheory.Integrable g μ) (h : Ω → ℝ) (hh_ae : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => μ[g | m n] ω) Filter.atTop (nhds (h ω))) (hh_int : MeasureTheory.Integrable h μ) (hh_meas : MeasureTheory.StronglyMeasurable h) : h =ᵐ[μ] μ[g | ⨅ (n : ℕ), m n]

Identification of the a.s. limit of conditional expectations along a decreasing sequence of σ-algebras. Suppose m n is any sequence of sub-σ-algebras of m0, g is integrable, and μ[g | m n] → h pointwise a.e. with h integrable and measurable with respect to the limit σ-algebra ⨅ n, m n. Then h = μ[g | ⨅ n, m n] μ-a.e. This is the key step needed to conclude Lévy's downward theorem from a.s. convergence of the conditional expectations.

theorem TheoryOfProbability3.condExp_antitone_ae_tendsto {Ω : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (g : Ω → ℝ) (m : ℕ → MeasurableSpace Ω) (hm_anti : Antitone m) (hm_le : ∀ (n : ℕ), m n ≤ m0) : ∃ (h : Ω → ℝ), MeasureTheory.StronglyMeasurable h ∧ MeasureTheory.Integrable h μ ∧ ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => μ[g | m n] ω) Filter.atTop (nhds (h ω))

Existence of an a.e. limit for conditional expectations along a decreasing sequence of σ-algebras. Given any integrable g and antitone m : ℕ → MeasurableSpace Ω with m n ≤ m0, there exists an integrable function h measurable with respect to ⨅ n, m n such that μ[g | m n] → h μ-a.e.

theorem TheoryOfProbability3.levy_downward_ae {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (g : Ω → ℝ) (m : ℕ → MeasurableSpace Ω) (hm_anti : Antitone m) (hm_le : ∀ (n : ℕ), m n ≤ m0) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => μ[g | m n] ω) Filter.atTop (nhds (μ[g | ⨅ (n : ℕ), m n] ω))

Lévy's downward theorem (a.s. form). For any g : Ω → ℝ and any antitone sequence of sub-σ-algebras m n ≤ m0, the conditional expectations μ[g | m n] converge μ-a.e. to the conditional expectation of g given the intersection σ-algebra ⨅ n, m n.

theorem TheoryOfProbability3.backwards_martingale_ae_tendsto {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {M : ℕ → Ω → ℝ} {ℱ : DecreasingFiltration Ω m0} (hM : IsBackwardsMartingale M ℱ μ) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => M n ω) Filter.atTop (nhds (μ[M 0 | ℱ.tailAlgebra] ω))

Backwards martingale convergence theorem (a.s. form). If M is a backwards martingale with respect to the decreasing filtration ℱ, then M n → μ[M 0 | ℱ.tailAlgebra] μ-almost surely as n → ∞. This is the content of Durrett's Theorem (Backwards martingales): with E(X_{n+1} | ℱ_n) = X_n for n ≤ 0 and ℱ_n increasing in n, the limit X_{-∞} = lim_{n → -∞} X_n exists a.s.