Doob-Meyer decomposition theorem #

source

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

Set ι

The fixed countable dense set used instead of dyadics, with both endpoints adjoined.

Equations

denseSet ι = ⋯.choose ∪ {⊥, ⊤}

Instances For

source

theorem denseSet_countable (ι : Type u_1) [LE ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [SecondCountableTopology ι] :

(denseSet ι).Countable

source

theorem denseSet_dense (ι : Type u_1) [LE ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [SecondCountableTopology ι] :

Dense (denseSet ι)

source

noncomputable def denseEnum (ι : Type u_1) [LE ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [SecondCountableTopology ι] :

ℕ → ι

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

Equations

denseEnum ι = Subtype.val ∘ ⋯.choose

Instances For

source

noncomputable def mesh (ι : Type u_1) [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [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)))

Instances For

source

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

⊥ ∈ mesh ι n

source

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

⊤ ∈ mesh ι n

source

@[implicit_reducible]

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

OrderBot ↥(mesh ι n)

Equations

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

source

@[implicit_reducible]

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

OrderTop ↥(mesh ι n)

Equations

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

source

@[simp]

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

↑⊤ = ⊤

source

@[simp]

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

↑⊥ = ⊥

source

@[implicit_reducible]

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

LocallyFiniteOrder ↥(mesh ι n)

Equations

instLocallyFiniteOrderSubtypeMemFinsetMesh ι n = Fintype.toLocallyFiniteOrder

source

@[implicit_reducible]

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

SuccOrder ↥(mesh ι n)

Equations

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

source

@[implicit_reducible]

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

PredOrder ↥(mesh ι n)

Equations

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

source

@[implicit_reducible]

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

CompleteLinearOrder ↥(mesh ι n)

Equations

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

source

def meshFiltration {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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 ⋯

Instances For

source

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

MeasureTheory.SigmaFiniteFiltration P (meshFiltration 𝓕 n)

source

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 ∈ Finset.Iio n, P[S (Order.succ i) - S i | ↑𝓕 i]

Instances For

source

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.

source

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.

source

@[simp]

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

predictablePart S 𝓕 P ⊥ = 0

source

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.

source

theorem MeasureTheory.Submartingale.monotone_predictablePart_ae {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] [Countable ι] {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 ω

For a submartingale indexed by a countable type, the predictable part is monotone a.e.

source

theorem MeasureTheory.Submartingale.predictablePart_nonneg' {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [LocallyFiniteOrder ι] [OrderBot ι] [SuccOrder ι] [Countable ι] {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 ω

For a submartingale indexed by a countable type, the predictable part is nonnegative a.e.

source

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

Instances For

source

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.

source

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.

source

theorem martingale_martingalePart {ι : 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 Ω) :

MeasureTheory.Martingale (martingalePart S 𝓕 P) 𝓕 P

The martingale part of a process is a martingale.

source

@[simp]

theorem martingalePart_add_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 Ω) :

martingalePart S 𝓕 P + predictablePart S 𝓕 P = S

source

noncomputable def predictableSeqTop {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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 ⊤

Instances For

source

theorem integrable_predictableSeqTop {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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.

source

theorem predictableSeqTop_eq_zero_of_martingale {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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.

source

noncomputable def martingaleSeqTop {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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 ⊤

Instances For

source

theorem martingaleSeqTop_add {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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.

source

theorem martingaleSeqTop_eq_self_of_martingale {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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.

source

theorem martingaleSeqTop_eq_neg_predictableSeqTop {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace 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.

source

theorem equation4 {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {S : ι → Ω → E} {𝓕 : MeasureTheory.Filtration ι mΩ} {n : ℕ} [MeasureTheory.SigmaFiniteFiltration 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. Note that T1 Space is needed to make sure that mesh ι n has order topology.

source

noncomputable def tauMesh {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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) ⊥ ⊤ ω)

Instances For

source

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

tauMesh S 𝓕 P n c ω ≤ ↑⊤

source

theorem stoppedValue_predictablePart_tauMesh_le {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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.

source

theorem isPredictable_predictablePart {ι : 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.IsStronglyPredictable 𝓕 (predictablePart S 𝓕 P)

The predictable part is predictable.

source

theorem stronglyMeasurable_pred_predictablePart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [PredOrder ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace 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.

source

theorem stronglyMeasurable_predictablePart {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [PredOrder ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace 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.

source

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

MeasureTheory.StronglyAdapted 𝓕 (predictablePart S 𝓕 P)

The predictable part of a process is strongly adapted.

source

theorem stronglyAdapted_predictablePart' {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace 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.

source

theorem isStoppingTime_tauMesh {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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.

source

theorem stoppedValue_le_neg_condExp_predictableSeqTop_add_const {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} (hstop : S ⊤ =ᵐ[P] 0) (𝓕 : MeasureTheory.Filtration ι mΩ) (n : ℕ) [MeasureTheory.SigmaFiniteFiltration 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.

source

theorem MeasureTheory.Submartingale.tauMesh_lt_top_eq_lt_predictableSeqTop {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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ⁿ₁}.

source

theorem MeasureTheory.Submartingale.integrableOn_const_tauMesh_lt_top {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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.

source

theorem MeasureTheory.Submartingale.integrable_stoppedValue_tauMesh {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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.

source

theorem first_estimate {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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.

source

theorem tauMesh_lt_top_subset_of_lt {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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}.

source

theorem integrable_stoppedValue_predictablePart_tauMesh {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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.

source

theorem second_estimate {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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.

source

theorem equation5 {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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

source

theorem equation5' {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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

source

noncomputable def tauMeshLift {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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

Instances For

source

@[simp]

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

tauMesh S 𝓕 P n c ω ≠ ⊤

source

@[simp]

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

tauMeshLift S 𝓕 P n c ω ≠ ⊤

source

theorem stoppedValue_tauMeshLift {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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)

source

theorem isStoppingTime_tauMeshLift {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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.

source

theorem integral_predictableSeqTop_eq_neg_integral_bot {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasureTheory.SigmaFiniteFiltration P 𝓕] (hstop : S ⊤ =ᵐ[P] 0) (n : ℕ) :

∫ (ω : Ω), predictableSeqTop S 𝓕 P n ω ∂P = -∫ (ω : Ω), S ⊥ ω ∂P

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

source

theorem measure_tauMesh_lt_top_le {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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}.

source

theorem uniformIntegrable_predictableSeqTop {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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 ω ≠ ⊤}) => MeasureTheory.stoppedValue S ↑τ) 1 P) (hstop : S ⊤ =ᵐ[P] 0) (ht : ∀ (t : ι), S t ≤ᵐ[P] 0) :

MeasureTheory.UniformIntegrable (predictableSeqTop S 𝓕 P) 1 P

The terminal values of the predictable parts are uniformly integrable.

source

theorem uniformIntegrable_martingaleSeqTopAux {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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 ω ≠ ⊤}) => MeasureTheory.stoppedValue S ↑τ) 1 P) (hstop : S ⊤ =ᵐ[P] 0) (ht : ∀ (t : ι), S t ≤ᵐ[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.

source

theorem uniformIntegrable_martingaleSeqTop {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : MeasureTheory.UniformIntegrable (fun (τ : ↑{T : Ω → WithTop ι | MeasureTheory.IsStoppingTime 𝓕 T ∧ ∀ (ω : Ω), T ω ≠ ⊤}) => 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 and ∀ t, S t ≤ᵐ[P] 0.

source

theorem exists_martingalPart_lim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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 ℝ ℕ), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (((a n).weights.sum fun (m : ℕ) (r : ℝ) => r • martingaleSeqTop S 𝓕 P m) - M) 1 P) Filter.atTop (nhds 0)

Show that the terminals values of some convex combinations of the martingale parts converge.

source

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

Ω → ℝ

This is the martingalePart in the doob-meyer decomposition of a submartingale.

Equations

martingalePartLim hd hs i = P[⋯.choose | ↑𝓕 i]

Instances For

source

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

MeasureTheory.Martingale (martingalePartLim hd hs) 𝓕 P

source

noncomputable def weight {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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

Instances For

source

noncomputable def martingaleSeqStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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]

Instances For

source

noncomputable def martingaleConvexStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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).weights.sum fun (m : ℕ) (r : ℝ) => r • martingaleSeqStep P S 𝓕 m

Instances For

source

theorem martingaleConvexStep_eLpNorm_tendsto {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (n : ℕ) (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.

source

def meshPredIoc {ι : Type u_1} [LinearOrder ι] [OrderBot ι] [OrderTop ι] [TopologicalSpace ι] [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

Instances For

source

noncomputable def predictableSeqStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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

Instances For

source

noncomputable def predictableConvexStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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).weights.sum fun (m : ℕ) (r : ℝ) => r • predictableSeqStep P S 𝓕 m

Instances For

source

noncomputable def predictablePartLim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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.

Equations

predictablePartLim hd hs = S - martingalePartLim hd hs

Instances For

source

theorem predictableConvexStep_eLpNorm_tendsto {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) (n : ℕ) {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 ι.

source

theorem predictableConvexStep_ae_tendsto {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) {t : ι} (ht : t ∈ denseSet ι) :

∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (n : ℕ) => predictableConvexStep hd hs (φ n) t ω) Filter.atTop (nhds (predictablePartLim hd hs t ω))

Almost everywhere convergence of predictableConvexStep.

source

theorem monotone_of_frequently_monotone_of_tendsto {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [TopologicalSpace β] [Preorder β] [OrderClosedTopology β] {l : Filter ι} {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 frequently monotone is monotone.

source

theorem antitone_of_frequently_antitone_of_tendsto {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [TopologicalSpace β] [Preorder β] [OrderClosedTopology β] {l : Filter ι} {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 frequently antitone is antitone.

source

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.

source

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.

source

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.

source

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.

source

theorem Dense.comap_val_nhdsWithin_Ioi_neBot {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {D : Set α} (hD : Dense D) {a b : α} (hab : a < b) :

(Filter.comap Subtype.val (nhdsWithin a (Set.Ioi a))).NeBot

This is an auxillary lemma used to prove Dense.monotone_of_isRightContinuous. It is saying that if D is a dense set and a, b are two points such that a < b, then the comap of 𝓝[Set.Ioi a] a under the inclusion D → α is nontrivial. Note that a < b is necessary as this is clearly not true if a is a top element.

source

theorem Dense.comap_val_nhdsWithin_Iio_neBot {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {D : Set α} (hD : Dense D) {a b : α} (hab : b < a) :

(Filter.comap Subtype.val (nhdsWithin a (Set.Iio a))).NeBot

This is the dual of Dense.comap_val_nhdsWithin_Ioi_neBot.

source

theorem Dense.monotone_of_isRightContinuous {α : Type u_1} {β : Type u_2} [LinearOrder α] [OrderTop α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [TopologicalSpace β] [Preorder β] [t : OrderClosedTopology β] {f : α → β} {D : Set α} (hD : Dense D) (htop : ⊤ ∈ D) (hm : Monotone (f ∘ Subtype.val)) (hf : Function.IsRightContinuous f) :

Monotone f

If f is monotone on a dense set D and is right continuous, then f is monotone. We prove under the assumption that α has a top element ⊤ and ⊤ ∈ D, which is a necessary assumption because otherwise it is possible that ⊤ is an isolated point. This theorem should be also true when α satisfies NoTopOrder α.

source

theorem Filter.IsCoboundedUnder.trans {ι : Type u_1} {α : Type u_2} {r : α → α → Prop} {l : Filter ι} [l.NeBot] [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.

source

theorem limsup_le_of_eventually_monotone_of_tendsto_on_dense {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrder α] [BoundedOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {l : Filter ι} [l.NeBot] {D : Set α} {F : ι → α → β} {f : α → β} (hF : ∀ᶠ (i : ι) in l, Monotone (F i)) (hD : Dense D) (htop : ⊤ ∈ 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. We prove this under the assumption that α has both a bottom element and a top element. The bottom element is needed because otherwise limsup evaluated at the bottome element may give a junk value to break the inequality.

source

theorem le_liminf_of_eventually_monotone_of_tendsto_on_dense {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrder α] [BoundedOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {l : Filter ι} [l.NeBot] {D : Set α} {F : ι → α → β} {f : α → β} (hF : ∀ᶠ (i : ι) in l, Monotone (F i)) (hD : Dense D) (htop : ⊤ ∈ D) (hbot : ⊥ ∈ 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.

source

theorem tendsto_of_eventually_monotone_of_tendsto_on_dense {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrder α] [BoundedOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {l : Filter ι} [l.NeBot] {D : Set α} {F : ι → α → β} {f : α → β} (hF : ∀ᶠ (i : ι) in l, Monotone (F i)) (hD : Dense 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.

source

theorem predictableSeqStep_eq_sum_indicator {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [SecondCountableTopology ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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

source

theorem predictableSeqStep_monotone_ae {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hs : MeasureTheory.Submartingale S 𝓕 P) (n : ℕ) (t : ι) :

∀ᵐ (ω : Ω) ∂P, Monotone fun (t : ι) => predictableSeqStep P S 𝓕 n t ω

source

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

∀ᵐ (ω : Ω) ∂P, Monotone fun (t : ι) => predictableConvexStep hd hs n t ω

source

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

∀ᵐ (ω : Ω) ∂P, Monotone fun (t : ι) => predictablePartLim hd hs t ω

source

theorem continuousWithinAt_Iio_indicator_Ioc {α : Type u_1} {M : Type u_2} [LinearOrder α] [TopologicalSpace α] [ClosedIicTopology α] [Zero M] [TopologicalSpace M] (a b : α) (c : M) (t : α) :

ContinuousWithinAt ((Set.Ioc a b).indicator fun (x : α) => c) (Set.Iio t) t

The indicator of a half-open interval Ioc a b with constant value c is left-continuous: when approached from the left it is eventually constant, so it is continuous within Iio t at t for every t.

source

theorem predictableSeqStep_leftContinuous {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [ClosedIicTopology ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (n : ℕ) (ω : Ω) (t : ι) :

ContinuousWithinAt (fun (s : ι) => predictableSeqStep P S 𝓕 n s ω) (Set.Iio t) t

The mesh step-extension of the discrete predictable part is left-continuous in time.

source

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

ContinuousWithinAt (fun (s : ι) => predictableConvexStep hd hs n s ω) (Set.Iio t) t

predictableConvexStep is left-continuous in time.

source

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

MeasureTheory.StronglyAdapted 𝓕 (predictableSeqStep P S 𝓕 n)

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

source

theorem stronglyAdapted_predictableConvexStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] {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.

source

theorem isStronglyPredictable_predictableConvexStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] [DenselyOrdered ι] {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.

source

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.

source

theorem isStronglyPredictable_limsup_predictableConvexStep {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] [DenselyOrdered ι] {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.

source

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

Filter.limsup (fun (n : ℕ) => MeasureTheory.stoppedValue (predictableConvexStep hd hs n) τ) Filter.atTop ≤ᵐ[P] MeasureTheory.stoppedValue (predictablePartLim hd hs) τ

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

source

theorem integral_stoppedValue_predictableConvexStep_tendsto_stoppedValue_predictablePartLim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] [DenselyOrdered ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) :

Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), MeasureTheory.stoppedValue (predictableConvexStep hd hs n) τ ω ∂P) Filter.atTop (nhds (∫ (ω : Ω), MeasureTheory.stoppedValue (predictablePartLim hd hs) τ ω ∂P))

Prove that ∫ ω, stoppedValue 𝒜^n τ ω ∂P converges to ∫ ω, stoppedValue A τ ω ∂P.

source

theorem limsup_integral_le_integral_limsup_of_tendsto_integral_posPart_sub {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ℕ → Ω → ℝ} {Y : Ω → ℝ} (hX_nonneg : ∀ (n : ℕ), 0 ≤ᵐ[P] X n) (hY : MeasureTheory.Integrable Y P) (hY_nonneg : 0 ≤ᵐ[P] Y) (h_tendsto : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), max (X n ω - Y ω) 0 ∂P) Filter.atTop (nhds 0)) :

Filter.limsup (fun (n : ℕ) => ∫ (ω : Ω), X n ω ∂P) Filter.atTop ≤ ∫ (ω : Ω), Filter.limsup (fun (n : ℕ) => X n ω) Filter.atTop ∂P

Reverse Fatou's lemma. See also limsup_lintegral_le.

source

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

Filter.limsup (fun (n : ℕ) => MeasureTheory.stoppedValue (predictableConvexStep hd hs n) τ) Filter.atTop =ᵐ[P] MeasureTheory.stoppedValue (predictablePartLim hd hs) τ

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

source

theorem limsup_predictableConvexStep_eq_predictablePartLim {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [OrderTopology ι] [DenselyOrdered ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hd : ProbabilityTheory.ClassD S 𝓕 P) (hs : MeasureTheory.Submartingale S 𝓕 P) {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime 𝓕 τ) :

∀ᵐ (ω : Ω) ∂P, ∀ (t : ι), Filter.limsup (fun (x : ℕ) => predictableConvexStep hd hs x t ω) Filter.atTop = predictablePartLim hd hs t ω

Show that fun t ω => limsup (predictableConvexStep hd hs · t ω and predictablePartLim hd hs are indistinguishable.

source

theorem ClassD.doob_meyer {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [T1Space ι] [SecondCountableTopology ι] [MeasurableSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTop ι] [SuccOrder ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {S : ι → Ω → ℝ} {𝓕 : MeasureTheory.Filtration ι mΩ} (hs : MeasureTheory.Submartingale S 𝓕 P) :

∃ (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 ω

source

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.IsStronglyProgressive 𝓕 A ∧ (∀ (ω : Ω), IsCadlag fun (x : ι) => A x ω) ∧ HasLocallyIntegrableSup A 𝓕 P ∧ ∀ (ω : Ω), Monotone fun (x : ι) => A x ω

source

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

Instances For

source

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

Instances For

source

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

source

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

source

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 ω

source

theorem ProbabilityTheory.IsLocalSubmartingale.isStronglyProgressive_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.IsStronglyProgressive 𝓕 (predictablePart X hX hX_cadlag)

source

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 ω

source

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

source

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 ω

Documentation

BrownianMotion.StochasticIntegral.DoobMeyer

Doob-Meyer decomposition theorem #