AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.StoppingTime

- Chewi Definition 1.1.11: at time `t`, the information in the filtration decides whether the extended nonnegative stopping time has occurred.

def IsChewiStoppingTime
    {Ω : Type*} {m : MeasurableSpace Ω}
    (filtration : Filtration ℝ≥0 m) (τ : Ω → WithTop ℝ≥0) : Prop :=
  MeasureTheory.IsStoppingTime filtration τ

/-- Constant nonnegative times satisfy the source stopping-time definition. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/StoppingTime.lean:27published source at 77184245109aOpen detailed card

- Constant nonnegative times satisfy the source stopping-time definition.

theorem isChewiStoppingTime_const
    {Ω : Type*} {m : MeasurableSpace Ω}
    (filtration : Filtration ℝ≥0 m) (t : ℝ≥0) :
    IsChewiStoppingTime filtration (fun _ : Ω => (t : WithTop ℝ≥0)) :=
  MeasureTheory.isStoppingTime_const filtration t

/-- The pointwise minimum of two Chewi stopping times is again a stopping
time. This is the stopping-time algebra needed for repeated stopping. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/StoppingTime.lean:33published source at 77184245109a

- The pointwise minimum of two Chewi stopping times is again a stopping time. This is the stopping-time algebra needed for repeated stopping.

theorem IsChewiStoppingTime.min
    {Ω : Type*} {m : MeasurableSpace Ω}
    {filtration : Filtration ℝ≥0 m} {τ σ : Ω → WithTop ℝ≥0}
    (hτ : IsChewiStoppingTime filtration τ)
    (hσ : IsChewiStoppingTime filtration σ) :
    IsChewiStoppingTime filtration (τ ⊓ σ) := by
  exact MeasureTheory.IsStoppingTime.min hτ hσ

/-- Truncating a stopping time by a deterministic nonnegative horizon preserves
the stopping-time property. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/StoppingTime.lean:41published source at 77184245109a

- Truncating a stopping time by a deterministic nonnegative horizon preserves the stopping-time property.

theorem IsChewiStoppingTime.min_const
    {Ω : Type*} {m : MeasurableSpace Ω}
    {filtration : Filtration ℝ≥0 m} {τ : Ω → WithTop ℝ≥0}
    (hτ : IsChewiStoppingTime filtration τ) (T : ℝ≥0) :
    IsChewiStoppingTime filtration
      (τ ⊓ fun _ => (T : WithTop ℝ≥0)) :=
  hτ.min (isChewiStoppingTime_const filtration T)

/-- Repeated stopping is exactly stopping at the pointwise infimum. This is a
pure process identity; no stopping-time or martingale hypotheses are needed. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/StoppingTime.lean:51published source at 77184245109a

- Repeated stopping is exactly stopping at the pointwise infimum. This is a pure process identity; no stopping-time or martingale hypotheses are needed.

theorem stoppedProcess_stoppedProcess_inf
    {Ω β : Type*} (u : ℝ≥0 → Ω → β)
    (τ σ : Ω → WithTop ℝ≥0) :
    stoppedProcess (stoppedProcess u τ) σ =
      stoppedProcess u (σ ⊓ τ) := by
  exact MeasureTheory.stoppedProcess_stoppedProcess

/-- If the second stopping time occurs no later than the first, stopping twice
reduces to the earlier stop. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/StoppingTime.lean:61published source at 77184245109a

- If the second stopping time occurs no later than the first, stopping twice reduces to the earlier stop.

theorem stoppedProcess_stoppedProcess_of_le
    {Ω β : Type*} (u : ℝ≥0 → Ω → β)
    {τ σ : Ω → WithTop ℝ≥0} (hστ : σ ≤ τ) :
    stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u σ := by
  exact MeasureTheory.stoppedProcess_stoppedProcess_of_le_right hστ

end StoppingTime
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/StoppingTime.lean:70published source at 77184245109a