The debut of a set

The debut after n of a set E ⊆ ι × Ω is the random time ω ↦ inf {t ≥ n | (t, ω) ∈ E}.

Main definitions

• MeasureTheory.debut E n: the debut of E after n.
• MeasureTheory.ProgMeasurableSet E 𝓕: the set E is progressively measurable for the filtration 𝓕.

Main statements

• MeasureTheory.IsPavingAnalytic.nullMeasurable_debut: the debut of an analytic set is null-measurable with respect to any s-finite measure.
• MeasureTheory.isStoppingTime_debut: debut theorem. The debut of a progressively measurable set is a stopping time, for a filtration that is right-continuous and complete with respect to an s-finite measure.
• MeasureTheory.IsStronglyProgressive.isStoppingTime_hittingAfter: the hitting time of a measurable set by a progressively measurable process is a stopping time, under the same assumptions on the filtration.

Implementation notes

We follow the implementation of hitting times in Mathlib.Probability.Process.HittingTime. The debut has values in WithTop ι, ensuring that it is always well-defined.

References

• [S. He, J. Wang and J. Yan, Semimartingale theory and stochastic calculus][he2019semimartingale]

instance MeasureTheory.instMeasurableInf₂WithTopNNReal_brownianMotion : MeasurableInf₂ (WithTop NNReal)

noncomputable def MeasureTheory.debut {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [InfSet ι] (E : Set (ι × Ω)) (n : ι) : Ω → WithTop ι

The debut of a set E ⊆ ι × Ω after n is the random variable that gives the smallest t ≥ n such that (t, ω) ∈ E for a given ω, or ⊤ if there is no such t.

Equations

• MeasureTheory.debut E n = MeasureTheory.hittingAfter (fun (t : ι) (ω : Ω) => (t, ω)) E n

theorem MeasureTheory.debut_eq_ite {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [InfSet ι] (E : Set (ι × Ω)) (n : ι) : debut E n = fun (ω : Ω) => if ∃ t ≥ n, (t, ω) ∈ E then ↑(sInf {t : ι | t ≥ n ∧ (t, ω) ∈ E}) else ⊤

theorem MeasureTheory.debut_eq_hittingAfter_indicator {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [InfSet ι] (E : Set (ι × Ω)) [(t : ι) → (ω : Ω) → Decidable ((t, ω) ∈ E)] (n : ι) : debut E n = hittingAfter (fun (t : ι) (ω : Ω) => if (t, ω) ∈ E then 1 else 0) {1} n

theorem MeasureTheory.hittingAfter_eq_debut {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [InfSet ι] {β : Type u_3} (u : ι → Ω → β) (s : Set β) (n : ι) : hittingAfter u s n = debut {p : ι × Ω | u p.1 p.2 ∈ s} n

@[simp]

theorem MeasureTheory.debut_empty {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [InfSet ι] (n : ι) : debut ∅ n = fun (x : Ω) => ⊤

The debut of the empty set is the constant function that returns ⊤.

@[simp]

theorem MeasureTheory.debut_univ {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLattice ι] (n : ι) : debut Set.univ n = fun (x : Ω) => ↑n

@[simp]

theorem MeasureTheory.debut_prod {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [InfSet ι] (n : ι) (I : Set ι) (A : Set Ω) : debut (I ×ˢ A) n = fun (ω : Ω) => if (Set.Ici n ∩ I).Nonempty then if ω ∈ A then ↑(sInf (Set.Ici n ∩ I)) else ⊤ else ⊤

theorem MeasureTheory.debut_prod_univ {Ω : Type u_1} {ι : Type u_2} [Preorder ι] [InfSet ι] (n : ι) (I : Set ι) [Decidable (Set.Ici n ∩ I).Nonempty] : debut (I ×ˢ Set.univ) n = fun (x : Ω) => if (Set.Ici n ∩ I).Nonempty then ↑(sInf (Set.Ici n ∩ I)) else ⊤

theorem MeasureTheory.debut_univ_prod {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLattice ι] (n : ι) (A : Set Ω) [DecidablePred fun (x : Ω) => x ∈ A] : debut (Set.univ ×ˢ A) n = fun (ω : Ω) => if ω ∈ A then ↑n else ⊤

theorem MeasureTheory.debut_anti {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrder ι] (n : ι) : Antitone fun (x : Set (ι × Ω)) => debut x n

theorem MeasureTheory.notMem_of_lt_debut {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrder ι] {E : Set (ι × Ω)} {n t : ι} {ω : Ω} (ht : ↑t < debut E n ω) (hnt : n ≤ t) : (t, ω) ∉ E

theorem MeasureTheory.debut_eq_top_iff {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrder ι] {E : Set (ι × Ω)} {n : ι} {ω : Ω} : debut E n ω = ⊤ ↔ ∀ t ≥ n, (t, ω) ∉ E

theorem MeasureTheory.debut_ne_top_iff {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrder ι] {E : Set (ι × Ω)} {n : ι} {ω : Ω} : debut E n ω ≠ ⊤ ↔ ∃ t ≥ n, (t, ω) ∈ E

theorem MeasureTheory.le_debut {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrder ι] {E : Set (ι × Ω)} {n : ι} (ω : Ω) : ↑n ≤ debut E n ω

theorem MeasureTheory.debut_mem_set {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrder ι] {E : Set (ι × Ω)} {n : ι} {ω : Ω} [WellFoundedLT ι] (h : ∃ t ≥ n, (t, ω) ∈ E) : ((debut E n ω).untopA, ω) ∈ E

theorem MeasureTheory.debut_mem_set_of_ne_top {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrder ι] {E : Set (ι × Ω)} {n : ι} {ω : Ω} [WellFoundedLT ι] (h : debut E n ω ≠ ⊤) : ((debut E n ω).untopA, ω) ∈ E

theorem MeasureTheory.debut_le_of_mem {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrder ι] {E : Set (ι × Ω)} {n t : ι} {ω : Ω} (ht : n ≤ t) (h_mem : (t, ω) ∈ E) : debut E n ω ≤ ↑t

theorem MeasureTheory.debut_le_iff {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrder ι] {E : Set (ι × Ω)} {n t : ι} {ω : Ω} [WellFoundedLT ι] : debut E n ω ≤ ↑t ↔ ∃ j ∈ Set.Icc n t, (j, ω) ∈ E

theorem MeasureTheory.debut_lt_iff {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrder ι] {E : Set (ι × Ω)} {n t : ι} {ω : Ω} : debut E n ω < ↑t ↔ ∃ j ∈ Set.Ico n t, (j, ω) ∈ E

theorem MeasureTheory.debut_mono {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrder ι] (E : Set (ι × Ω)) (ω : Ω) : Monotone fun (x : ι) => debut E x ω

theorem MeasureTheory.debut_ne_top_iff_of_isBot {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrder ι] {E : Set (ι × Ω)} {n : ι} {ω : Ω} (hn : IsBot n) : debut E n ω ≠ ⊤ ↔ ω ∈ Prod.snd '' E

theorem MeasureTheory.setOf_debut_ne_top_eq_of_isBot {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrder ι] {E : Set (ι × Ω)} {n : ι} (hn : IsBot n) : {ω : Ω | debut E n ω ≠ ⊤} = Prod.snd '' E

theorem MeasureTheory.setOf_debut_lt_eq {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrder ι] (E : Set (ι × Ω)) (n t : ι) : {ω : Ω | debut E n ω < ↑t} = Prod.snd '' (E ∩ Set.Ico n t ×ˢ Set.univ)

theorem MeasureTheory.setOf_debut_ne_top_eq {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrder ι] (E : Set (ι × Ω)) (n : ι) : {ω : Ω | debut E n ω ≠ ⊤} = Prod.snd '' (E ∩ Set.Ici n ×ˢ Set.univ)

theorem MeasureTheory.debut_mem_of_isClosed {𝓧 : Type u_3} {ι : Type u_4} [TopologicalSpace ι] [ConditionallyCompleteLinearOrder ι] [OrderTopology ι] [FirstCountableTopology ι] {s : Set (ι × 𝓧)} {ω : 𝓧} {n : ι} (hs : IsClosed {t : ι | n ≤ t ∧ (t, ω) ∈ s}) (hω : debut s n ω ≠ ⊤) : ((debut s n ω).untopA, ω) ∈ s

def MeasureTheory.ProgMeasurableSet {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder ι] [MeasurableSpace ι] (E : Set (ι × Ω)) (𝓕 : Filtration ι mΩ) : Prop

A set E : Set ι × Ω is progressively measurable with respect to a filtration 𝓕 if the indicator function of E is a progressively measurable process with respect to 𝓕.

Equations

• MeasureTheory.ProgMeasurableSet E 𝓕 = MeasureTheory.IsStronglyProgressive 𝓕 (Function.curry (E.indicator fun (x : ι × Ω) => 1))

theorem MeasureTheory.ProgMeasurableSet.measurableSet_prod {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder ι] [MeasurableSpace ι] {E : Set (ι × Ω)} {𝓕 : Filtration ι mΩ} (hE : ProgMeasurableSet E 𝓕) (t : ι) : MeasurableSet {p : ↑(Set.Iic t) × Ω | (↑p.1, p.2) ∈ E}

theorem MeasureTheory.ProgMeasurableSet.measurableSet_inter_Iic {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder ι] [TopologicalSpace ι] [ClosedIicTopology ι] {mι : MeasurableSpace ι} [OpensMeasurableSpace ι] {E : Set (ι × Ω)} {𝓕 : Filtration ι mΩ} (hE : ProgMeasurableSet E 𝓕) (t : ι) : MeasurableSet (E ∩ Set.Iic t ×ˢ Set.univ)

theorem MeasureTheory.ProgMeasurableSet.measurableSet_inter_Iio {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [ConditionallyCompleteLinearOrder ι] [TopologicalSpace ι] [FirstCountableTopology ι] [OrderTopology ι] {mι : MeasurableSpace ι} [OpensMeasurableSpace ι] {E : Set (ι × Ω)} {𝓕 : Filtration ι mΩ} (hE : ProgMeasurableSet E 𝓕) (t : ι) : MeasurableSet (E ∩ Set.Iio t ×ˢ Set.univ)

theorem MeasureTheory.ProgMeasurableSet.measurableSet_inter_Ico {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [ConditionallyCompleteLinearOrder ι] [TopologicalSpace ι] [FirstCountableTopology ι] [OrderTopology ι] {mι : MeasurableSpace ι} [OpensMeasurableSpace ι] {E : Set (ι × Ω)} {𝓕 : Filtration ι mΩ} (hE : ProgMeasurableSet E 𝓕) (s t : ι) : MeasurableSet (E ∩ Set.Ico s t ×ˢ Set.univ)

theorem MeasureTheory.ProgMeasurableSet.measurableSet_inter_Icc {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [ConditionallyCompleteLinearOrder ι] [TopologicalSpace ι] [FirstCountableTopology ι] [OrderTopology ι] {mι : MeasurableSpace ι} [OpensMeasurableSpace ι] {E : Set (ι × Ω)} {𝓕 : Filtration ι mΩ} (hE : ProgMeasurableSet E 𝓕) (s t : ι) : MeasurableSet (E ∩ Set.Icc s t ×ˢ Set.univ)

theorem MeasureTheory.ProgMeasurableSet.measurableSet_preimage_prodMk {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [Preorder ι] [MeasurableSpace ι] {𝓕 : Filtration ι mΩ} {E : Set (ι × Ω)} (hE : ProgMeasurableSet E 𝓕) (t : ι) : MeasurableSet {ω : Ω | (t, ω) ∈ E}

theorem MeasureTheory.IsPavingAnalytic.nullMeasurableSet_debut_lt {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [MeasurableSpace ι] [BorelSpace ι] {P : Measure Ω} [SFinite P] {E : Set (ι × Ω)} (hE : IsPavingAnalytic {t : Set (ι × Ω) | MeasurableSet t} E) (n s : ι) : NullMeasurableSet {ω : Ω | debut E n ω < ↑s} P

For an analytic set E, the set {ω | debut E n ω < s} is null-measurable with respect to any s-finite measure.

theorem MeasurableSet.nullMeasurableSet_debut_lt {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [ConditionallyCompleteLinearOrder ι] [TopologicalSpace ι] [ClosedIciTopology ι] [MeasurableSpace ι] [PolishSpace ι] [BorelSpace ι] {P : MeasureTheory.Measure Ω} [MeasureTheory.SFinite P] {E : Set (ι × Ω)} (hE : MeasurableSet E) (n s : ι) : MeasureTheory.NullMeasurableSet {ω : Ω | MeasureTheory.debut E n ω < ↑s} P

theorem MeasurableSet.measurableSet_debut_lt {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [ConditionallyCompleteLinearOrder ι] [TopologicalSpace ι] [ClosedIciTopology ι] [MeasurableSpace ι] [PolishSpace ι] [BorelSpace ι] (P : MeasureTheory.Measure Ω) [MeasureTheory.SFinite P] [P.IsComplete] {E : Set (ι × Ω)} (hE : MeasurableSet E) (n s : ι) : MeasurableSet {ω : Ω | MeasureTheory.debut E n ω < ↑s}

theorem MeasureTheory.IsPavingAnalytic.nullMeasurable_debut {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {ι : Type u_3} [ConditionallyCompleteLinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] [MeasurableSpace ι] [BorelSpace ι] {P : Measure Ω} [SFinite P] {s : Set (ι × Ω)} (hs : IsPavingAnalytic {t : Set (ι × Ω) | MeasurableSet t} s) (u : ι) : NullMeasurable (debut s u) P

The debut of an analytic set is universally measurable: it is null-measurable with respect to any s-finite measure.

theorem MeasureTheory.ProgMeasurableSet.measurableSet_debut_lt {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [ConditionallyCompleteLinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [PolishSpace ι] [BorelSpace ι] (P : Measure Ω) [SFinite P] {𝓕 : Filtration ι mΩ} [𝓕.IsComplete P] {E : Set (ι × Ω)} (hE : ProgMeasurableSet E 𝓕) (n s : ι) : MeasurableSet {ω : Ω | debut E n ω < ↑s}

theorem MeasureTheory.debut_eq_iff_of_nhdsGT_eq_bot {Ω : Type u_1} {ι : Type u_2} [ConditionallyCompleteLinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] (E : Set (ι × Ω)) {n t : ι} (hnt : n ≤ t) (ht : nhdsWithin t (Set.Ioi t) = ⊥) (ω : Ω) (h_ge : ↑t ≤ debut E n ω) : debut E n ω = ↑t ↔ (t, ω) ∈ E

theorem MeasureTheory.isStoppingTime_debut {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [MeasurableSpace ι] [ConditionallyCompleteLinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [PolishSpace ι] [BorelSpace ι] (P : Measure Ω) [SFinite P] {𝓕 : Filtration ι mΩ} [𝓕.IsComplete P] [𝓕.IsRightContinuous] {E : Set (ι × Ω)} (hE : ProgMeasurableSet E 𝓕) (n : ι) : IsStoppingTime 𝓕 (debut E n)

Debut theorem: the debut of a progressively measurable set E is a stopping time, for a filtration that is right-continuous and complete with respect to an s-finite measure.

theorem MeasurableSet.progMeasurableSet_preimage {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [MeasurableSpace ι] [Preorder ι] {β : Type u_3} [TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] {𝓕 : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → β} (hX : MeasureTheory.IsStronglyProgressive 𝓕 X) {s : Set β} (hs : MeasurableSet s) : MeasureTheory.ProgMeasurableSet (Function.uncurry X ⁻¹' s) 𝓕

theorem MeasureTheory.IsStronglyProgressive.isStoppingTime_hittingAfter {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [MeasurableSpace ι] [ConditionallyCompleteLinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [PolishSpace ι] [BorelSpace ι] {β : Type u_3} [TopologicalSpace β] [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] (P : Measure Ω) [SFinite P] {𝓕 : Filtration ι mΩ} [𝓕.IsComplete P] [𝓕.IsRightContinuous] {X : ι → Ω → β} (hX : IsStronglyProgressive 𝓕 X) {s : Set β} (hs : MeasurableSet s) (n : ι) : IsStoppingTime 𝓕 (hittingAfter X s n)

The hitting time of a measurable set by a progressively measurable process for a filtration satisfying the usual conditions is a stopping time.

theorem MeasureTheory.IsStronglyProgressive.isStoppingTime_leastGE {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [MeasurableSpace ι] [ConditionallyCompleteLinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [PolishSpace ι] [BorelSpace ι] {β : Type u_3} [Preorder β] [TopologicalSpace β] [ClosedIciTopology β] [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] (P : Measure Ω) [SFinite P] {𝓕 : Filtration ι mΩ} [𝓕.IsComplete P] [𝓕.IsRightContinuous] {X : ι → Ω → β} (hX : IsStronglyProgressive 𝓕 X) (r : β) : IsStoppingTime 𝓕 (leastGE X r)

The first time that a progressively measurable process is greater than or equal to r is a stopping time, for a filtration satisfying the usual conditions.

theorem MeasureTheory.IsStronglyProgressive.isStoppingTime_leastGT {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [MeasurableSpace ι] [ConditionallyCompleteLinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [PolishSpace ι] [BorelSpace ι] {β : Type u_3} [LinearOrder β] [TopologicalSpace β] [ClosedIicTopology β] [MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] (P : Measure Ω) [SFinite P] {𝓕 : Filtration ι mΩ} [𝓕.IsComplete P] [𝓕.IsRightContinuous] {X : ι → Ω → β} (hX : IsStronglyProgressive 𝓕 X) (r : β) : IsStoppingTime 𝓕 (leastGT X r)

The first time that a progressively measurable process is greater than r is a stopping time, for a filtration satisfying the usual conditions.