Theorem Definition:

        theorem MeasureTheory.submartingale_iff_expected_stoppedValue_mono {Ω : Type u_1} {m0 : MeasurableSpace Ω}  {μ : Measure Ω}  {𝒢 : Filtration ℕ m0}  {f : ℕ → Ω → ℝ} [IsFiniteMeasure μ]  (hadp : Adapted 𝒢 f)  (hint : ∀ (i : ℕ), Integrable (f i) μ) : Submartingale f 𝒢 μ ↔ ∀ (τ π : Ω → ℕ), IsStoppingTime 𝒢 τ → IsStoppingTime 𝒢 π → τ ≤ π → (∃ (N : ℕ), ∀ (x : Ω), π x ≤ N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ :=