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.hittingAfter_lt_iff' {Ω : Type u_3} {β : Type u_4} {ι : Type u_5} [ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β} {n : ι} {ω : Ω} {i : ι} : hittingAfter u s n ω < ↑i ↔ ∃ j ∈ Set.Ico n i, u j ω ∈ s

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 ω

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.ProgMeasurable 𝓕 (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.MeasurableSpace.prod_mono {Ω : Type u_1} {ι : Type u_2} {mι mι' : MeasurableSpace ι} {mΩ mΩ' : MeasurableSpace Ω} (h₁ : mι ≤ mι') (h₂ : mΩ ≤ mΩ') : mι.prod mΩ ≤ mι'.prod mΩ'

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 Ω} [ConditionallyCompleteLinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [PolishSpace ι] [BorelSpace ι] {P : Measure Ω} [IsFiniteMeasure P] {𝓕 : Filtration ι mΩ} (h𝓕 : 𝓕.HasUsualConditions P) {E : Set (ι × Ω)} (hE : ProgMeasurableSet E 𝓕) (t : ι) : MeasurableSet {ω : Ω | (t, ω) ∈ E}

theorem MeasureTheory.ProgMeasurableSet.measurableSet_debut_lt {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [ConditionallyCompleteLinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [MeasurableSpace ι] [PolishSpace ι] [BorelSpace ι] {P : Measure Ω} [IsFiniteMeasure P] {𝓕 : Filtration ι mΩ} (h𝓕 : 𝓕.HasUsualConditions 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 Ω} [IsFiniteMeasure P] {𝓕 : Filtration ι mΩ} (h𝓕 : 𝓕.HasUsualConditions P) {E : Set (ι × Ω)} (hE : ProgMeasurableSet E 𝓕) (n : ι) : IsStoppingTime 𝓕 (debut E n)

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

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.ProgMeasurable 𝓕 X) {s : Set β} (hs : MeasurableSet s) : MeasureTheory.ProgMeasurableSet (Function.uncurry X ⁻¹' s) 𝓕

theorem MeasureTheory.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 Ω} [IsFiniteMeasure P] {𝓕 : Filtration ι mΩ} (h𝓕 : 𝓕.HasUsualConditions P) {X : ι → Ω → β} (hX : ProgMeasurable 𝓕 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.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 Ω} [IsFiniteMeasure P] {𝓕 : Filtration ι mΩ} (h𝓕 : 𝓕.HasUsualConditions P) {X : ι → Ω → β} (hX : ProgMeasurable 𝓕 X) (r : β) : IsStoppingTime 𝓕 (leastGE X r)