Real quasimartingales

Almost-sure regularity along countable time sets

structure ProbabilityTheory.IsRealQuasimartingale {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} (𝓕 : MeasureTheory.Filtration ι mΩ) (X : ι → Ω → ℝ) (μ : MeasureTheory.Measure Ω) : Prop

A real quasimartingale is a real-valued stochastic process that is adapted, integrable, and has bounded variation.

• adapted : MeasureTheory.Adapted 𝓕 X
• integrable (t : ι) : MeasureTheory.Integrable (X t) μ
• boundedVariation (t : ι) : ∃ (C : ℝ), ∀ (S : ElementaryPredictableSet 𝓕), ∫ (x : Ω), SimpleProcess.integral (ContinuousLinearMap.mul ℝ ℝ) (S.indicator 1) X t x ∂μ ≤ C

noncomputable def ProbabilityTheory.variationBound {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} (X : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (μ : MeasureTheory.Measure Ω) (t : ι) : ℝ

The minimal bound on the variation of the process.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.IsRealQuasimartingale.integral_indicator_le_variationBound {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} (hX : IsRealQuasimartingale 𝓕 X μ) (t : ι) (S : ElementaryPredictableSet 𝓕) : ∫ (x : Ω), SimpleProcess.integral (ContinuousLinearMap.mul ℝ ℝ) (S.indicator 1) X t x ∂μ ≤ variationBound X 𝓕 μ t

theorem ProbabilityTheory.IsRealQuasimartingale.stronglyAdapted {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} (hX : IsRealQuasimartingale 𝓕 X μ) : MeasureTheory.StronglyAdapted 𝓕 X

theorem ProbabilityTheory.IsRealQuasimartingale.measurable {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} (hX : IsRealQuasimartingale 𝓕 X μ) (t : ι) : Measurable (X t)

Martingales and submartingales are quasimartingales

theorem MeasureTheory.Martingale.integral_elementaryPredictableSet_indicator_eq_zero {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {X : ι → Ω → ℝ} [SigmaFiniteFiltration μ 𝓕] (hX : Martingale X 𝓕 μ) (S : ProbabilityTheory.ElementaryPredictableSet 𝓕) (t : ι) : ∫ (x : Ω), ProbabilityTheory.SimpleProcess.integral (ContinuousLinearMap.mul ℝ ℝ) (S.indicator 1) X t x ∂μ = 0

The elementary stochastic integral of the indicator of an elementary predictable set against a martingale has zero expectation.

theorem MeasureTheory.Martingale.isRealQuasimartingale {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {X : ι → Ω → ℝ} [SigmaFiniteFiltration μ 𝓕] (hX : Martingale X 𝓕 μ) : ProbabilityTheory.IsRealQuasimartingale 𝓕 X μ

theorem MeasureTheory.Submartingale.setIntegral_sub_setIntegral_le {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {X : ι → Ω → ℝ} [SigmaFiniteFiltration μ 𝓕] (hX : Submartingale X 𝓕 μ) {s t : ι} (hst : s ≤ t) {B : Set Ω} (hB : MeasurableSet B) : ∫ (ω : Ω) in B, X t ω ∂μ - ∫ (ω : Ω) in B, X s ω ∂μ ≤ ∫ (x : Ω), X t x ∂μ - ∫ (x : Ω), X s x ∂μ

For a submartingale X, times s ≤ t and a set B ∈ 𝓕 s, the expectation of the increment X t - X s over B is at most the expectation of the increment.

theorem MeasureTheory.Submartingale.sum_setIntegral_sub_le_aux {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {X : ι → Ω → ℝ} [SigmaFiniteFiltration μ 𝓕] (hX : Submartingale X 𝓕 μ) (A : ι × ι → Set Ω) (I : Finset (ι × ι)) (t : ι) : (∀ p ∈ I, p.1 ≤ p.2) → (∀ p ∈ I, MeasurableSet (A p)) → ((↑I).PairwiseDisjoint fun (p : ι × ι) => Set.Ioc p.1 p.2 ×ˢ A p) → ∑ p ∈ I, (∫ (ω : Ω) in A p, X (min p.2 t) ω ∂μ - ∫ (ω : Ω) in A p, X (min p.1 t) ω ∂μ) ≤ ∫ (x : Ω), X t x ∂μ - ∫ (x : Ω), X ⊥ x ∂μ

Auxiliary lemma for Submartingale.integral_elementaryPredictableSet_indicator_le, stated in terms of the data of an elementary predictable set to allow for an induction on the set of intervals.

theorem MeasureTheory.Submartingale.integral_elementaryPredictableSet_indicator_le {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {X : ι → Ω → ℝ} [SigmaFiniteFiltration μ 𝓕] (hX : Submartingale X 𝓕 μ) (S : ProbabilityTheory.ElementaryPredictableSet 𝓕) (t : ι) : ∫ (x : Ω), ProbabilityTheory.SimpleProcess.integral (ContinuousLinearMap.mul ℝ ℝ) (S.indicator 1) X t x ∂μ ≤ ∫ (x : Ω), X t x ∂μ - ∫ (x : Ω), X ⊥ x ∂μ

The expectation of the elementary stochastic integral of the indicator of an elementary predictable set against a submartingale X is bounded by μ[X t] - μ[X ⊥].

theorem MeasureTheory.Submartingale.isRealQuasimartingale {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {X : ι → Ω → ℝ} [SigmaFiniteFiltration μ 𝓕] (hX : Submartingale X 𝓕 μ) : ProbabilityTheory.IsRealQuasimartingale 𝓕 X μ