-
Notifications
You must be signed in to change notification settings - Fork 299
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/stopping): generalize mem_ℒp_stopped_value
#16369
Conversation
(integrable.integrable_on (@integrable_stopped_value Ω ℕ _ _ _ _ _ _ _ _ _ | ||
(hitting_is_stopping_time hsub.adapted measurable_set_Ici) hsub.integrable _ hitting_le)), |
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 need to add the @
because somehow none of the arguments can precisely indicate what the index type is and Lean guesses incorrectly Ω → ℕ
instead of ℕ
.
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.
bors d+
Thanks!
@@ -575,28 +575,28 @@ begin | |||
have h := set_integral_ge_of_const_le (measurable_set_le measurable_const | |||
(finset.measurable_range_sup'' (λ n _, (hsub.strongly_measurable n).measurable.le (𝒢.le n)))) | |||
(measure_ne_top _ _) this | |||
(integrable.integrable_on (integrable_stopped_value (hitting_is_stopping_time | |||
hsub.adapted measurable_set_Ici) hsub.integrable hitting_le)), | |||
(integrable.integrable_on (@integrable_stopped_value Ω ℕ _ _ _ _ _ _ _ _ _ |
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.
could you make the ℕ
argument of integrable_stopped_value
explicit, since it seems Lean has difficulties inferring it, to avoid using the @
version here and below?
✌️ RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
Also rename many lemmas which had names `*_of_encodable` but took `countable` arguments since a recent PR which replaced all `encodable` by `countable` but did not touch the names. Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
Build failed: |
bors r- |
bors r+ |
Also rename many lemmas which had names `*_of_encodable` but took `countable` arguments since a recent PR which replaced all `encodable` by `countable` but did not touch the names. Co-authored-by: Rémy Degenne <remydegenne@gmail.com> Co-authored-by: RemyDegenne <remydegenne@gmail.com>
Pull request successfully merged into master. Build succeeded: |
mem_ℒp_stopped_value
mem_ℒp_stopped_value
Also rename many lemmas which had names `*_of_encodable` but took `countable` arguments since a recent PR which replaced all `encodable` by `countable` but did not touch the names. Co-authored-by: Rémy Degenne <remydegenne@gmail.com> Co-authored-by: RemyDegenne <remydegenne@gmail.com>
Also rename many lemmas which had names `*_of_encodable` but took `countable` arguments since a recent PR which replaced all `encodable` by `countable` but did not touch the names. Co-authored-by: Rémy Degenne <remydegenne@gmail.com> Co-authored-by: RemyDegenne <remydegenne@gmail.com>
Also rename many lemmas which had names
*_of_encodable
but tookcountable
arguments since a recent PR which replaced allencodable
bycountable
but did not touch the names.