Doob-Meyer decomposition theorem

theorem PolishSpace.of_compactSpace_of_secondCountableTopology {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [T2Space X] [SecondCountableTopology X] : PolishSpace X

A compact Hausdorff second-countable space is Polish: it is metrizable by Urysohn's metrization theorem, and a compact metric space is complete.

theorem countable_of_linearOrder_of_locallyFiniteOrderBot (ι : Type u_1) [LinearOrder ι] [LocallyFiniteOrderBot ι] : Countable ι

A linear order in which all the intervals Iio t are finite is countable.

theorem MeasureTheory.debut_mem_set_of_finite {ι : Type u_1} {Ω : Type u_2} [ConditionallyCompleteLinearOrder ι] {E : Set (ι × Ω)} {n : ι} {ω : Ω} (hfin : {t : ι | n ≤ t ∧ (t, ω) ∈ E}.Finite) (h : ∃ t ≥ n, (t, ω) ∈ E) : ((debut E n ω).untopA, ω) ∈ E

If the section {t | n ≤ t ∧ (t, ω) ∈ E} of a set E is finite and nonempty, then the début of E after n at ω belongs to that section.

theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range' {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [Nonempty ι] {m : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {ℱ : Filtration ι m} [SigmaFiniteFiltration μ ℱ] {τ : Ω → WithTop ι} {f : ι → Ω → E} {n : ι} (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ) (hτ_le : ∀ (x : Ω), τ x ≤ ↑n) (h_countable_range : (Set.range τ).Countable) [SigmaFinite (μ.trim ⋯)] : stoppedValue f τ =ᵐ[μ] μ[f n | hτ.measurableSpace]

Optional sampling for a stopping time with countable range bounded by n. This is Martingale.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range without any topological assumption on the index set.

noncomputable def denseSet (ι : Type u_1) [Preorder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [SecondCountableTopology ι] : Set ι

The fixed countable dense set used instead of dyadics, with both endpoints adjoined, as well as the points that are isolated from the right or from the left. Those points are not limits of other points from the corresponding side, hence the values of a process at these times are not controlled by its values on a set which is merely dense. If ι is densely ordered, the only such points are ⊥ and ⊤.

Equations

• denseSet ι = ⋯.choose ∪ {⊥, ⊤} ∪ {t : ι | nhdsWithin t (Set.Ioi t) = ⊥} ∪ {t : ι | nhdsWithin t (Set.Iio t) = ⊥}

theorem denseSet_countable (ι : Type u_1) [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] : (denseSet ι).Countable

theorem denseSet_dense (ι : Type u_1) [Preorder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [SecondCountableTopology ι] : Dense (denseSet ι)

theorem bot_mem_denseSet (ι : Type u_1) [Preorder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [SecondCountableTopology ι] : ⊥ ∈ denseSet ι

theorem top_mem_denseSet (ι : Type u_1) [Preorder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [SecondCountableTopology ι] : ⊤ ∈ denseSet ι

theorem mem_denseSet_of_nhdsGT_eq_bot {ι : Type u_1} [Preorder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [SecondCountableTopology ι] {t : ι} (ht : nhdsWithin t (Set.Ioi t) = ⊥) : t ∈ denseSet ι

The points that are isolated from the right belong to the dense set.

theorem mem_denseSet_of_nhdsLT_eq_bot {ι : Type u_1} [Preorder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [SecondCountableTopology ι] {t : ι} (ht : nhdsWithin t (Set.Iio t) = ⊥) : t ∈ denseSet ι

The points that are isolated from the left belong to the dense set.

theorem exists_mem_denseSet_Ico {ι : Type u_1} [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {a b : ι} (hab : a < b) : ∃ d ∈ denseSet ι, a ≤ d ∧ d < b

Between two times a < b there is a point d of the dense set with a ≤ d < b: a point of the open interval (a, b) if that interval is nonempty, and a itself otherwise since a is then isolated from the right.

noncomputable def denseEnum (ι : Type u_1) [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] : ℕ → ι

A choice of enumeration of the countable dense set used to construct finite meshes.

Equations

• denseEnum ι = Subtype.val ∘ ⋯.choose

theorem exists_denseEnum_eq (ι : Type u_1) [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {d : ι} (hd : d ∈ denseSet ι) : ∃ (k : ℕ), denseEnum ι k = d

Every element of the dense set is attained by the enumeration.

noncomputable def mesh (ι : Type u_1) [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (n : ℕ) : Finset ι

The n-th finite mesh: the first n points of the dense enumeration, plus endpoints.

Equations

• mesh ι n = insert ⊥ (insert ⊤ (Finset.image (denseEnum ι) (Finset.range n)))

theorem denseEnum_mem_mesh (ι : Type u_1) [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {k n : ℕ} (hkn : k < n) : denseEnum ι k ∈ mesh ι n

The k-th point of the dense enumeration belongs to all meshes past k.

theorem bot_mem_mesh (ι : Type u_1) [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (n : ℕ) : ⊥ ∈ mesh ι n

theorem top_mem_mesh (ι : Type u_1) [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (n : ℕ) : ⊤ ∈ mesh ι n

@[instance_reducible]

instance instOrderBotSubtypeMemFinsetMesh (ι : Type u_1) [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (n : ℕ) : OrderBot ↥(mesh ι n)

Equations

• instOrderBotSubtypeMemFinsetMesh ι n = { bot := ⟨⊥, ⋯⟩, bot_le := ⋯ }

@[instance_reducible]

instance instOrderTopSubtypeMemFinsetMesh (ι : Type u_1) [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (n : ℕ) : OrderTop ↥(mesh ι n)

Equations

• instOrderTopSubtypeMemFinsetMesh ι n = { top := ⟨⊤, ⋯⟩, le_top := ⋯ }

@[simp]

theorem top_eq_top (ι : Type u_1) [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (n : ℕ) : ↑⊤ = ⊤

@[simp]

theorem bot_eq_bot (ι : Type u_1) [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (n : ℕ) : ↑⊥ = ⊥

@[instance_reducible]

noncomputable instance instLocallyFiniteOrderSubtypeMemFinsetMesh (ι : Type u_1) [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (n : ℕ) : LocallyFiniteOrder ↥(mesh ι n)

Equations

• instLocallyFiniteOrderSubtypeMemFinsetMesh ι n = Fintype.toLocallyFiniteOrder

@[instance_reducible]

noncomputable instance instSuccOrderSubtypeMemFinsetMesh (ι : Type u_1) [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (n : ℕ) : SuccOrder ↥(mesh ι n)

Equations

• instSuccOrderSubtypeMemFinsetMesh ι n = LinearLocallyFiniteOrder.succOrder ↥(mesh ι n)

@[instance_reducible]

noncomputable instance instPredOrderSubtypeMemFinsetMesh (ι : Type u_1) [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (n : ℕ) : PredOrder ↥(mesh ι n)

Equations

• instPredOrderSubtypeMemFinsetMesh ι n = LinearLocallyFiniteOrder.predOrder ↥(mesh ι n)

@[instance_reducible]

noncomputable instance instCompleteLinearOrderSubtypeMemFinsetMesh (ι : Type u_1) [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (n : ℕ) : CompleteLinearOrder ↥(mesh ι n)

Equations

• instCompleteLinearOrderSubtypeMemFinsetMesh ι n = Fintype.toCompleteLinearOrder ↥(mesh ι n)

def meshFiltration {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (𝓕 : MeasureTheory.Filtration ι mΩ) (n : ℕ) : MeasureTheory.Filtration (↥(mesh ι n)) mΩ

The filtration obtained by restricting 𝓕 to a finite dense mesh.

Equations

• meshFiltration 𝓕 n = 𝓕.indexComap ⋯

instance sigmaFiniteFiltration_meshFiltration {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasureTheory.SigmaFiniteFiltration P 𝓕] (n : ℕ) : MeasureTheory.SigmaFiniteFiltration P (meshFiltration 𝓕 n)

noncomputable def predictablePart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) : ι → Ω → E

Predictable part of a discrete process.

Equations

• predictablePart S 𝓕 P n = ∑ i < n, P[S (Order.succ i) - S i | ↑𝓕 i]

theorem predictablePart_add {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {P : MeasureTheory.Measure Ω} {S₁ S₂ : ι → Ω → E} (𝓕 : MeasureTheory.Filtration ι mΩ) (hS₁ : ∀ (t : ι), MeasureTheory.Integrable (S₁ t) P) (hS₂ : ∀ (t : ι), MeasureTheory.Integrable (S₂ t) P) (t : ι) : predictablePart (S₁ + S₂) 𝓕 P t =ᵐ[P] predictablePart S₁ 𝓕 P t + predictablePart S₂ 𝓕 P t

The predictable part is additive for integrable processes.

theorem predictablePart_eq_zero_of_martingale {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {P : MeasureTheory.Measure Ω} {S : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} (hS : MeasureTheory.Martingale S 𝓕 P) (t : ι) : predictablePart S 𝓕 P t =ᵐ[P] 0

The predictable part of a martingale is zero at every time.

@[simp]

theorem predictablePart_bot {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [LocallyFiniteOrder ι] [OrderBot ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) : predictablePart S 𝓕 P ⊥ = 0

theorem integrable_predictablePart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (S : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) (t : ι) : MeasureTheory.Integrable (predictablePart S 𝓕 P t) P

The predictable part at a fixed point of a discrete mesh is integrable.

theorem MeasureTheory.Submartingale.monotone_predictablePart_ae {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [PartialOrder E] [IsOrderedAddMonoid E] {S : ι → Ω → E} {𝓕 : Filtration ι mΩ} (hs : Submartingale S 𝓕 P) : ∀ᵐ (ω : Ω) ∂P, Monotone fun (x : ι) => _root_.predictablePart S 𝓕 P x ω

The predictable part of a discrete submartingale is monotone a.e.

theorem MeasureTheory.Submartingale.predictablePart_nonneg' {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [LocallyFiniteOrder ι] [OrderBot ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [PartialOrder E] [IsOrderedAddMonoid E] {S : ι → Ω → E} {𝓕 : Filtration ι mΩ} (hs : Submartingale S 𝓕 P) : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ι), 0 ≤ _root_.predictablePart S 𝓕 P n ω

The predictable part of a discrete submartingale is nonnegative a.e.

noncomputable def martingalePart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) : ι → Ω → E

Martingale part of a discrete process.

Equations

• martingalePart S 𝓕 P = S - predictablePart S 𝓕 P

theorem martingalePart_add {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {P : MeasureTheory.Measure Ω} {S₁ S₂ : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} (hS₁ : ∀ (t : ι), MeasureTheory.Integrable (S₁ t) P) (hS₂ : ∀ (t : ι), MeasureTheory.Integrable (S₂ t) P) (t : ι) : martingalePart (S₁ + S₂) 𝓕 P t =ᵐ[P] martingalePart S₁ 𝓕 P t + martingalePart S₂ 𝓕 P t

The martingale part is additive for integrable processes.

theorem martingalePart_eq_self_of_martingale {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {P : MeasureTheory.Measure Ω} {S : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} (hS : MeasureTheory.Martingale S 𝓕 P) (t : ι) : martingalePart S 𝓕 P t =ᵐ[P] S t

The martingale part of a martingale is the martingale itself.

theorem stronglyAdapted_predictablePart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) : MeasureTheory.StronglyAdapted 𝓕 (predictablePart S 𝓕 P)

The predictable part of a process is strongly adapted.

theorem predictablePart_succ_of_not_isMax {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) {j : ι} (hj : ¬IsMax j) : predictablePart S 𝓕 P (Order.succ j) = predictablePart S 𝓕 P j + P[S (Order.succ j) - S j | ↑𝓕 j]

The predictable part at succ j is the predictable part at j plus the conditional expectation of the increment.

theorem martingale_martingalePart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [LocallyFiniteOrder ι] [OrderBot ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} {P : MeasureTheory.Measure Ω} [MeasureTheory.SigmaFiniteFiltration P 𝓕] (hS_adapted : MeasureTheory.StronglyAdapted 𝓕 S) (hS_int : ∀ (t : ι), MeasureTheory.Integrable (S t) P) : MeasureTheory.Martingale (martingalePart S 𝓕 P) 𝓕 P

The martingale part of an adapted integrable process is a martingale.

@[simp]

theorem martingalePart_add_predictablePart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) : martingalePart S 𝓕 P + predictablePart S 𝓕 P = S

noncomputable def predictableSeqTop {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) (n : ℕ) : Ω → E

Sequence of terminal values of the predictable part.

Equations

• predictableSeqTop S 𝓕 P n = predictablePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P ⊤

theorem integrable_predictableSeqTop {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (S : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) (n : ℕ) : MeasureTheory.Integrable (predictableSeqTop S 𝓕 P n) P

The terminal values of the predictable parts on each mesh are integrable.

theorem predictableSeqTop_eq_zero_of_martingale {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {P : MeasureTheory.Measure Ω} {S : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} (hS : MeasureTheory.Martingale S 𝓕 P) (n : ℕ) : predictableSeqTop S 𝓕 P n =ᵐ[P] 0

The terminal values of the predictable parts of a martingale vanish on every mesh.

noncomputable def martingaleSeqTop {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) (n : ℕ) : Ω → E

Sequence of terminal values of the martingale part.

Equations

• martingaleSeqTop S 𝓕 P n = martingalePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P ⊤

theorem martingaleSeqTop_add {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {P : MeasureTheory.Measure Ω} {S₁ S₂ : ι → Ω → E} (𝓕 : MeasureTheory.Filtration ι mΩ) (hS₁ : ∀ (t : ι), MeasureTheory.Integrable (S₁ t) P) (hS₂ : ∀ (t : ι), MeasureTheory.Integrable (S₂ t) P) (n : ℕ) : martingaleSeqTop (S₁ + S₂) 𝓕 P n =ᵐ[P] martingaleSeqTop S₁ 𝓕 P n + martingaleSeqTop S₂ 𝓕 P n

The terminal values of the discrete martingale parts are additive.

theorem martingaleSeqTop_eq_self_of_martingale {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {P : MeasureTheory.Measure Ω} {S : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} (hS : MeasureTheory.Martingale S 𝓕 P) (n : ℕ) : martingaleSeqTop S 𝓕 P n =ᵐ[P] S ⊤

The terminal values of the martingale parts of a martingale are its terminal value on every mesh.

theorem martingaleSeqTop_eq_neg_predictableSeqTop {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] {S : ι → Ω → E} (𝓕 : MeasureTheory.Filtration ι mΩ) (hstop : S ⊤ =ᵐ[P] 0) (n : ℕ) : martingaleSeqTop S 𝓕 P n =ᵐ[P] -predictableSeqTop S 𝓕 P n

If S = 0 a.e., then the martingale part’s terminal value equals the negative of the predictable part’s terminal value.

theorem integrable_martingaleSeqTop {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : ι → Ω → E} (𝓕 : MeasureTheory.Filtration ι mΩ) (hS : MeasureTheory.Integrable (S ⊤) P) (n : ℕ) : MeasureTheory.Integrable (martingaleSeqTop S 𝓕 P n) P

The terminal values of the martingale parts on each mesh are integrable.

theorem martingale_martingalePart_mesh {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasureTheory.SigmaFiniteFiltration P 𝓕] (hS_adapted : MeasureTheory.StronglyAdapted 𝓕 S) (hS_int : ∀ (t : ι), MeasureTheory.Integrable (S t) P) (n : ℕ) : MeasureTheory.Martingale (martingalePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P) (meshFiltration 𝓕 n) P

The discrete martingale part of an adapted integrable process on the n-th mesh is a martingale.

theorem integral_martingaleSeqTop {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : ι → Ω → E} (𝓕 : MeasureTheory.Filtration ι mΩ) [MeasureTheory.SigmaFiniteFiltration P 𝓕] (hS_adapted : MeasureTheory.StronglyAdapted 𝓕 S) (hS_int : ∀ (t : ι), MeasureTheory.Integrable (S t) P) (n : ℕ) : ∫ (ω : Ω), martingaleSeqTop S 𝓕 P n ω ∂P = ∫ (ω : Ω), S ⊥ ω ∂P

On each mesh, the terminal value of the martingale part has the same expectation as the initial value of the process.

theorem equation4 {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} {n : ℕ} [MeasureTheory.SigmaFiniteFiltration P 𝓕] (hS_adapted : MeasureTheory.StronglyAdapted 𝓕 S) (hS_int : ∀ (t : ι), MeasureTheory.Integrable (S t) P) (hstop : S ⊤ =ᵐ[P] 0) {τ : Ω → WithTop ↥(mesh ι n)} (hτ : ∀ (ω : Ω), τ ω ≤ ↑⊤) (hτs : MeasureTheory.IsStoppingTime (meshFiltration 𝓕 n) τ) : MeasureTheory.stoppedValue (S ∘ Subtype.val) τ =ᵐ[P] -P[predictableSeqTop S 𝓕 P n | hτs.measurableSpace] + MeasureTheory.stoppedValue (predictablePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P) τ

Apply the optional stopping theorem to get equation 4.

noncomputable def tauMesh {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) (n : ℕ) (c : ℝ) : Ω → WithTop ↥(mesh ι n)

The mesh stopping time τₙ(c) associated with the predictable part on the n-th mesh.

Equations

• tauMesh S 𝓕 P n c ω = ↑(MeasureTheory.hittingBtwn (fun (t : ↥(mesh ι n)) (ω : Ω) => predictablePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P (Order.succ t) ω) (Set.Ioi c) ⊥ ⊤ ω)

theorem tauMesh_le_top {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) (n : ℕ) (c : ℝ) (ω : Ω) : tauMesh S 𝓕 P n c ω ≤ ↑⊤

theorem stoppedValue_predictablePart_tauMesh_le {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) (n : ℕ) {c : ℝ} (hc : 0 ≤ c) : MeasureTheory.stoppedValue (predictablePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P) (tauMesh S 𝓕 P n c) ≤ fun (x : Ω) => c

The stopped valued of the predictable part with respect to τₙ(c) is less than or equal to c.

theorem stronglyMeasurable_predictable_indicator_Ioi {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [TopologicalSpace E] [Zero E] {𝓕 : MeasureTheory.Filtration ι mΩ} {i : ι} {f : Ω → E} (hf : MeasureTheory.StronglyMeasurable f) : MeasureTheory.StronglyMeasurable ((Set.Ioi i ×ˢ Set.univ).indicator fun (p : ι × Ω) => f p.2)

If f is strongly measurable with respect to 𝓕 i, then the process equal to f on (i, ∞) and to 0 elsewhere is strongly measurable for the predictable σ-algebra.

theorem isPredictable_predictablePart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [LocallyFiniteOrder ι] [OrderBot ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) : MeasureTheory.IsStronglyPredictable 𝓕 (predictablePart S 𝓕 P)

The predictable part is predictable.

theorem stronglyMeasurable_pred_predictablePart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [PredOrder ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) (t : ι) : MeasureTheory.StronglyMeasurable (predictablePart S 𝓕 P t)

At time t, the predictable part is strongly measurable with respect to the previous σ-algebra.

theorem stronglyMeasurable_predictablePart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [PredOrder ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) (t : ι) : MeasureTheory.StronglyMeasurable (predictablePart S 𝓕 P t)

At time t, the predictable part is strongly measurable with respect to the previous σ-algebra.

theorem stronglyAdapted_predictablePart' {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : ι → Ω → E) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) : MeasureTheory.StronglyAdapted 𝓕 fun (t : ι) (ω : Ω) => predictablePart S 𝓕 P (Order.succ t) ω

The predictable part of a process is strongly adapted.

theorem isStoppingTime_tauMesh {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) (n : ℕ) (c : ℝ) : MeasureTheory.IsStoppingTime (meshFiltration 𝓕 n) (tauMesh S 𝓕 P n c)

τₙ(c) is indeed a stopping time.

theorem stoppedValue_le_neg_condExp_predictableSeqTop_add_const {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} (hstop : S ⊤ =ᵐ[P] 0) (𝓕 : MeasureTheory.Filtration ι mΩ) (n : ℕ) [MeasureTheory.SigmaFiniteFiltration P 𝓕] (hS_adapted : MeasureTheory.StronglyAdapted 𝓕 S) (hS_int : ∀ (t : ι), MeasureTheory.Integrable (S t) P) {c : ℝ} (hc : 0 ≤ c) : MeasureTheory.stoppedValue (S ∘ Subtype.val) (tauMesh S 𝓕 P n c) ≤ᵐ[P] -P[predictableSeqTop S 𝓕 P n | ⋯.measurableSpace] + fun (x : Ω) => c

Combine equation 4 and stoppedValue_predictablePart_tauMesh_le to get this inequality.

theorem MeasureTheory.Submartingale.tauMesh_lt_top_eq_lt_predictableSeqTop {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {S : ι → Ω → ℝ} {𝓕 : Filtration ι mΩ} (hs : Submartingale S 𝓕 P) (n : ℕ) {c : ℝ} (hc : 0 ≤ c) : {ω : Ω | tauMesh S 𝓕 P n c ω < ↑⊤} =ᵐ[P] {ω : Ω | c < predictableSeqTop S 𝓕 P n ω}

{τₙ(c) < 1} = {c < Aⁿ₁}.

theorem MeasureTheory.Submartingale.integrableOn_const_tauMesh_lt_top {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {S : ι → Ω → ℝ} {𝓕 : Filtration ι mΩ} (hs : Submartingale S 𝓕 P) (n : ℕ) {c : ℝ} (hc : 0 ≤ c) : IntegrableOn (fun (x : Ω) => c) {ω : Ω | tauMesh S 𝓕 P n c ω < ↑⊤} P

The constant c is integrable on the event where τₙ(c) hits before the top element.

theorem MeasureTheory.Submartingale.integrable_stoppedValue_tauMesh {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {S : ι → Ω → ℝ} {𝓕 : Filtration ι mΩ} (hs : Submartingale S 𝓕 P) (n : ℕ) (c : ℝ) : Integrable (stoppedValue (S ∘ Subtype.val) (tauMesh S 𝓕 P n c)) P

Stopping S at the bounded mesh time τₙ(c) preserves integrability.

theorem first_estimate {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} (hstop : S ⊤ =ᵐ[P] 0) (𝓕 : MeasureTheory.Filtration ι mΩ) (n : ℕ) [MeasureTheory.SigmaFiniteFiltration P 𝓕] {c : ℝ} (hc : 0 ≤ c) (hs : MeasureTheory.Submartingale S 𝓕 P) : ∫ (ω : Ω) in {ω : Ω | c < predictableSeqTop S 𝓕 P n ω}, predictableSeqTop S 𝓕 P n ω ∂P ≤ c * P.real {ω : Ω | tauMesh S 𝓕 P n c ω < ↑⊤} - ∫ (ω : Ω) in {ω : Ω | tauMesh S 𝓕 P n c ω < ↑⊤}, MeasureTheory.stoppedValue (S ∘ Subtype.val) (tauMesh S 𝓕 P n c) ω ∂P

The first estimate before equation 5.

theorem tauMesh_lt_top_subset_of_lt {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) (n : ℕ) {a b : ℝ} (hab : a ≤ b) : {ω : Ω | tauMesh S 𝓕 P n b ω < ↑⊤} ⊆ {ω : Ω | tauMesh S 𝓕 P n a ω < ↑⊤}

If a ≤ b, then {τₙ(b) < 1} ⊆ {τₙ(a) < 1}.

theorem integrable_stoppedValue_predictablePart_tauMesh {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) (n : ℕ) (c : ℝ) : MeasureTheory.Integrable (MeasureTheory.stoppedValue (predictablePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P) (tauMesh S 𝓕 P n c)) P

Stopping the predictable part at the bounded mesh time τₙ(c) preserves integrability.

theorem second_estimate {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} (hstop : S ⊤ =ᵐ[P] 0) (𝓕 : MeasureTheory.Filtration ι mΩ) (n : ℕ) [MeasureTheory.SigmaFiniteFiltration P 𝓕] {c : ℝ} (hc : 0 ≤ c) (hs : MeasureTheory.Submartingale S 𝓕 P) : c / 2 * P.real {ω : Ω | tauMesh S 𝓕 P n c ω < ↑⊤} ≤ -∫ (ω : Ω) in {ω : Ω | tauMesh S 𝓕 P n (c / 2) ω < ↑⊤}, MeasureTheory.stoppedValue (S ∘ Subtype.val) (tauMesh S 𝓕 P n (c / 2)) ω ∂P

The second estimate before equation 5.

theorem equation5 {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} (hstop : S ⊤ =ᵐ[P] 0) (𝓕 : MeasureTheory.Filtration ι mΩ) (n : ℕ) [MeasureTheory.SigmaFiniteFiltration P 𝓕] {c : ℝ} (hc : 0 ≤ c) (hs : MeasureTheory.Submartingale S 𝓕 P) : ∫ (ω : Ω) in {ω : Ω | c < predictableSeqTop S 𝓕 P n ω}, predictableSeqTop S 𝓕 P n ω ∂P ≤ -2 * ∫ (ω : Ω) in {ω : Ω | tauMesh S 𝓕 P n (c / 2) ω < ↑⊤}, MeasureTheory.stoppedValue (S ∘ Subtype.val) (tauMesh S 𝓕 P n (c / 2)) ω ∂P - ∫ (ω : Ω) in {ω : Ω | tauMesh S 𝓕 P n c ω < ↑⊤}, MeasureTheory.stoppedValue (S ∘ Subtype.val) (tauMesh S 𝓕 P n c) ω ∂P

theorem equation5' {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} (hstop : S ⊤ =ᵐ[P] 0) (𝓕 : MeasureTheory.Filtration ι mΩ) (n : ℕ) [MeasureTheory.SigmaFiniteFiltration P 𝓕] {c : ℝ} (hc : 0 ≤ c) (hs : MeasureTheory.Submartingale S 𝓕 P) : ∫ (ω : Ω) in {ω : Ω | c < predictableSeqTop S 𝓕 P n ω}, predictableSeqTop S 𝓕 P n ω ∂P ≤ ∫ (ω : Ω) in {ω : Ω | tauMesh S 𝓕 P n (c / 2) ω < ↑⊤}, -2 * MeasureTheory.stoppedValue (S ∘ Subtype.val) (tauMesh S 𝓕 P n (c / 2)) ω ∂P + ∫ (ω : Ω) in {ω : Ω | tauMesh S 𝓕 P n c ω < ↑⊤}, -MeasureTheory.stoppedValue (S ∘ Subtype.val) (tauMesh S 𝓕 P n c) ω ∂P

noncomputable def tauMeshLift {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) (n : ℕ) (c : ℝ) : Ω → WithTop ι

Lift the mesh stopping time τₙ(c) to a stopping time on the original index set.

Equations

• tauMeshLift S 𝓕 P n c ω = ↑↑(tauMesh S 𝓕 P n c ω).untopA

@[simp]

theorem tauMesh_ne_top {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) (n : ℕ) (c : ℝ) (ω : Ω) : tauMesh S 𝓕 P n c ω ≠ ⊤

@[simp]

theorem tauMeshLift_ne_top {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) (n : ℕ) (c : ℝ) (ω : Ω) : tauMeshLift S 𝓕 P n c ω ≠ ⊤

theorem stoppedValue_tauMeshLift {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) (n : ℕ) (c : ℝ) : MeasureTheory.stoppedValue S (tauMeshLift S 𝓕 P n c) = MeasureTheory.stoppedValue (S ∘ Subtype.val) (tauMesh S 𝓕 P n c)

theorem countable_range_tauMeshLift {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) (n : ℕ) (c : ℝ) : (Set.range (tauMeshLift S 𝓕 P n c)).Countable

The lifted mesh stopping time takes values in the finite mesh, hence has countable range.

theorem isStoppingTime_tauMeshLift {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (P : MeasureTheory.Measure Ω) (n : ℕ) (c : ℝ) : MeasureTheory.IsStoppingTime 𝓕 (tauMeshLift S 𝓕 P n c)

We still get a stopping time after the lifting.

theorem integral_predictableSeqTop_eq_neg_integral_bot {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasureTheory.SigmaFiniteFiltration P 𝓕] (hS_adapted : MeasureTheory.StronglyAdapted 𝓕 S) (hS_int : ∀ (t : ι), MeasureTheory.Integrable (S t) P) (hstop : S ⊤ =ᵐ[P] 0) (n : ℕ) : ∫ (ω : Ω), predictableSeqTop S 𝓕 P n ω ∂P = -∫ (ω : Ω), S ⊥ ω ∂P

Used in estimating the size of the set {τₙ(b) < 1}.

theorem measure_tauMesh_lt_top_le {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasureTheory.SigmaFiniteFiltration P 𝓕] (hs : MeasureTheory.Submartingale S 𝓕 P) (hstop : S ⊤ =ᵐ[P] 0) (n : ℕ) {c : ℝ} (hc : 0 < c) : P {ω : Ω | tauMesh S 𝓕 P n c ω < ↑⊤} ≤ ENNReal.ofReal (-∫ (ω : Ω), S ⊥ ω ∂P) / ENNReal.ofReal c

Estimate for the hitting event {τₙ(c) < 1}.

theorem UniformIntegrable.eLpNorm_tendsto_zero_of_iSup_measure_tendsto_zero {α : Type u_1} {ι : Type u_2} {κ : Type u_3} {Ω : Type u_4} {E : Type u_5} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] {X : α → Ω → E} {p : ENNReal} (hX : MeasureTheory.UniformIntegrable X p μ) {A : κ → ι → Set Ω} (hA_meas : ∀ (k : κ) (i : ι), MeasurableSet (A k i)) {F : κ → ι → α} {l : Filter κ} (hA : Filter.Tendsto (fun (k : κ) => ⨆ (i : ι), μ (A k i)) l (nhds 0)) : Filter.Tendsto (fun (k : κ) => ⨆ (i : ι), MeasureTheory.eLpNorm ((A k i).indicator (X (F k i))) p μ) l (nhds 0)

If X is uniformly integrable in Lᵖ and the sets A k i have supremum-over-i measure tending to 0 along l, then ⨆ i, eLpNorm ((A k i).indicator (X (F k i))) tends to 0. This isolates the ε–δ core of uniform integrability from any particular application: reindexing the family by F is harmless because uniform integrability controls the whole index type at once.

theorem MeasureTheory.Submartingale.ae_le_zero_of_top_ae_eq_zero {ι : Type u_1} {Ω : Type u_2} [Preorder ι] [OrderTop ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {S : ι → Ω → ℝ} {𝓕 : Filtration ι mΩ} (hs : Submartingale S 𝓕 P) (hstop : S ⊤ =ᵐ[P] 0) (t : ι) : S t ≤ᵐ[P] 0

A submartingale whose terminal value vanishes is nonpositive.

theorem uniformIntegrable_predictableSeqTop {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hs : MeasureTheory.Submartingale S 𝓕 P) (hd : MeasureTheory.UniformIntegrable (fun (τ : ↑{T : Ω → WithTop ι | MeasureTheory.IsStoppingTime 𝓕 T ∧ (∀ (ω : Ω), T ω ≠ ⊤) ∧ (Set.range T).Countable}) => MeasureTheory.stoppedValue S ↑τ) 1 P) (hstop : S ⊤ =ᵐ[P] 0) : MeasureTheory.UniformIntegrable (predictableSeqTop S 𝓕 P) 1 P

The terminal values of the predictable parts are uniformly integrable.

theorem uniformIntegrable_stoppedValue_condExp_of_countable_range {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderTop ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {𝓕 : MeasureTheory.Filtration ι mΩ} {ξ : Ω → ℝ} : MeasureTheory.UniformIntegrable (fun (τ : ↑{T : Ω → WithTop ι | MeasureTheory.IsStoppingTime 𝓕 T ∧ (∀ (ω : Ω), T ω ≠ ⊤) ∧ (Set.range T).Countable}) => MeasureTheory.stoppedValue (fun (i : ι) => P[ξ | ↑𝓕 i]) ↑τ) 1 P

The stopped values of a closed martingale t ↦ P[ξ | 𝓕 t] at finite stopping times with countable range are uniformly integrable.

theorem uniformIntegrable_stoppedValue_sub_condExp_of_countable_range {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderTop ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : MeasureTheory.UniformIntegrable (fun (τ : ↑{T : Ω → WithTop ι | MeasureTheory.IsStoppingTime 𝓕 T ∧ (∀ (ω : Ω), T ω ≠ ⊤) ∧ (Set.range T).Countable}) => MeasureTheory.stoppedValue S ↑τ) 1 P) : MeasureTheory.UniformIntegrable (fun (τ : ↑{T : Ω → WithTop ι | MeasureTheory.IsStoppingTime 𝓕 T ∧ (∀ (ω : Ω), T ω ≠ ⊤) ∧ (Set.range T).Countable}) => MeasureTheory.stoppedValue (S - fun (i : ι) => P[S ⊤ | ↑𝓕 i]) ↑τ) 1 P

If the stopped values of S at finite stopping times with countable range are uniformly integrable, then so are those of S - (fun i ↦ P[S ⊤ | 𝓕 i]).

theorem ProbabilityTheory.ClassD.uniformIntegrable_of_countable_range {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderTop ι] [MeasurableSpace ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ClassD S 𝓕 P) : MeasureTheory.UniformIntegrable (fun (τ : ↑{T : Ω → WithTop ι | MeasureTheory.IsStoppingTime 𝓕 T ∧ (∀ (ω : Ω), T ω ≠ ⊤) ∧ (Set.range T).Countable}) => MeasureTheory.stoppedValue S ↑τ) 1 P

For a process of class D, the stopped values at finite stopping times with countable range are uniformly integrable.

theorem uniformIntegrable_martingaleSeqTopAux {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hs : MeasureTheory.Submartingale S 𝓕 P) (hd : MeasureTheory.UniformIntegrable (fun (τ : ↑{T : Ω → WithTop ι | MeasureTheory.IsStoppingTime 𝓕 T ∧ (∀ (ω : Ω), T ω ≠ ⊤) ∧ (Set.range T).Countable}) => MeasureTheory.stoppedValue S ↑τ) 1 P) (hstop : S ⊤ =ᵐ[P] 0) : MeasureTheory.UniformIntegrable (martingaleSeqTop S 𝓕 P) 1 P

As the terminal values of predictable parts are uniformly integrable, the terminal values of the martingale parts are uniformly integrable.

theorem uniformIntegrable_martingaleSeqTop {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : MeasureTheory.UniformIntegrable (fun (τ : ↑{T : Ω → WithTop ι | MeasureTheory.IsStoppingTime 𝓕 T ∧ (∀ (ω : Ω), T ω ≠ ⊤) ∧ (Set.range T).Countable}) => MeasureTheory.stoppedValue S ↑τ) 1 P) (hs : MeasureTheory.Submartingale S 𝓕 P) : MeasureTheory.UniformIntegrable (martingaleSeqTop S 𝓕 P) 1 P

Prove uniform integrability without the assumption S ⊤ =ᵐ[P] 0.

noncomputable def martingaleSeqStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (n : ℕ) (i : ι) : Ω → ℝ

The extension of the discrete martingale part M^n.

Equations

• martingaleSeqStep P S 𝓕 n i = P[martingaleSeqTop S 𝓕 P n | ↑𝓕 i]

noncomputable def meshPredIoc {ι : Type u_1} [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] (n : ℕ) (t : ↥(mesh ι n)) : Set ι

The half-open mesh interval ending at t, with left endpoint the predecessor of t in the finite mesh.

Equations

• meshPredIoc n t = Set.Ioc ↑(Order.pred t) ↑t

noncomputable def predictableSeqStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (n : ℕ) : ι → Ω → ℝ

The mesh step-extension of the discrete predictable part A^n.

Equations

• predictableSeqStep P S 𝓕 n t = ∑ u : ↥(mesh ι n), (meshPredIoc n u).indicator (fun (x : ι) => predictablePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P u) t

theorem stronglyAdapted_predictableSeqStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (n : ℕ) : MeasureTheory.StronglyAdapted 𝓕 (predictableSeqStep P S 𝓕 n)

The mesh step-extension of the discrete predictable part is strongly adapted.

theorem stronglyAdapted_weights_sum_predictableSeqStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (w : ℕ →₀ ℝ) : MeasureTheory.StronglyAdapted 𝓕 (w.sum fun (m : ℕ) (r : ℝ) => r • predictableSeqStep P S 𝓕 m)

Finite linear combinations of the mesh step-extensions of the discrete predictable parts are strongly adapted.

theorem predictableSeqStep_apply_of_mem {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} {n : ℕ} {t : ι} {u : ↥(mesh ι n)} (ht : t ∈ meshPredIoc n u) : predictableSeqStep P S 𝓕 n t = predictablePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P u

On the half-open mesh interval (pred u, u], the step extension of the discrete predictable part takes the value of the discrete predictable part at u.

theorem predictableSeqStep_ae_eq_sub_martingaleSeqStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasureTheory.SigmaFiniteFiltration P 𝓕] (hS_adapted : MeasureTheory.StronglyAdapted 𝓕 S) (hS_int : ∀ (t : ι), MeasureTheory.Integrable (S t) P) {n : ℕ} {t : ι} (ht : t ∈ mesh ι n) : predictableSeqStep P S 𝓕 n t =ᵐ[P] S t - martingaleSeqStep P S 𝓕 n t

At a point of the n-th mesh, the step extension of the discrete predictable part is a.e. equal to the process minus the conditional expectation of the terminal value of the discrete martingale part.

theorem exists_strictMono_forall_ae_tendsto_of_tendstoInMeasure {κ : Type u_1} {Ω : Type u_2} {E : Type u_3} [Countable κ] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [PseudoEMetricSpace E] {f : κ → ℕ → Ω → E} {g : κ → Ω → E} (h : ∀ (k : κ), MeasureTheory.TendstoInMeasure μ (f k) Filter.atTop (g k)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ᵐ (ω : Ω) ∂μ, ∀ (k : κ), Filter.Tendsto (fun (n : ℕ) => f k (φ n) ω) Filter.atTop (nhds (g k ω))

Countably many sequences converging in measure admit a common subsequence along which all of them converge almost everywhere.

theorem tendsto_eLpNorm_weights_sum_martingaleSeqStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} {a : ℕ → Convexity.StdSimplex ℝ ℕ} {M : Ω → ℝ} (hs : MeasureTheory.Submartingale S 𝓕 P) (hM : MeasureTheory.Integrable M P) (ha : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (((a n).sum fun (m : ℕ) (r : ℝ) => r • martingaleSeqTop S 𝓕 P m) - M) 1 P) Filter.atTop (nhds 0)) (t : ι) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm ((a n).sum (fun (m : ℕ) (r : ℝ) => r • martingaleSeqStep P S 𝓕 m) t - P[M | ↑𝓕 t]) 1 P) Filter.atTop (nhds 0)

If convex combinations of the terminal values M^m_⊤ of the discrete martingale parts converge in L¹ to M, then at each time t the same convex combinations of the processes martingaleSeqStep converge in L¹ to P[M | 𝓕 t]. Proved by using conditional Jensen.

theorem weights_sum_predictableSeqStep_ae_eq {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} {a : ℕ → Convexity.StdSimplex ℝ ℕ} [MeasureTheory.IsFiniteMeasure P] (hs : MeasureTheory.Submartingale S 𝓕 P) (ha0 : ∀ (n m : ℕ), m < n → (a n).weights m = 0) {t : ι} {k n : ℕ} (hk : denseEnum ι k = t) (hkn : k < n) : (a n).sum (fun (m : ℕ) (r : ℝ) => r • predictableSeqStep P S 𝓕 m) t =ᵐ[P] S t - (a n).sum (fun (m : ℕ) (r : ℝ) => r • martingaleSeqStep P S 𝓕 m) t

If the weights at step n vanish on meshes of index below n, then past the index at which t enters the meshes, the convex combination of the processes predictableSeqStep at t is a.e. equal to the process minus the same convex combination of the processes martingaleSeqStep.

theorem tendsto_eLpNorm_weights_sum_predictableSeqStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} {a : ℕ → Convexity.StdSimplex ℝ ℕ} {M : Ω → ℝ} [MeasureTheory.IsFiniteMeasure P] (hs : MeasureTheory.Submartingale S 𝓕 P) (hM : MeasureTheory.Integrable M P) (ha0 : ∀ (n m : ℕ), m < n → (a n).weights m = 0) (ha : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (((a n).sum fun (m : ℕ) (r : ℝ) => r • martingaleSeqTop S 𝓕 P m) - M) 1 P) Filter.atTop (nhds 0)) {t : ι} (ht : t ∈ denseSet ι) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm ((a n).sum (fun (m : ℕ) (r : ℝ) => r • predictableSeqStep P S 𝓕 m) t - (S t - P[M | ↑𝓕 t])) 1 P) Filter.atTop (nhds 0)

If convex combinations of the terminal values M^m_⊤ of the discrete martingale parts converge in L¹ to M, with weights at step n vanishing on meshes of index below n, then for t in denseSet ι the same convex combinations of the processes predictableSeqStep at t converge in L¹ to S t - P[M | 𝓕 t].

theorem exists_strictMono_ae_tendsto_weights_sum_predictableSeqStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} {a : ℕ → Convexity.StdSimplex ℝ ℕ} {M : Ω → ℝ} [MeasureTheory.IsFiniteMeasure P] (hs : MeasureTheory.Submartingale S 𝓕 P) (hM : MeasureTheory.Integrable M P) (ha0 : ∀ (n m : ℕ), m < n → (a n).weights m = 0) (ha : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (((a n).sum fun (m : ℕ) (r : ℝ) => r • martingaleSeqTop S 𝓕 P m) - M) 1 P) Filter.atTop (nhds 0)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ᵐ (ω : Ω) ∂P, ∀ t ∈ denseSet ι, Filter.Tendsto (fun (n : ℕ) => (a (φ n)).sum (fun (m : ℕ) (r : ℝ) => r • predictableSeqStep P S 𝓕 m) t ω) Filter.atTop (nhds (S t ω - P[M | ↑𝓕 t] ω))

If convex combinations of the terminal values M^m_⊤ of the discrete martingale parts converge in L¹ to M, with weights at step n vanishing on meshes of index below n, then there is a subsequence along which, almost surely, the same convex combinations of the processes predictableSeqStep converge to S t - P[M | 𝓕 t] at every point t of the countable dense set.

theorem exists_martingalPart_lim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) : ∃ (M : Ω → ℝ) (a : ℕ → Convexity.StdSimplex ℝ ℕ), MeasureTheory.Integrable M P ∧ (∀ (n m : ℕ), m < n → (a n).weights m = 0) ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (((a n).sum fun (m : ℕ) (r : ℝ) => r • martingaleSeqTop S 𝓕 P m) - M) 1 P) Filter.atTop (nhds 0) ∧ ∀ᵐ (ω : Ω) ∂P, ∀ t ∈ denseSet ι, Filter.Tendsto (fun (n : ℕ) => (a n).sum (fun (m : ℕ) (r : ℝ) => r • predictableSeqStep P S 𝓕 m) t ω) Filter.atTop (nhds (S t ω - P[M | ↑𝓕 t] ω))

Show that the terminals values of some convex combinations of the martingale parts converge. The convex combination at step n only involves meshes of index at least n, as provided by komlos_L1. The weights are moreover chosen along a subsequence for which the corresponding convex combinations of the step extensions of the discrete predictable parts converge almost surely, simultaneously at all points of the countable dense set.

noncomputable def martingaleLim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) : Ω → ℝ

The L¹ limit of the convex combinations of the terminal values of the discrete martingale parts, given by exists_martingalPart_lim.

Equations

• martingaleLim hd hs = ⋯.choose

noncomputable def martingalePartLim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) : ι → Ω → ℝ

The martingale part M in the Doob-Meyer decomposition of a submartingale of class D: the càdlàg modification of the martingale t ↦ P[martingaleLim hd hs | 𝓕 t].

All its paths are càdlàg (isCadlag_martingalePartLim) and it is a modification of t ↦ P[martingaleLim hd hs | 𝓕 t] (martingalePartLim_ae_eq). Under the usual conditions on the filtration it is adapted, hence a martingale (martingale_martingalePartLim).

Equations

• martingalePartLim hd hs = ProbabilityTheory.cadlagModifReal fun (i : ι) => P[martingaleLim hd hs | ↑𝓕 i]

noncomputable def weight {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) : ℕ → Convexity.StdSimplex ℝ ℕ

This is the weight associated with the martingale part.

Equations

• weight hd hs = ⋯.choose

theorem integrable_martingaleLim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) : MeasureTheory.Integrable (martingaleLim hd hs) P

The limit of the convex combinations of the terminal martingale parts is integrable.

theorem weight_apply_eq_zero_of_lt {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) {m n : ℕ} (hmn : m < n) : (weight hd hs n).weights m = 0

The Komlós weights at step n vanish on meshes of index below n.

theorem tendsto_eLpNorm_weight_sum_martingaleSeqTop {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (((weight hd hs n).sum fun (m : ℕ) (r : ℝ) => r • martingaleSeqTop S 𝓕 P m) - martingaleLim hd hs) 1 P) Filter.atTop (nhds 0)

L¹ convergence of the convex combinations of the terminal martingale parts to martingaleLim.

theorem ae_tendsto_weight_sum_predictableSeqStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) : ∀ᵐ (ω : Ω) ∂P, ∀ t ∈ denseSet ι, Filter.Tendsto (fun (n : ℕ) => (weight hd hs n).sum (fun (m : ℕ) (r : ℝ) => r • predictableSeqStep P S 𝓕 m) t ω) Filter.atTop (nhds (S t ω - P[martingaleLim hd hs | ↑𝓕 t] ω))

Almost surely, the convex combinations of the step extensions of the discrete predictable parts converge to S t - P[martingaleLim hd hs | 𝓕 t] at every point t of the countable dense set.

theorem martingalePartLim_ae_eq {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (t : ι) : martingalePartLim hd hs t =ᵐ[P] P[martingaleLim hd hs | ↑𝓕 t]

The martingale part of the decomposition is a modification of the martingale t ↦ P[martingaleLim hd hs | 𝓕 t].

theorem isCadlag_martingalePartLim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (ω : Ω) : IsCadlag fun (x : ι) => martingalePartLim hd hs x ω

The paths of the martingale part of the decomposition are càdlàg.

theorem integrable_martingalePartLim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (t : ι) : MeasureTheory.Integrable (martingalePartLim hd hs t) P

The martingale part of the decomposition is integrable at each time.

theorem stronglyAdapted_martingalePartLim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] [𝓕.IsComplete P] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) : MeasureTheory.StronglyAdapted 𝓕 (martingalePartLim hd hs)

Under the usual conditions, the martingale part of the decomposition is strongly adapted.

theorem martingale_martingalePartLim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] [𝓕.IsComplete P] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) : MeasureTheory.Martingale (martingalePartLim hd hs) 𝓕 P

Under the usual conditions, the martingale part of the decomposition is a martingale.

theorem integral_martingalePartLim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (i : ι) : ∫ (ω : Ω), martingalePartLim hd hs i ω ∂P = ∫ (ω : Ω), S ⊥ ω ∂P

At each time, the martingale part of the decomposition has the same expectation as the initial value of the process.

noncomputable def martingaleConvexStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (n : ℕ) : ι → Ω → ℝ

The convexly averaged mesh step-extension ℳ^n of the martingale parts.

Equations

• martingaleConvexStep hd hs n = (weight hd hs n).sum fun (m : ℕ) (r : ℝ) => r • martingaleSeqStep P S 𝓕 m

theorem martingaleConvexStep_eLpNorm_tendsto {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (t : ι) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (martingaleConvexStep hd hs n t - martingalePartLim hd hs t) 1 P) Filter.atTop (nhds 0)

L¹ norm convergence of martingaleConvexStep, proved by using conditional Jensen.

noncomputable def predictableConvexStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (n : ℕ) : ι → Ω → ℝ

The convexly averaged mesh step-extension 𝒜^n of the predictable parts.

Equations

• predictableConvexStep hd hs n = (weight hd hs n).sum fun (m : ℕ) (r : ℝ) => r • predictableSeqStep P S 𝓕 m

noncomputable def predictablePartLim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) : ι → Ω → ℝ

The predictable part A in the Doob-Meyer decomposition, defined as S - M where the martingale part M = martingalePartLim hd hs is the càdlàg modification of the martingale t ↦ P[martingaleLim hd hs | 𝓕 t]. In particular A is càdlàg as soon as S is (isCadlag_predictablePartLim_ae).

Equations

• predictablePartLim hd hs = S - martingalePartLim hd hs

theorem integrable_predictablePartLim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (t : ι) : MeasureTheory.Integrable (predictablePartLim hd hs t) P

The predictable part of the decomposition is integrable at each time.

theorem isCadlag_predictablePartLim_ae {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (hc : ∀ᵐ (ω : Ω) ∂P, IsCadlag fun (x : ι) => S x ω) : ∀ᵐ (ω : Ω) ∂P, IsCadlag fun (x : ι) => predictablePartLim hd hs x ω

If the paths of S are almost surely càdlàg, then so are the paths of the predictable part of the decomposition.

theorem isRightContinuous_predictablePartLim_ae {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (hc : ∀ᵐ (ω : Ω) ∂P, IsCadlag fun (x : ι) => S x ω) : ∀ᵐ (ω : Ω) ∂P, IsRightContinuous fun (x : ι) => predictablePartLim hd hs x ω

If the paths of S are almost surely càdlàg, then the paths of the predictable part of the decomposition are almost surely right-continuous.

theorem stronglyAdapted_predictableConvexStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (n : ℕ) : MeasureTheory.StronglyAdapted 𝓕 (predictableConvexStep hd hs n)

The convexly averaged mesh step-extension of the predictable parts is strongly adapted.

noncomputable def meshCeil {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] (n : ℕ) (τ : Ω → WithTop ι) : Ω → WithTop ι

The discretization σₙ of a stopping time τ from the right along the n-th mesh: the smallest mesh point greater than or equal to τ, or ⊤ if τ = ⊤.

Equations

• meshCeil n τ ω = {u ∈ mesh ι n | τ ω ≤ ↑u}.min

theorem le_meshCeil {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {τ : Ω → WithTop ι} (n : ℕ) (ω : Ω) : τ ω ≤ meshCeil n τ ω

theorem meshCeil_le {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {τ : Ω → WithTop ι} {n : ℕ} {ω : Ω} {u : ι} (hu : u ∈ mesh ι n) (hτu : τ ω ≤ ↑u) : meshCeil n τ ω ≤ ↑u

theorem meshCeil_ne_top {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {τ : Ω → WithTop ι} (n : ℕ) {ω : Ω} (hτ : τ ω ≠ ⊤) : meshCeil n τ ω ≠ ⊤

theorem mesh_mem_of_meshCeil_eq_coe {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {τ : Ω → WithTop ι} {n : ℕ} {ω : Ω} {u : ι} (h : meshCeil n τ ω = ↑u) : u ∈ mesh ι n ∧ τ ω ≤ ↑u

theorem exists_meshCeil_eq_coe {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {τ : Ω → WithTop ι} (n : ℕ) {ω : Ω} (hτ : τ ω ≠ ⊤) : ∃ u ∈ mesh ι n, meshCeil n τ ω = ↑u ∧ τ ω ≤ ↑u

theorem meshCeil_eq_bot {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {τ : Ω → WithTop ι} {n : ℕ} {ω : Ω} (h : τ ω = ↑⊥) : meshCeil n τ ω = ↑⊥

theorem countable_range_meshCeil {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] (n : ℕ) (τ : Ω → WithTop ι) : (Set.range (meshCeil n τ)).Countable

theorem isStoppingTime_meshCeil {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) (n : ℕ) : MeasureTheory.IsStoppingTime 𝓕 (meshCeil n τ)

The mesh discretization of a stopping time is a stopping time.

theorem tendsto_untopA_meshCeil {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {τ : Ω → WithTop ι} {ω : Ω} (hτ : τ ω ≠ ⊤) : Filter.Tendsto (fun (n : ℕ) => (meshCeil n τ ω).untopA) Filter.atTop (nhdsWithin (τ ω).untopA (Set.Ici (τ ω).untopA))

The mesh discretizations of τ converge to τ from the right.

theorem stoppedValue_predictableSeqStep_meshCeil {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} {τ : Ω → WithTop ι} {n : ℕ} (hτ_ne : ∀ (ω : Ω), τ ω ≠ ⊤) : MeasureTheory.stoppedValue (predictableSeqStep P S 𝓕 n) τ = MeasureTheory.stoppedValue (predictableSeqStep P S 𝓕 n) (meshCeil n τ)

Sampling the step extension of the discrete predictable part at τ is the same as sampling it at the mesh discretization σₙ of τ.

theorem stoppedValue_predictableSeqStep_ae_eq {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} {τ : Ω → WithTop ι} [MeasureTheory.SigmaFiniteFiltration P 𝓕] {n : ℕ} (hS_adapted : MeasureTheory.StronglyAdapted 𝓕 S) (hS_int : ∀ (t : ι), MeasureTheory.Integrable (S t) P) (hτ_ne : ∀ (ω : Ω), τ ω ≠ ⊤) : MeasureTheory.stoppedValue (predictableSeqStep P S 𝓕 n) (meshCeil n τ) =ᵐ[P] MeasureTheory.stoppedValue S (meshCeil n τ) - MeasureTheory.stoppedValue (martingaleSeqStep P S 𝓕 n) (meshCeil n τ)

Sampled at the mesh discretization σₙ, the step extension of the discrete predictable part decomposes as the sampled process minus the sampled conditional expectations of the terminal value of the discrete martingale part.

theorem integral_stoppedValue_predictableSeqStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} {τ : Ω → WithTop ι} [MeasurableSpace ι] [MeasureTheory.IsFiniteMeasure P] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hS_adapted : MeasureTheory.StronglyAdapted 𝓕 S) (hS_int : ∀ (t : ι), MeasureTheory.Integrable (S t) P) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) (hτ_ne : ∀ (ω : Ω), τ ω ≠ ⊤) (n : ℕ) : ∫ (ω : Ω), MeasureTheory.stoppedValue (predictableSeqStep P S 𝓕 n) τ ω ∂P = ∫ (ω : Ω), MeasureTheory.stoppedValue S (meshCeil n τ) ω ∂P - ∫ (ω : Ω), S ⊥ ω ∂P

The expectation of the stopped step extension of the discrete predictable part.

theorem tendsto_integral_stoppedValue_meshCeil {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} {τ : Ω → WithTop ι} [MeasurableSpace ι] [MeasureTheory.IsFiniteMeasure P] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) (hτ_ne : ∀ (ω : Ω), τ ω ≠ ⊤) (hc : ∀ᵐ (ω : Ω) ∂P, IsCadlag fun (x : ι) => S x ω) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), MeasureTheory.stoppedValue S (meshCeil n τ) ω ∂P) Filter.atTop (nhds (∫ (ω : Ω), MeasureTheory.stoppedValue S τ ω ∂P))

Expectations of the process sampled at the mesh discretizations of τ converge to the expectation of the process sampled at τ.

theorem mesh_mono (ι : Type u_3) [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] : Monotone (mesh ι)

The meshes are increasing.

theorem meshCeil_anti {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] (τ : Ω → WithTop ι) : Antitone fun (n : ℕ) => meshCeil n τ

The mesh discretizations of a random time are decreasing in the mesh index.

theorem tendsto_meshCeil {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] (τ : Ω → WithTop ι) (ω : Ω) : Filter.Tendsto (fun (n : ℕ) => meshCeil n τ ω) Filter.atTop (nhds (τ ω))

The mesh discretizations of a random time converge to it in WithTop ι.

noncomputable def MeasureTheory.IsStoppingTime.meshCeilApproxSequence {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {τ : Ω → WithTop ι} (hτ : IsStoppingTime 𝓕 τ) (μ : Measure Ω) : DiscreteApproxSequence 𝓕 τ μ

The mesh discretizations of a stopping time form a discrete approximation sequence.

Equations

• hτ.meshCeilApproxSequence μ = { seq := fun (n : ℕ) => meshCeil n τ, isStoppingTime := ⋯, countable := ⋯, antitone := ⋯, le := ⋯, tendsto := ⋯ }

@[instance_reducible]

noncomputable instance approximable_of_mesh {ι : Type u_3} {Ω : Type u_4} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} : MeasureTheory.Approximable 𝓕 μ

A second-countable time index with a bottom and a top element is approximable: every stopping time is the limit of its mesh discretizations.

Equations

• approximable_of_mesh = { approxSeq := fun (x : Ω → WithTop ι) (hτ : MeasureTheory.IsStoppingTime 𝓕 x) => hτ.meshCeilApproxSequence μ }

theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_top {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsFiniteMeasure P] {𝓕 : Filtration ι mΩ} {X : ι → Ω → ℝ} {τ : Ω → WithTop ι} (hX : Martingale X 𝓕 P) (hRC : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) (hτ : IsStoppingTime 𝓕 τ) (hτ_ne : ∀ (ω : Ω), τ ω ≠ ⊤) : stoppedValue X τ =ᵐ[P] P[X ⊤ | hτ.measurableSpace]

Optional sampling at a finite stopping time for a right-continuous martingale indexed by a bounded time set.

theorem MeasureTheory.Martingale.integrable_stoppedValue_top {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} [IsFiniteMeasure P] {𝓕 : Filtration ι mΩ} {X : ι → Ω → ℝ} {τ : Ω → WithTop ι} (hX : Martingale X 𝓕 P) (hRC : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) (hτ : IsStoppingTime 𝓕 τ) (hτ_ne : ∀ (ω : Ω), τ ω ≠ ⊤) : Integrable (stoppedValue X τ) P

The value of a right-continuous martingale indexed by a bounded time set at a finite stopping time is integrable.

theorem predictableConvexStep_ae_eq_sub_martingaleConvexStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) {t : ι} {k n : ℕ} (hk : denseEnum ι k = t) (hkn : k < n) : predictableConvexStep hd hs n t =ᵐ[P] S t - martingaleConvexStep hd hs n t

Past the index at which t enters the meshes, predictableConvexStep at t is a.e. equal to the process minus martingaleConvexStep.

theorem predictableConvexStep_eLpNorm_tendsto {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) {t : ι} (ht : t ∈ denseSet ι) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (predictableConvexStep hd hs n t - predictablePartLim hd hs t) 1 P) Filter.atTop (nhds 0)

L¹ norm convergence of predictableConvexStep for t in denseSet ι.

theorem predictableConvexStep_ae_tendsto {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) : ∀ᵐ (ω : Ω) ∂P, ∀ t ∈ denseSet ι, Filter.Tendsto (fun (n : ℕ) => predictableConvexStep hd hs n t ω) Filter.atTop (nhds (predictablePartLim hd hs t ω))

Almost sure convergence of predictableConvexStep to predictablePartLim, simultaneously at all points of the countable dense set. This holds for the whole sequence since the weights were chosen along a suitable subsequence in exists_martingalPart_lim.

theorem monotone_of_eventually_monotone_of_tendsto {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [TopologicalSpace β] [Preorder β] [OrderClosedTopology β] {l : Filter ι} [l.NeBot] {F : ι → α → β} {f : α → β} (hF : ∀ᶠ (i : ι) in l, Monotone (F i)) (hlim : ∀ (x : α), Filter.Tendsto (fun (i : ι) => F i x) l (nhds (f x))) : Monotone f

The limit of a collection of functions that is eventually monotone is monotone.

theorem antitone_of_eventually_antitone_of_tendsto {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [TopologicalSpace β] [Preorder β] [OrderClosedTopology β] {l : Filter ι} [l.NeBot] {F : ι → α → β} {f : α → β} (hF : ∀ᶠ (i : ι) in l, Antitone (F i)) (hlim : ∀ (x : α), Filter.Tendsto (fun (i : ι) => F i x) l (nhds (f x))) : Antitone f

The limit of a collection of functions that is eventually antitone is antitone.

theorem monotone_of_monotone_of_tendsto {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [TopologicalSpace β] [Preorder β] [OrderClosedTopology β] {l : Filter ι} [l.NeBot] {F : ι → α → β} {f : α → β} (hF : ∀ (i : ι), Monotone (F i)) (hlim : ∀ (x : α), Filter.Tendsto (fun (i : ι) => F i x) l (nhds (f x))) : Monotone f

The limit of a collection of monotone functions is monotone.

theorem antitone_of_antitone_of_tendsto {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [TopologicalSpace β] [Preorder β] [OrderClosedTopology β] {l : Filter ι} [l.NeBot] {F : ι → α → β} {f : α → β} (hF : ∀ (i : ι), Antitone (F i)) (hlim : ∀ (x : α), Filter.Tendsto (fun (i : ι) => F i x) l (nhds (f x))) : Antitone f

The limit of a collection of antitone functions is antitone.

theorem Dense.comap_val_nhdsWithin_Ioi_neBot {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {D : Set α} (hD : Dense D) {a : α} (ha : (nhdsWithin a (Set.Ioi a)).NeBot) : (Filter.comap Subtype.val (nhdsWithin a (Set.Ioi a))).NeBot

If D is a dense set and a is not isolated from the right, then the comap of 𝓝[>] a under the inclusion D → α is nontrivial.

theorem Dense.comap_val_nhdsWithin_Iio_neBot {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {D : Set α} (hD : Dense D) {a : α} (ha : (nhdsWithin a (Set.Iio a)).NeBot) : (Filter.comap Subtype.val (nhdsWithin a (Set.Iio a))).NeBot

This is the dual of Dense.comap_val_nhdsWithin_Ioi_neBot.

theorem Dense.monotone_of_isRightContinuous {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [TopologicalSpace β] [Preorder β] [OrderClosedTopology β] {f : α → β} {D : Set α} (hD : Dense D) (hiso : ∀ (t : α), nhdsWithin t (Set.Ioi t) = ⊥ → t ∈ D) (hm : Monotone (f ∘ Subtype.val)) (hf : IsRightContinuous f) : Monotone f

If f is right continuous and is monotone on a dense set D which contains the points that are isolated from the right, then f is monotone. The assumption on D is necessary since right-continuity gives no information at the points that are isolated from the right, for example at a top element.

theorem Filter.IsCoboundedUnder.trans {ι : Type u_1} {α : Type u_2} {r : α → α → Prop} {l : Filter ι} [IsTrans α r] {u v : ι → α} (hle : ∀ᶠ (i : ι) in l, r (u i) (v i)) (h : IsCoboundedUnder r l u) : IsCoboundedUnder r l v

A helper lemma.

theorem limsup_le_of_eventually_monotone_of_tendsto_on_dense {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrder α] [OrderBot α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {l : Filter ι} [l.NeBot] {D : Set α} {F : ι → α → β} {f : α → β} (hF : ∀ᶠ (i : ι) in l, Monotone (F i)) (hD : Dense D) (hiso : ∀ (t : α), nhdsWithin t (Set.Ioi t) = ⊥ → t ∈ D) (hbot : ⊥ ∈ D) {a : α} (hfa : ContinuousWithinAt f (Set.Ioi a) a) (hlim : ∀ t ∈ D, Filter.Tendsto (fun (x : ι) => F x t) l (nhds (f t))) : Filter.limsup (fun (x : ι) => F x a) l ≤ f a

Convergence on a dense set of a collection of monotone function controls the limsup at a point if f is right continuous at a. The dense set has to contain the points that are isolated from the right, at which right-continuity gives no information. We prove this under the assumption that α has a bottom element which belongs to the dense set, because otherwise limsup may have a junk value which breaks the inequality.

theorem le_liminf_of_eventually_monotone_of_tendsto_on_dense {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrder α] [OrderTop α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {l : Filter ι} [l.NeBot] {D : Set α} {F : ι → α → β} {f : α → β} (hF : ∀ᶠ (i : ι) in l, Monotone (F i)) (hD : Dense D) (hiso : ∀ (t : α), nhdsWithin t (Set.Iio t) = ⊥ → t ∈ D) (htop : ⊤ ∈ D) {a : α} (hfa : ContinuousWithinAt f (Set.Iio a) a) (hlim : ∀ t ∈ D, Filter.Tendsto (fun (x : ι) => F x t) l (nhds (f t))) : f a ≤ Filter.liminf (fun (x : ι) => F x a) l

This is the dual of limsup_le_of_eventually_monotone_of_tendsto_on_dense.

theorem tendsto_of_eventually_monotone_of_tendsto_on_dense {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrder α] [BoundedOrder α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {l : Filter ι} [l.NeBot] {D : Set α} {F : ι → α → β} {f : α → β} (hF : ∀ᶠ (i : ι) in l, Monotone (F i)) (hD : Dense D) (hiso_right : ∀ (t : α), nhdsWithin t (Set.Ioi t) = ⊥ → t ∈ D) (hiso_left : ∀ (t : α), nhdsWithin t (Set.Iio t) = ⊥ → t ∈ D) (htop : ⊤ ∈ D) (hbot : ⊥ ∈ D) (a : α) (hfa : ContinuousAt f a) (hlim : ∀ t ∈ D, Filter.Tendsto (fun (x : ι) => F x t) l (nhds (f t))) : Filter.Tendsto (fun (x : ι) => F x a) l (nhds (f a))

We combine limsup_le_of_eventually_monotone_of_tendsto_on_dense and le_liminf_of_eventually_monotone_of_tendsto_on_dense to prove that F · a converges to f a if f is continuous at a.

theorem leftLim_le_liminf_of_eventually_monotone_of_tendsto_on_dense {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrder α] [OrderTop α] [TopologicalSpace α] [OrderTopology α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {l : Filter ι} [l.NeBot] {D : Set α} {F : ι → α → β} {f : α → β} (hF : ∀ᶠ (i : ι) in l, Monotone (F i)) (hD : Dense D) (hiso : ∀ (t : α), nhdsWithin t (Set.Iio t) = ⊥ → t ∈ D) (htop : ⊤ ∈ D) {a : α} (hfa : ∃ (c : β), Filter.Tendsto f (nhdsWithin a (Set.Iio a)) (nhds c)) (hlim : ∀ t ∈ D, Filter.Tendsto (fun (x : ι) => F x t) l (nhds (f t))) : Function.leftLim f a ≤ Filter.liminf (fun (x : ι) => F x a) l

A variant of le_liminf_of_eventually_monotone_of_tendsto_on_dense in which f is only assumed to have a left limit at a: that left limit is at most the liminf of F · a. At a point a which is isolated from the left, f.leftLim a = f a and the inequality follows from the convergence at a, which belongs to D.

theorem predictableSeqStep_eq_sum_indicator {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (n : ℕ) (ω : Ω) (t : ι) : predictableSeqStep P S 𝓕 n t ω = ∑ v : ↥(mesh ι n), (meshPredIoc n v).indicator (fun (x : ι) => predictablePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P v ω) t

theorem predictableSeqStep_apply {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (n : ℕ) (ω : Ω) {t : ι} {u : ↥(mesh ι n)} (ht : t ∈ meshPredIoc n u) : predictableSeqStep P S 𝓕 n t ω = predictablePart (S ∘ Subtype.val) (meshFiltration 𝓕 n) P u ω

On the mesh cell Ioc (pred u) u containing t, the step process predictableSeqStep is constant, equal to the discrete predictable part at the cell's right endpoint u.

theorem predictableSeqStep_monotone_ae {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hs : MeasureTheory.Submartingale S 𝓕 P) (n : ℕ) : ∀ᵐ (ω : Ω) ∂P, Monotone fun (t : ι) => predictableSeqStep P S 𝓕 n t ω

theorem predictableConvexStep_monotone_ae {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (n : ℕ) : ∀ᵐ (ω : Ω) ∂P, Monotone fun (t : ι) => predictableConvexStep hd hs n t ω

theorem MeasureTheory.TendstoInMeasure.ae_le {α : Type u_1} {ι : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [PseudoEMetricSpace E] [Preorder E] [OrderClosedTopology E] {u : Filter ι} [u.NeBot] [u.IsCountablyGenerated] {f g : ι → α → E} {f' g' : α → E} (hf : TendstoInMeasure μ f u f') (hg : TendstoInMeasure μ g u g') (hfg : ∀ (i : ι), f i ≤ᵐ[μ] g i) : f' ≤ᵐ[μ] g'

If f i ≤ g i almost everywhere for all i, f tends to f' in measure and g tends to g' in measure, then f' ≤ g' almost everywhere.

theorem predictablePartLim_monotoneOn_denseSet_ae {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) : ∀ᵐ (ω : Ω) ∂P, MonotoneOn (fun (t : ι) => predictablePartLim hd hs t ω) (denseSet ι)

The predictable part A is almost surely monotone on the countable dense set.

theorem predictablePartLim_monotone_ae {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (hc : ∀ᵐ (ω : Ω) ∂P, IsCadlag fun (x : ι) => S x ω) : ∀ᵐ (ω : Ω) ∂P, Monotone fun (t : ι) => predictablePartLim hd hs t ω

If the paths of S are almost surely càdlàg, then the predictable part A is almost surely monotone: it is monotone on the countable dense set and right-continuous.

theorem isStronglyPredictable_predictableSeqStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (n : ℕ) : MeasureTheory.IsStronglyPredictable 𝓕 (predictableSeqStep P S 𝓕 n)

The mesh step-extension of the discrete predictable part is strongly predictable: it is a finite sum of processes of the form 1_{(pred u, u]} Aⁿ_u, where Aⁿ_u is measurable with respect to the σ-algebra at time pred u.

theorem isStronglyPredictable_predictableConvexStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (n : ℕ) : MeasureTheory.IsStronglyPredictable 𝓕 (predictableConvexStep hd hs n)

The convexly averaged mesh step-extension of the predictable parts is strongly predictable.

theorem IsStronglyPredictable.limsup {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [Preorder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [TopologicalSpace E] [MeasurableSpace E] [BorelSpace E] [TopologicalSpace.PseudoMetrizableSpace E] [ConditionallyCompleteLinearOrder E] [OrderTopology E] [SecondCountableTopology E] {X : ℕ → ι → Ω → E} (hX : ∀ (n : ℕ), MeasureTheory.IsStronglyPredictable 𝓕 (X n)) : MeasureTheory.IsStronglyPredictable 𝓕 fun (t : ι) (ω : Ω) => Filter.limsup (fun (n : ℕ) => X n t ω) Filter.atTop

The pointwise limsup of strongly predictable processes is strongly predictable.

theorem isStronglyPredictable_limsup_predictableConvexStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) : MeasureTheory.IsStronglyPredictable 𝓕 fun (t : ι) (ω : Ω) => Filter.limsup (fun (x : ℕ) => predictableConvexStep hd hs x t ω) Filter.atTop

The limsup of convexly averaged mesh step-extension of the predictable parts is strongly predictable.

theorem limsup_stoppedValue_predictableConvexStep_ae_le_stoppedValue_predictablePartLim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (τ : Ω → WithTop ι) (hc : ∀ᵐ (ω : Ω) ∂P, IsCadlag fun (x : ι) => S x ω) : (fun (ω : Ω) => Filter.limsup (fun (n : ℕ) => MeasureTheory.stoppedValue (predictableConvexStep hd hs n) τ ω) Filter.atTop) ≤ᵐ[P] MeasureTheory.stoppedValue (predictablePartLim hd hs) τ

For each random time τ, almost everywhere, limsup (fun n => stoppedValue 𝒜^n τ ω) atTop ≤ stoppedValue A τ ω.

theorem integral_stoppedValue_predictableConvexStep_tendsto_stoppedValue_predictablePartLim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] [𝓕.IsComplete P] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) (hτ_ne : ∀ (ω : Ω), τ ω ≠ ⊤) (hc : ∀ᵐ (ω : Ω) ∂P, IsCadlag fun (x : ι) => S x ω) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), MeasureTheory.stoppedValue (predictableConvexStep hd hs n) τ ω ∂P) Filter.atTop (nhds (∫ (ω : Ω), MeasureTheory.stoppedValue (predictablePartLim hd hs) τ ω ∂P))

For each finite stopping time τ, ∫ ω, stoppedValue 𝒜^n τ ω ∂P converges to ∫ ω, stoppedValue A τ ω ∂P.

theorem limsup_lintegral_le' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} {L : Filter ι} [L.IsCountablyGenerated] {f : ι → Ω → ENNReal} (g : Ω → ENNReal) (hf_meas : ∀ (i : ι), AEMeasurable (f i) P) (h_bound : ∀ (i : ι), f i ≤ᵐ[P] g) (h_fin : ∫⁻ (ω : Ω), g ω ∂P ≠ ⊤) : Filter.limsup (fun (i : ι) => ∫⁻ (ω : Ω), f i ω ∂P) L ≤ ∫⁻ (ω : Ω), Filter.limsup (fun (i : ι) => f i ω) L ∂P

Reverse Fatou's lemma for the lower Lebesgue integral along a countably generated filter, AEMeasurable version.

theorem limsup_integral_le_integral_limsup_of_le_of_tendsto_integral_posPart_sub {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} [Countable ι] {L : Filter ι} [L.NeBot] [L.IsCountablyGenerated] {X : ι → Ω → ℝ} {W Y : Ω → ℝ} (hX_int : ∀ (i : ι), MeasureTheory.Integrable (X i) P) (hW : MeasureTheory.Integrable W P) (hWX : ∀ (i : ι), W ≤ᵐ[P] X i) (hY : MeasureTheory.Integrable Y P) (hX_bdd : ∀ᵐ (ω : Ω) ∂P, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) L fun (i : ι) => X i ω) (h_tendsto : Filter.Tendsto (fun (i : ι) => ∫ (ω : Ω), max (X i ω - Y ω) 0 ∂P) L (nhds 0)) (hL_int : MeasureTheory.Integrable (fun (ω : Ω) => Filter.limsup (fun (i : ι) => X i ω) L) P) : Filter.limsup (fun (i : ι) => ∫ (ω : Ω), X i ω ∂P) L ≤ ∫ (ω : Ω), Filter.limsup (fun (i : ι) => X i ω) L ∂P

Reverse Fatou's lemma along a countably generated filter for a family uniformly bounded below by an integrable function W.

theorem limsup_lintegral_le_of_tendsto_lintegral_sub {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} {L : Filter ι} [L.IsCountablyGenerated] {X : ι → Ω → ENNReal} {g : Ω → ENNReal} (hX_meas : ∀ (i : ι), AEMeasurable (X i) P) (hg_meas : AEMeasurable g P) (hg_fin : ∫⁻ (ω : Ω), g ω ∂P ≠ ⊤) (h_tendsto : Filter.Tendsto (fun (i : ι) => ∫⁻ (ω : Ω), X i ω - g ω ∂P) L (nhds 0)) : Filter.limsup (fun (i : ι) => ∫⁻ (ω : Ω), X i ω ∂P) L ≤ ∫⁻ (ω : Ω), Filter.limsup (fun (i : ι) => X i ω) L ∂P

Reverse Fatou's lemma for the lower Lebesgue integral along a countably generated filter, when the integral of the truncated difference X i - g tends to 0.

theorem predictableSeqStep_bot {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) (S : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (n : ℕ) : predictableSeqStep P S 𝓕 n ⊥ = 0

The step extension of the discrete predictable part vanishes at ⊥.

theorem predictableConvexStep_bot {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (n : ℕ) : predictableConvexStep hd hs n ⊥ = 0

The convexly averaged step extension of the predictable parts vanishes at ⊥.

theorem integrable_stoppedValue_predictableSeqStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} {τ : Ω → WithTop ι} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) (hτ_ne : ∀ (ω : Ω), τ ω ≠ ⊤) (m : ℕ) : MeasureTheory.Integrable (MeasureTheory.stoppedValue (predictableSeqStep P S 𝓕 m) τ) P

The stopped step extension of the discrete predictable part is integrable.

theorem integrable_stoppedValue_predictableConvexStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} {τ : Ω → WithTop ι} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) (hτ_ne : ∀ (ω : Ω), τ ω ≠ ⊤) (n : ℕ) : MeasureTheory.Integrable (MeasureTheory.stoppedValue (predictableConvexStep hd hs n) τ) P

The stopped convexly averaged step extension of the predictable parts is integrable.

theorem integrable_stoppedValue_predictablePartLim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} {τ : Ω → WithTop ι} [𝓕.IsRightContinuous] [𝓕.IsComplete P] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) (hτ_ne : ∀ (ω : Ω), τ ω ≠ ⊤) : MeasureTheory.Integrable (MeasureTheory.stoppedValue (predictablePartLim hd hs) τ) P

The predictable part of the Doob-Meyer decomposition stopped at a finite stopping time is integrable.

theorem limsup_stoppedValue_predictableConvexStep_ae_eq_stoppedValue_predictablePartLim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] [𝓕.IsComplete P] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) (hτ_ne : ∀ (ω : Ω), τ ω ≠ ⊤) (hc : ∀ᵐ (ω : Ω) ∂P, IsCadlag fun (x : ι) => S x ω) : (fun (ω : Ω) => Filter.limsup (fun (n : ℕ) => MeasureTheory.stoppedValue (predictableConvexStep hd hs n) τ ω) Filter.atTop) =ᵐ[P] MeasureTheory.stoppedValue (predictablePartLim hd hs) τ

For each finite stopping time τ, almost everywhere, limsup (fun n => stoppedValue 𝒜^n τ ω) atTop = stoppedValue A τ ω.

theorem isStronglyProgressive_predictablePartLim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] [OpensMeasurableSpace ι] [𝓕.IsComplete P] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) : MeasureTheory.IsStronglyProgressive 𝓕 (predictablePartLim hd hs)

Under the usual conditions, the predictable part of the decomposition is strongly progressive.

theorem limsup_predictableConvexStep_le_predictablePartLim_ae {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (hc : ∀ᵐ (ω : Ω) ∂P, IsCadlag fun (x : ι) => S x ω) : ∀ᵐ (ω : Ω) ∂P, ∀ (t : ι), Filter.limsup (fun (x : ℕ) => predictableConvexStep hd hs x t ω) Filter.atTop ≤ predictablePartLim hd hs t ω

Almost surely, limsup (predictableConvexStep hd hs · t ω) atTop ≤ predictablePartLim hd hs t ω for all times t.

theorem leftLim_predictablePartLim_le_limsup_predictableConvexStep_ae {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (hc : ∀ᵐ (ω : Ω) ∂P, IsCadlag fun (x : ι) => S x ω) : ∀ᵐ (ω : Ω) ∂P, ∀ (t : ι), Function.leftLim (fun (x : ι) => predictablePartLim hd hs x ω) t ≤ Filter.limsup (fun (x : ℕ) => predictableConvexStep hd hs x t ω) Filter.atTop

Almost surely, the left limit of predictablePartLim hd hs at t is at most limsup (predictableConvexStep hd hs · t ω) atTop, for all times t.

theorem finite_setOf_lt_predictablePartLim_sub_limsup_predictableConvexStep_ae {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] [CompactSpace ι] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (hc : ∀ᵐ (ω : Ω) ∂P, IsCadlag fun (x : ι) => S x ω) : ∀ᵐ (ω : Ω) ∂P, ∀ ε > 0, {t : ι | ε < predictablePartLim hd hs t ω - Filter.limsup (fun (x : ℕ) => predictableConvexStep hd hs x t ω) Filter.atTop}.Finite

Almost surely, for all ε > 0, there are only finitely many times at which limsup (predictableConvexStep hd hs · t ω) atTop is smaller than predictablePartLim hd hs t ω by more than ε: these are times of jumps of size at least ε of the càdlàg path of predictablePartLim hd hs.

theorem limsup_predictableConvexStep_eq_predictablePartLim {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {ι : Type u_3} [CompleteLinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [MeasurableSpace ι] [BorelSpace ι] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] [𝓕.IsComplete P] (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (hc : ∀ᵐ (ω : Ω) ∂P, IsCadlag fun (x : ι) => S x ω) : ∀ᵐ (ω : Ω) ∂P, ∀ (t : ι), Filter.limsup (fun (x : ℕ) => predictableConvexStep hd hs x t ω) Filter.atTop = predictablePartLim hd hs t ω

The processes fun t ω ↦ limsup (predictableConvexStep hd hs · t ω) atTop and predictablePartLim hd hs are indistinguishable.

theorem ProbabilityTheory.ClassD.doob_meyer {ι : Type u_1} {Ω : Type u_2} [CompleteLinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [MeasurableSpace ι] [BorelSpace ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [𝓕.IsRightContinuous] [𝓕.IsComplete P] (hd : ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (hc : ∀ (ω : Ω), IsCadlag fun (x : ι) => S x ω) : ∃ (M : ι → Ω → ℝ) (A : ι → Ω → ℝ), S = M + A ∧ MeasureTheory.Martingale M 𝓕 P ∧ (∀ (ω : Ω), IsCadlag fun (x : ι) => M x ω) ∧ MeasureTheory.IsStronglyPredictable 𝓕 A ∧ (∀ (ω : Ω), IsCadlag fun (x : ι) => A x ω) ∧ (∀ (ω : Ω), Monotone fun (x : ι) => A x ω) ∧ A ⊥ = 0

Doob–Meyer decomposition of a càdlàg submartingale of class D.

theorem ProbabilityTheory.IsLocalSubmartingale.doob_meyer {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (hX : IsLocalSubmartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) : ∃ (M : ι → Ω → ℝ) (A : ι → Ω → ℝ), X = M + A ∧ IsLocalMartingale M 𝓕 P ∧ (∀ (ω : Ω), IsCadlag fun (x : ι) => M x ω) ∧ MeasureTheory.IsStronglyPredictable 𝓕 A ∧ (∀ (ω : Ω), IsCadlag fun (x : ι) => A x ω) ∧ HasLocallyIntegrableSup A 𝓕 P ∧ ∀ (ω : Ω), Monotone fun (x : ι) => A x ω

noncomputable def ProbabilityTheory.IsLocalSubmartingale.martingalePart {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (X : ι → Ω → ℝ) (hX : IsLocalSubmartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) : ι → Ω → ℝ

The local martingale part of the Doob-Meyer decomposition of the local submartingale.

Equations

• ProbabilityTheory.IsLocalSubmartingale.martingalePart X hX hX_cadlag = ⋯.choose

noncomputable def ProbabilityTheory.IsLocalSubmartingale.predictablePart {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (X : ι → Ω → ℝ) (hX : IsLocalSubmartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) : ι → Ω → ℝ

The predictable part of the Doob-Meyer decomposition of the local submartingale.

Equations

• ProbabilityTheory.IsLocalSubmartingale.predictablePart X hX hX_cadlag = ⋯.choose

theorem ProbabilityTheory.IsLocalSubmartingale.martingalePart_add_predictablePart {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (hX : IsLocalSubmartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) : X = martingalePart X hX hX_cadlag + predictablePart X hX hX_cadlag

theorem ProbabilityTheory.IsLocalSubmartingale.isLocalMartingale_martingalePart {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (hX : IsLocalSubmartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) : IsLocalMartingale (martingalePart X hX hX_cadlag) 𝓕 P

theorem ProbabilityTheory.IsLocalSubmartingale.cadlag_martingalePart {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (hX : IsLocalSubmartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) (ω : Ω) : IsCadlag fun (x : ι) => martingalePart X hX hX_cadlag x ω

theorem ProbabilityTheory.IsLocalSubmartingale.isStronglyPredictable_predictablePart {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (hX : IsLocalSubmartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) : MeasureTheory.IsStronglyPredictable 𝓕 (predictablePart X hX hX_cadlag)

theorem ProbabilityTheory.IsLocalSubmartingale.cadlag_predictablePart {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (hX : IsLocalSubmartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) (ω : Ω) : IsCadlag fun (x : ι) => predictablePart X hX hX_cadlag x ω

theorem ProbabilityTheory.IsLocalSubmartingale.hasLocallyIntegrableSup_predictablePart {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (hX : IsLocalSubmartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) : HasLocallyIntegrableSup (predictablePart X hX hX_cadlag) 𝓕 P

theorem ProbabilityTheory.IsLocalSubmartingale.monotone_predictablePart {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasurableSpace ι] (hX : IsLocalSubmartingale X 𝓕 P) (hX_cadlag : ∀ (ω : Ω), IsCadlag fun (x : ι) => X x ω) (ω : Ω) : Monotone fun (x : ι) => predictablePart X hX hX_cadlag x ω