Commit 2026-01-25 22:12 6eedf698

feat(Probability): Generalize some theorems by replacing StronglyAdapted with Adapted (#34381) I changed the name from hittingBtwn_isStoppingTime to Adapted.isStoppingTime_hittingBtwn. This allows us to take advantage of the dot notation, so that for example, we can prove the following theorem in one line:

theorem StronglyAdapted.isStoppingTime_hittingBtwn [ConditionallyCompleteLinearOrder ι]
    [WellFoundedLT ι] [Countable ι] [TopologicalSpace β] [PseudoMetrizableSpace β]
    [MeasurableSpace β] [BorelSpace β]
    {f : Filtration ι m} {u : ι → Ω → β} {s : Set β} {n n' : ι} (hu : StronglyAdapted f u)
    (hs : MeasurableSet s) : IsStoppingTime f (fun ω ↦ (hittingBtwn u s n n' ω : ι)) :=
  hu.adapted.isStoppingTime_hittingBtwn hs

I also golfed some proofs.