This file contains the basic definitions and properties of the debut of a set.

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.

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

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

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 m.

@[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 ≠ ∅ 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 ≠ ∅)] : debut (I ×ˢ Set.univ) n = fun (x : Ω) => if Set.Ici n ∩ I ≠ ∅ 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.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 : ι} {ω : Ω} [WellFoundedLT ι] : 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 ω

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

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

Equations

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

theorem MeasureTheory.isStoppingTime_debut {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [MeasurableSpace ι] [Preorder ι] [InfSet ι] {E : Set (ι × Ω)} {f : Filtration ι mΩ} (hE : ProgMeasurableSet E f) (n : ι) : IsStoppingTime f (debut E n)

Debut Theorem: The debut of a progressively measurable set E is a stopping time.

theorem MeasureTheory.isStoppingTime_hittingAfter' {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [ConditionallyCompleteLinearOrder ι] [MeasurableSpace ι] {β : Type u_3} [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β] {f : Filtration ι mΩ} {X : ι → Ω → β} (hX : ProgMeasurable f X) {s : Set β} {n m : ι} (hs : MeasurableSet s) : IsStoppingTime f (hittingAfter X s n)