Discrete approximation of a stopping time

structure MeasureTheory.DiscreteApproxSequence {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} (𝓕 : Filtration ι mΩ) (τ : Ω → WithTop ι) (μ : Measure Ω := by volume_tac) : Type (max u_1 u_2)

Given a random time τ, a discrete approximation sequence τn of τ is a sequence of stopping times with countable range that converges to τ from above almost surely.

• seq : ℕ → Ω → WithTop ι

  The sequence of stopping times approximating τ.

• isStoppingTime (n : ℕ) : IsStoppingTime 𝓕 (self.seq n)

  Each τn is a stopping time.

• countable (n : ℕ) : (Set.range (self.seq n)).Countable

  Each τn has countable range.

• antitone : Antitone self.seq

  The sequence is antitone.

• le (n : ℕ) : τ ≤ self.seq n

  Each τn is greater than or equal to τ.

• tendsto : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (x : ℕ) => self.seq x ω) Filter.atTop (nhds (τ ω))

  The sequence converges to τ almost surely.

theorem MeasureTheory.DiscreteApproxSequence.ext {ι : Type u_1} {Ω : Type u_2} {inst✝ : TopologicalSpace ι} {inst✝¹ : LinearOrder ι} {inst✝² : OrderTopology ι} {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {τ : Ω → WithTop ι} {μ : autoParam (Measure Ω) _auto✝} {x y : DiscreteApproxSequence 𝓕 τ μ} (seq : x.seq = y.seq) : x = y

theorem MeasureTheory.DiscreteApproxSequence.ext_iff {ι : Type u_1} {Ω : Type u_2} {inst✝ : TopologicalSpace ι} {inst✝¹ : LinearOrder ι} {inst✝² : OrderTopology ι} {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {τ : Ω → WithTop ι} {μ : autoParam (Measure Ω) _auto✝} {x y : DiscreteApproxSequence 𝓕 τ μ} : x = y ↔ x.seq = y.seq

instance MeasureTheory.instFunLikeDiscreteApproxSequenceNatForallWithTop {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {τ : Ω → WithTop ι} : FunLike (DiscreteApproxSequence 𝓕 τ μ) ℕ (Ω → WithTop ι)

Equations

• MeasureTheory.instFunLikeDiscreteApproxSequenceNatForallWithTop = { coe := fun (s : MeasureTheory.DiscreteApproxSequence 𝓕 τ μ) => s.seq, coe_injective' := ⋯ }

theorem MeasureTheory.isStoppingTime_const' {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {ι : Type u_4} [Preorder ι] (f : Filtration ι mΩ) (i : WithTop ι) : IsStoppingTime f fun (x : Ω) => i

class MeasureTheory.Approximable {ι : Type u_4} {Ω : Type u_5} {mΩ : MeasurableSpace Ω} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] (𝓕 : Filtration ι mΩ) (μ : Measure Ω := by volume_tac) : Type (max u_4 u_5)

A time index ι is said to be approximable if for any stopping time τ on ι, there exists a discrete approximation sequence of τ.

• approxSeq (τ : Ω → WithTop ι) : IsStoppingTime 𝓕 τ → DiscreteApproxSequence 𝓕 τ μ

  For any stopping time τ, there exists a discrete approximation sequence of τ.

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

Given a stopping time τ on an approximable time index, we obtain an associated discrete approximation sequence.

Equations

• h.discreteApproxSequence μ = MeasureTheory.Approximable.approxSeq τ h

instance Nat.approximable {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration ℕ mΩ} : MeasureTheory.Approximable 𝓕 μ

Equations

• Nat.approximable = sorry

instance NNReal.approximable {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝓕 : MeasureTheory.Filtration NNReal mΩ} : MeasureTheory.Approximable 𝓕 μ

Equations

• NNReal.approximable = sorry

def MeasureTheory.discreteApproxSequence_const {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {μ : Measure Ω} (𝓕 : Filtration ι mΩ) (i : WithTop ι) : DiscreteApproxSequence 𝓕 (Function.const Ω i) μ

The constant discrete approximation sequence.

Equations

• MeasureTheory.discreteApproxSequence_const 𝓕 i = { seq := fun (x : ℕ) (x_1 : Ω) => i, isStoppingTime := ⋯, countable := ⋯, antitone := ⋯, le := ⋯, tendsto := ⋯ }

theorem MeasureTheory.tendsto_stoppedValue_discreteApproxSequence {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {X : ι → Ω → ℝ} {τ : Ω → WithTop ι} [Nonempty ι] (τn : DiscreteApproxSequence 𝓕 τ μ) (hX : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => stoppedValue X (τn.seq n) ω) Filter.atTop (nhds (stoppedValue X τ ω))

def MeasureTheory.discreteApproxSequence_of {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {τ : Ω → WithTop ι} {i : ι} (𝓕 : Filtration ι mΩ) (hτ : ∀ (ω : Ω), τ ω ≤ ↑i) (τn : DiscreteApproxSequence 𝓕 τ μ) : DiscreteApproxSequence 𝓕 τ μ

For τ a time bounded by i and τn a discrete approximation sequence of τ, discreteApproxSequence_of is the discrete approximation sequence of τ defined by τn ∧ i.

Equations

• MeasureTheory.discreteApproxSequence_of 𝓕 hτ τn = { seq := fun (m : ℕ) => τn m ⊓ Function.const Ω ↑i, isStoppingTime := ⋯, countable := ⋯, antitone := ⋯, le := ⋯, tendsto := ⋯ }

theorem MeasureTheory.discreteApproxSequence_of_le {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {τ : Ω → WithTop ι} {i : ι} (hτ : ∀ (ω : Ω), τ ω ≤ ↑i) (τn : DiscreteApproxSequence 𝓕 τ μ) (m : ℕ) (ω : Ω) : (discreteApproxSequence_of 𝓕 hτ τn) m ω ≤ ↑i

def MeasureTheory.DiscreteApproxSequence.inf {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {τ σ : Ω → WithTop ι} (τn : DiscreteApproxSequence 𝓕 τ μ) (σn : DiscreteApproxSequence 𝓕 σ μ) : DiscreteApproxSequence 𝓕 (τ ⊓ σ) μ

The minimum of two discrete approximation sequences is a discrete approximation sequence of the minimum of the two stopping times.

Equations

• τn.inf σn = { seq := fun (m : ℕ) => τn m ⊓ σn m, isStoppingTime := ⋯, countable := ⋯, antitone := ⋯, le := ⋯, tendsto := ⋯ }

def MeasureTheory.DiscreteApproxSequence.inf' {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {τ : Ω → WithTop ι} (τn τn' : DiscreteApproxSequence 𝓕 τ μ) : DiscreteApproxSequence 𝓕 τ μ

The minimum of two discrete approximation sequence of the same stopping time.

Equations

• τn.inf' τn' = { seq := fun (m : ℕ) => τn m ⊓ τn' m, isStoppingTime := ⋯, countable := ⋯, antitone := ⋯, le := ⋯, tendsto := ⋯ }

@[simp]

theorem MeasureTheory.DiscreteApproxSequence.inf'_eq {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {τ : Ω → WithTop ι} (τn τn' : DiscreteApproxSequence 𝓕 τ μ) (n : ℕ) : (τn.inf' τn') n = τn n ⊓ τn' n

@[simp]

theorem MeasureTheory.DiscreteApproxSequence.inf'_apply {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {τ : Ω → WithTop ι} (τn τn' : DiscreteApproxSequence 𝓕 τ μ) (n : ℕ) (ω : Ω) : (τn.inf' τn') n ω = min (τn n ω) (τn' n ω)

instance MeasureTheory.instLEDiscreteApproxSequence {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {τ : Ω → WithTop ι} : LE (DiscreteApproxSequence 𝓕 τ μ)

Equations

• MeasureTheory.instLEDiscreteApproxSequence = { le := fun (τn σn : MeasureTheory.DiscreteApproxSequence 𝓕 τ μ) => ∀ (n : ℕ), τn n ≤ σn n }

instance MeasureTheory.instPartialOrderDiscreteApproxSequence {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {τ : Ω → WithTop ι} : PartialOrder (DiscreteApproxSequence 𝓕 τ μ)

Equations

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

instance MeasureTheory.instSemilatticeInfDiscreteApproxSequence {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {τ : Ω → WithTop ι} : SemilatticeInf (DiscreteApproxSequence 𝓕 τ μ)

Equations

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

theorem MeasureTheory.DiscreteApproxSequence.discreteApproxSequence_of_le_inf_le_of_left {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {τ σ : Ω → WithTop ι} {i : ι} (τn : DiscreteApproxSequence 𝓕 τ μ) (σn : DiscreteApproxSequence 𝓕 σ μ) (hτ : ∀ (ω : Ω), τ ω ≤ ↑i) (m : ℕ) (ω : Ω) : ((discreteApproxSequence_of 𝓕 hτ τn).inf σn) m ω ≤ ↑i

theorem MeasureTheory.uniformIntegrable_stoppedValue_discreteApproxSequence_of_le {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {X : ι → Ω → ℝ} {τ : Ω → WithTop ι} {i : ι} [Nonempty ι] [OrderBot ι] [FirstCountableTopology ι] [IsFiniteMeasure μ] (h : Martingale X 𝓕 μ) (τn : DiscreteApproxSequence 𝓕 τ μ) (hτn_le : ∀ (n : ℕ) (ω : Ω), τn n ω ≤ ↑i) : UniformIntegrable (fun (m : ℕ) => stoppedValue X (τn m)) 1 μ

theorem MeasureTheory.uniformIntegrable_stoppedValue_discreteApproxSequence {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {X : ι → Ω → ℝ} {τ : Ω → WithTop ι} {i : ι} [Nonempty ι] [OrderBot ι] [FirstCountableTopology ι] [IsFiniteMeasure μ] (h : Martingale X 𝓕 μ) (hτ_le : ∀ (ω : Ω), τ ω ≤ ↑i) (τn : DiscreteApproxSequence 𝓕 τ μ) : UniformIntegrable (fun (m : ℕ) => stoppedValue X ((discreteApproxSequence_of 𝓕 hτ_le τn) m)) 1 μ

theorem MeasureTheory.integrable_stoppedValue_of_discreteApproxSequence {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {X : ι → Ω → ℝ} {τ : Ω → WithTop ι} {i : ι} [Nonempty ι] [OrderBot ι] [FirstCountableTopology ι] [IsFiniteMeasure μ] (h : Martingale X 𝓕 μ) (hτ_le : ∀ (ω : Ω), τ ω ≤ ↑i) (τn : DiscreteApproxSequence 𝓕 τ μ) (m : ℕ) : Integrable (stoppedValue X ((discreteApproxSequence_of 𝓕 hτ_le τn) m)) μ

theorem MeasureTheory.aestronglyMeasurable_stoppedValue_of_discreteApproxSequence {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {X : ι → Ω → ℝ} {τ : Ω → WithTop ι} {i : ι} [Nonempty ι] [OrderBot ι] [FirstCountableTopology ι] [IsFiniteMeasure μ] (h : Martingale X 𝓕 μ) (hRC : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω) (hτ_le : ∀ (ω : Ω), τ ω ≤ ↑i) (τn : DiscreteApproxSequence 𝓕 τ μ) : AEStronglyMeasurable (stoppedValue X τ) μ

theorem MeasureTheory.stoppedValue_ae_eq_condExp_discreteApproxSequence_of {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {X : ι → Ω → ℝ} {τ : Ω → WithTop ι} {i : ι} [Nonempty ι] [OrderBot ι] [FirstCountableTopology ι] [IsFiniteMeasure μ] (h : Martingale X 𝓕 μ) (hτ_le : ∀ (ω : Ω), τ ω ≤ ↑i) (τn : DiscreteApproxSequence 𝓕 τ μ) (m : ℕ) : stoppedValue X ((discreteApproxSequence_of 𝓕 hτ_le τn) m) =ᶠ[ae μ] μ[X i|⋯.measurableSpace]

theorem MeasureTheory.tendsto_eLpNorm_stoppedValue_of_discreteApproxSequence {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {X : ι → Ω → ℝ} {τ : Ω → WithTop ι} {i : ι} [Nonempty ι] [OrderBot ι] [FirstCountableTopology ι] [IsFiniteMeasure μ] (h : Martingale X 𝓕 μ) (hRC : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω) (hτ_le : ∀ (ω : Ω), τ ω ≤ ↑i) (τn : DiscreteApproxSequence 𝓕 τ μ) : Filter.Tendsto (fun (i_1 : ℕ) => eLpNorm (stoppedValue X ((discreteApproxSequence_of 𝓕 hτ_le τn) i_1) - stoppedValue X τ) 1 μ) Filter.atTop (nhds 0)

theorem MeasureTheory.integrable_stoppedValue_of_discreteApproxSequence' {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {X : ι → Ω → ℝ} {τ : Ω → WithTop ι} {i : ι} [Nonempty ι] [OrderBot ι] [FirstCountableTopology ι] [IsFiniteMeasure μ] (h : Martingale X 𝓕 μ) (hRC : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω) (hτ_le : ∀ (ω : Ω), τ ω ≤ ↑i) (τn : DiscreteApproxSequence 𝓕 τ μ) : Integrable (stoppedValue X τ) μ

theorem MeasureTheory.tendsto_eLpNorm_stoppedValue_of_discreteApproxSequence_of_le {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] {mΩ : MeasurableSpace Ω} {𝓕 : Filtration ι mΩ} {μ : Measure Ω} {X : ι → Ω → ℝ} {τ : Ω → WithTop ι} {i : ι} [Nonempty ι] [OrderBot ι] [FirstCountableTopology ι] [IsFiniteMeasure μ] (h : Martingale X 𝓕 μ) (hRC : ∀ (ω : Ω), Function.RightContinuous fun (x : ι) => X x ω) (τn : DiscreteApproxSequence 𝓕 τ μ) (hτn_le : ∀ (n : ℕ) (ω : Ω), τn n ω ≤ ↑i) : Filter.Tendsto (fun (i : ℕ) => eLpNorm (stoppedValue X (τn i) - stoppedValue X τ) 1 μ) Filter.atTop (nhds 0)