-
Notifications
You must be signed in to change notification settings - Fork 298
[Merged by Bors] - feat(probability/upcrossing): Doob's upcrossing estimate #14933
Conversation
…rover-community/mathlib into JasonKYi/disc_stoch_int
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…rty of the conditional expectation (#15274) We prove this result: ```lean lemma condexp_strongly_measurable_mul {f g : α → ℝ} (hf : strongly_measurable[m] f) (hfg : integrable (f * g) μ) (hg : integrable g μ) : μ[f * g | m] =ᵐ[μ] f * μ[g | m] := ``` This could be extended beyond multiplication, to any bounded bilinear map, but we leave this to a future PR. For now we only prove the real multiplication case, which is needed for #14909 and #14933.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This looks very good, thanks!
src/probability/upcrossing.lean
Outdated
|
||
namespace measure_theory | ||
|
||
variables {α ι : Type*} {m0 : measurable_space α} {μ : measure α} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is there a reason you call the space α
and not Ω
, and your measure μ
and not ℙ
(and the points in the space x
and not ω
)? I know it doesn't make any difference, but it can help your probability-inclined reader.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've changed α
to Ω
and x
to ω
. I've not switched μ
to ℙ
since this file had opened probability.notation
and it seems the notation for ℙ
being the volume doesn't allow me to declare it as a measure (I can't use measure_space
here since I want to specify the measurable_space
).
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
bors r+ |
This PR proves Doob's upcrossing estimate which is central for the martingale convergence theorems. Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
Pull request successfully merged into master. Build succeeded: |
This PR proves Doob's upcrossing estimate which is central for the martingale convergence theorems.
mul_indicator_finset_bUnion
#14919