-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(probability/martingale): the discrete stochastic integral of a submartingale is a submartingale #14909
Conversation
…rover-community/mathlib into JasonKYi/disc_stoch_int
…rover-community/mathlib into JasonKYi/disc_stoch_int
…ommunity/mathlib into JasonKYi/disc_stoch_int
…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.
Could you please merge master? |
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.
Thanks!
bors d+
✌️ JasonKYi can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
Thanks for the reviews! |
…ubmartingale is a submartingale (#14909) This PR proves that the discrete stochastic integral of a predictable process with a submartingale is a submartingale. Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
Pull request successfully merged into master. Build succeeded: |
…rty of the conditional expectation (leanprover-community#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 leanprover-community#14909 and leanprover-community#14933.
…ubmartingale is a submartingale (leanprover-community#14909) This PR proves that the discrete stochastic integral of a predictable process with a submartingale is a submartingale. Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
…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.
…ubmartingale is a submartingale (#14909) This PR proves that the discrete stochastic integral of a predictable process with a submartingale is a submartingale. Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
…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.
…ubmartingale is a submartingale (#14909) This PR proves that the discrete stochastic integral of a predictable process with a submartingale is a submartingale. Co-authored-by: RemyDegenne <Remydegenne@gmail.com>
This PR proves that the discrete stochastic integral of a predictable process with a submartingale is a submartingale.