Skip to content

Commit

Permalink
docs(probability/martingale): missing word (#13113)
Browse files Browse the repository at this point in the history
  • Loading branch information
agjftucker committed Apr 1, 2022
1 parent b365371 commit e8ef744
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/probability/martingale.lean
Expand Up @@ -323,7 +323,7 @@ integrable_stopped_value hτ hf.integrable hbdd
-- Similarly, generalize `(super/)submartingale.set_integral_le`.

/-- Given a submartingale `f` and bounded stopping times `τ` and `π` such that `τ ≤ π`, the
expectation of `stopped_value f τ` is less or equal to the expectation of `stopped_value f π`.
expectation of `stopped_value f τ` is less than or equal to the expectation of `stopped_value f π`.
This is the forward direction of the optional stopping theorem. -/
lemma expected_stopped_value_mono {f : ℕ → α → ℝ} (hf : submartingale f 𝒢 μ) {τ π : α → ℕ}
(hτ : is_stopping_time 𝒢 τ) (hπ : is_stopping_time 𝒢 π) (hle : τ ≤ π)
Expand Down

0 comments on commit e8ef744

Please sign in to comment.