Backwards martingales and Lévy's downward theorem

TheoremLévy's downward theorem, almost sure convergence#✓fully proved

Let \((\Omega, \mathcal F, \mu)\) be a probability space, let \(\mathcal F_0 \supseteq \mathcal F_1 \supseteq \cdots\) be a decreasing sequence of sub-σ-algebras of \(\mathcal F\), and let \(\mathcal F_\infty = \bigcap_n \mathcal F_n\). For every function \(g : \Omega \to \mathbb R\), the conditional expectations \(\mathbb E[g \mid \mathcal F_n]\) converge to \(\mathbb E[g \mid \mathcal F_\infty]\) as \(n \to \infty\), \(\mu\)-almost everywhere.

No integrability hypothesis is needed: for a non-integrable \(g\) every conditional expectation is \(0\) by convention, and the statement is trivial.

theorem levy_downward_ae {g : Ω → ℝ} (m : ℕ → MeasurableSpace Ω)
    (hm : Antitone m) (hm0 : ∀ n, m n ≤ m0) :
    ∀ᵐ ω ∂μ, Tendsto (fun n => (μ[g | m n]) ω) atTop (𝓝 ((μ[g | ⨅ n, m n]) ω))

Used by 2

Used byBackwards martingale convergence theorem, almost sure convergence · Lévy's downward theorem in L¹

TheoremLévy's downward theorem in L¹#✓fully proved

Let \((\Omega, \mathcal F, \mu)\) be a probability space, let \(\mathcal F_0 \supseteq \mathcal F_1 \supseteq \cdots\) be a decreasing sequence of sub-σ-algebras of \(\mathcal F\), and let \(\mathcal F_\infty = \bigcap_n \mathcal F_n\). For every integrable function \(g : \Omega \to \mathbb R\), the \(L^1(\mu)\) norm \(\lVert \mathbb E[g \mid \mathcal F_n] - \mathbb E[g \mid \mathcal F_\infty] \rVert_1\) tends to \(0\) as \(n \to \infty\).

theorem levy_downward_tendsto_eLpNorm_one {g : Ω → ℝ} (m : ℕ → MeasurableSpace Ω)
    (hm : Antitone m) (hm0 : ∀ n, m n ≤ m0) (hg : Integrable g μ) :
    Tendsto (fun n => eLpNorm ((μ[g | m n]) - μ[g | ⨅ n, m n]) 1 μ) atTop (𝓝 0)

Uses 1

Proof usesLévy's downward theorem, almost sure convergence

DefinitionBackwards martingale#✓fully proved

Let \(\mu\) be a measure on a measurable space \((\Omega, \mathcal F)\) and let \((\mathcal F_n)_{n \ge 0}\) be a sequence of σ-algebras on \(\Omega\). A sequence of functions \(M_n : \Omega \to \mathbb R\) is a backwards martingale with respect to \((\mathcal F_n)\) and \(\mu\) if \(M_0\) is \(\mu\)-integrable and, for every \(n\), \(M_n = \mathbb E[M_0 \mid \mathcal F_n]\) \(\mu\)-almost everywhere.

Here \(\mathbb E[M_0 \mid \mathcal F_n]\) is the conditional expectation with respect to \(\mu\) when \(\mathcal F_n \subseteq \mathcal F\) and the restriction of \(\mu\) to \(\mathcal F_n\) is σ-finite, and is \(0\) by convention otherwise. The definition is used when \((\mathcal F_n)\) is a decreasing sequence of sub-σ-algebras, but it does not require this.

def IsBackwardsMartingale (M : ℕ → Ω → ℝ) (m : ℕ → MeasurableSpace Ω) (μ : Measure Ω) : Prop :=
  Integrable (M 0) μ ∧ ∀ n, M n =ᵐ[μ] μ[M 0 | m n]

Used by 6

Used byBackwards martingale convergence theorem, almost sure convergence · Backwards martingale convergence theorem in L¹ · Conditioning a backwards martingale on the next level · Terms of a backwards martingale are integrable · Conditional expectations form a backwards martingale · Backwards martingales are uniformly integrable

TheoremBackwards martingale convergence theorem, almost sure convergence#✓fully proved

Let \((\Omega, \mathcal F, \mu)\) be a probability space, let \(\mathcal F_0 \supseteq \mathcal F_1 \supseteq \cdots\) be a decreasing sequence of sub-σ-algebras of \(\mathcal F\), and let \(\mathcal F_\infty = \bigcap_n \mathcal F_n\). If the real-valued process \((M_n)_{n \ge 0}\) is a backwards martingale with respect to \((\mathcal F_n)\) and \(\mu\), then \(M_n \to \mathbb E[M_0 \mid \mathcal F_\infty]\) as \(n \to \infty\), \(\mu\)-almost everywhere.

theorem backwards_martingale_ae_tendsto {M : ℕ → Ω → ℝ} (m : ℕ → MeasurableSpace Ω)
    (hm : Antitone m) (hm0 : ∀ n, m n ≤ m0) (hM : IsBackwardsMartingale M m μ) :
    ∀ᵐ ω ∂μ, Tendsto (fun n => M n ω) atTop (𝓝 ((μ[M 0 | ⨅ n, m n]) ω))

Uses 2 · Used by 1

Statement usesBackwards martingale

Proof usesLévy's downward theorem, almost sure convergence

Used byBackwards martingale convergence theorem in L¹

TheoremBackwards martingale convergence theorem in L¹#✓fully proved

Let \((\Omega, \mathcal F, \mu)\) be a probability space, let \(\mathcal F_0 \supseteq \mathcal F_1 \supseteq \cdots\) be a decreasing sequence of sub-σ-algebras of \(\mathcal F\), and let \(\mathcal F_\infty = \bigcap_n \mathcal F_n\). If the real-valued process \((M_n)_{n \ge 0}\) is a backwards martingale with respect to \((\mathcal F_n)\) and \(\mu\), then the \(L^1(\mu)\) norm \(\lVert M_n - \mathbb E[M_0 \mid \mathcal F_\infty] \rVert_1\) tends to \(0\) as \(n \to \infty\).

theorem backwards_martingale_tendsto_eLpNorm_one {M : ℕ → Ω → ℝ}
    (m : ℕ → MeasurableSpace Ω) (hm : Antitone m) (hm0 : ∀ n, m n ≤ m0)
    (hM : IsBackwardsMartingale M m μ) :
    Tendsto (fun n => eLpNorm (M n - μ[M 0 | ⨅ n, m n]) 1 μ) atTop (𝓝 0)

Uses 2

Statement usesBackwards martingale

Proof usesBackwards martingale convergence theorem, almost sure convergence

DefinitionTail sigma-algebra of a decreasing filtration#✓fully proved

The tail sigma-algebra of a decreasing filtration, the intersection of its levels.

@[reducible]
def tailAlgebra (ℱ : Filtration ℕᵒᵈ m0) : MeasurableSpace Ω := ⨅ n, ℱ n

Used by 3

Used byTail sigma-algebra of a constant filtration · Tail sigma-algebra lies in the ambient sigma-algebra · Tail sigma-algebra lies in every level of the filtration

TheoremTail sigma-algebra lies in the ambient sigma-algebra#✓fully proved

The tail sigma-algebra lies in the ambient sigma-algebra.

theorem tailAlgebra_le (ℱ : Filtration ℕᵒᵈ m0) : ℱ.tailAlgebra ≤ m0

Uses 1

Statement usesTail sigma-algebra of a decreasing filtration

TheoremTail sigma-algebra lies in every level of the filtration#✓fully proved

The tail sigma-algebra lies in every level of the decreasing filtration.

theorem tailAlgebra_le_seq (ℱ : Filtration ℕᵒᵈ m0) (n : ℕᵒᵈ) :
    ℱ.tailAlgebra ≤ ℱ n

Uses 1

Statement usesTail sigma-algebra of a decreasing filtration

TheoremTail sigma-algebra of a constant filtration#✓fully proved

A constant decreasing filtration has its constant value as tail algebra.

theorem tailAlgebra_const (m : MeasurableSpace Ω) (hm : m ≤ m0) :
    (Filtration.const ℕᵒᵈ m hm).tailAlgebra = m

Uses 1

Statement usesTail sigma-algebra of a decreasing filtration

TheoremConditional expectations along a filtration are strongly adapted#✓fully proved

Conditional-expectation representatives are strongly adapted separately from their canonical backwards-martingale membership. No integrability of g is needed.

theorem stronglyAdapted_condExp (ℱ : Filtration ℕᵒᵈ m0) (g : Ω → ℝ) (μ : Measure Ω) :
    StronglyAdapted ℱ (fun n => μ[g | ℱ n])

TheoremTerms of a backwards martingale are integrable#✓fully proved

Every term is integrable by its canonical conditional-expectation representation.

theorem integrable {M : ℕ → Ω → ℝ} {m : ℕ → MeasurableSpace Ω}
    (hM : IsBackwardsMartingale M m μ) (n : ℕ) : Integrable (M n) μ

Uses 1

Statement usesBackwards martingale

TheoremBackwards martingales are uniformly integrable#✓fully proved

Canonical backwards membership is uniformly integrable in L1 on a finite measure. The ambient bounds suffice; representative adaptedness and antitonicity are unnecessary.

theorem uniformIntegrable [IsFiniteMeasure μ]
    {M : ℕ → Ω → ℝ} {m : ℕ → MeasurableSpace Ω}
    (hM : IsBackwardsMartingale M m μ) (hm0 : ∀ n, m n ≤ m0) :
    UniformIntegrable M 1 μ

Uses 1

Statement usesBackwards martingale

TheoremConditioning a backwards martingale on the next level#✓fully proved

Conditioning a term on the next, smaller level gives the next term a.e.

theorem condExp_succ_ae_eq [IsFiniteMeasure μ]
    {M : ℕ → Ω → ℝ} {m : ℕ → MeasurableSpace Ω}
    (hM : IsBackwardsMartingale M m μ) (hm : Antitone m)
    (hm0 : ∀ n, m n ≤ m0) (n : ℕ) : μ[M n | m (n + 1)] =ᵐ[μ] M (n + 1)

Uses 1

Statement usesBackwards martingale

TheoremConditional expectations form a backwards martingale#✓fully proved

Conditional expectations of arbitrary g form a canonical backwards martingale along decreasing sub-sigma-algebras. The nonintegrable-g convention is retained.

theorem isBackwardsMartingale_condExp [IsFiniteMeasure μ] (g : Ω → ℝ)
    (m : ℕ → MeasurableSpace Ω) (hm : Antitone m) (hm0 : ∀ n, m n ≤ m0) :
    IsBackwardsMartingale (fun n => μ[g | m n]) m μ

Uses 1

Statement usesBackwards martingale

TheoremAlmost-everywhere convergent conditional expectations converge in L¹#✓fully proved

Let \(\mu\) be a finite measure on a measurable space \((\Omega, \mathcal{F})\), let \((\mathcal{G}_n)_{n \in \mathbb{N}}\) be a sequence of sub-σ-algebras of \(\mathcal{F}\), let \(g : \Omega \to \mathbb{R}\) be integrable, and write \(\mu[g \mid \mathcal{G}_n]\) for the conditional expectation of \(g\) given \(\mathcal{G}_n\) with respect to \(\mu\). If \(h : \Omega \to \mathbb{R}\) is integrable and \(\mu[g \mid \mathcal{G}_n] \to h\) \(\mu\)-almost everywhere as \(n \to \infty\), then \(\int_\Omega |\mu[g \mid \mathcal{G}_n] - h| \, d\mu \to 0\) as \(n \to \infty\).

This is Vitali's theorem applied to the uniformly integrable family of conditional expectations of a single integrable function.

theorem tendsto_eLpNorm_condExp_sub_of_ae_tendsto [IsFiniteMeasure μ]
    (g : Ω → ℝ) (m : ℕ → MeasurableSpace Ω)
    (hm_le : ∀ n, m n ≤ m0)
    (hg : Integrable g μ)
    (h : Ω → ℝ)
    (hh_ae : ∀ᵐ ω ∂μ, Tendsto (fun n => (μ[g | m n]) ω) atTop (𝓝 (h ω)))
    (hh_int : Integrable h μ) :
    Tendsto (fun n => eLpNorm ((μ[g | m n]) - h) 1 μ) atTop (𝓝 0)

Used by 1

Used byIdentifying the a.e. limit of conditional expectations

TheoremIdentifying the a.e. limit of conditional expectations#✓fully proved

Let \(\mu\) be a finite measure on a measurable space \((\Omega, \mathcal{F})\), let \((\mathcal{G}_n)_{n \in \mathbb{N}}\) be any sequence of sub-σ-algebras of \(\mathcal{F}\) (not assumed monotone), and let \(g : \Omega \to \mathbb{R}\) be integrable. Write \(\mu[g \mid \mathcal{G}]\) for the conditional expectation of \(g\) given a sub-σ-algebra \(\mathcal{G}\) with respect to \(\mu\), and \(\mathcal{G}_\infty = \bigcap_n \mathcal{G}_n\). Suppose \(h : \Omega \to \mathbb{R}\) is integrable, strongly measurable with respect to \(\mathcal{G}_\infty\), and \(\mu[g \mid \mathcal{G}_n](\omega) \to h(\omega)\) as \(n \to \infty\) for \(\mu\)-almost every \(\omega\). Then \(h = \mu[g \mid \mathcal{G}_\infty]\) \(\mu\)-almost everywhere.

theorem condExp_antitone_limit_eq [IsFiniteMeasure μ]
    (g : Ω → ℝ) (m : ℕ → MeasurableSpace Ω)
    (hm_le : ∀ n, m n ≤ m0)
    (hg : Integrable g μ)
    (h : Ω → ℝ)
    (hh_ae : ∀ᵐ ω ∂μ, Tendsto (fun n => (μ[g | m n]) ω) atTop (𝓝 (h ω)))
    (hh_int : Integrable h μ)
    (hh_meas : StronglyMeasurable[⨅ n, m n] h) :
    h =ᵐ[μ] μ[g | ⨅ n, m n]

Uses 1

Proof usesAlmost-everywhere convergent conditional expectations converge in L¹

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.