[Merged by Bors] - feat(probability_theory/notation): add notations for expected value, conditional expectation #9469
Conversation
src/probability_theory/notation.lean
Outdated
| variables {α E : Type*} [measure_space α] {ℙ ℙ' : measure α} [measurable_space E] [normed_group E] | ||
| [normed_space ℝ E] [borel_space E] [second_countable_topology E] [complete_space E] {X Y : α → E} | ||
|
|
||
| example : ℙ[X] = ∫ a, X a ∂ℙ := rfl |
There was a problem hiding this comment.
I don't really like this one. I'd prefer ℙ to be a notation for volume, and then ℙ s would be the probability of the set s. Or maybe rather for the real-valued version of the measure (do we already have an API around this for finite measures?)
There was a problem hiding this comment.
You're right that ℙ s should be the probability of a set, either as notation for volume s or as a consequence of your proposal of ℙ being a notation for the volume. In any case, I should not use ℙ as a name for a measure.
But it does not rule out µ[X] where µ is the measure, and not part of the notation. I think those two notations could go well together.
If ℙ is a notation for volume as you suggest, then with the µ[X] notation for expected value, ℙ[X] would be a way to write the expected value of X. Or we can still define the 𝔼[X] notation on top of that if we prefer.
I really want a nice way to write an expectation with respect to a non-volume measure, since almost every paper I write uses a change of probability measure somewhere (I realize that this contradicts the first sentence of the PR description, in which I say that the measure is often implicit).
The notations I see most often in real math to make the measure explicit are 𝔼_P[X] or 𝔼_{X∼P}[X] (with subscripts), which is not something we can do. The P[X] notation is also something I've seen used by some people to denote the expected value under P, and that one is mathlib-compatible.
There was a problem hiding this comment.
I am perfectly ok with µ[X], although maybe 𝔼[X; µ] would also work. I'll let you choose whichever you prefer.
There was a problem hiding this comment.
Regarding the real vs ennreal issue for ℙ s, I think it could be nice to have it real because working with ennreal is not fun.
But that means that ℙ cannot be a notation for the volume. ℙ s has to be notation for the real-valued finite measure applied to s, or ℙ has to be notation for the real-valued measure, but it then cannot be used to write ℙ[X] for example.
I will leave that out for now and look at what we have about that real-valued version of a finite measure.
There was a problem hiding this comment.
I agree that often ennreal values for probabilities are not fun. Currently measure_theory.finite_measure.has_coe_to_fun and measure_theory.probability_measure.has_coe_to_fun yield the underlying measures of sets composed with ennreal.to_nnreal, but there is no API and this is therefore largely untested for now.
One possibility would be to try something similar to dist vs nndist. For example one could have a typeclass has_nnmeasure, instantiated either under the assumption [is_finite_measure µ] or for the types finite_measure and probability_measure. Notation should be chosen anyway. And it would require some API, but nndist has worked well for me recently.
I am not suggesting anything for this PR, just commenting on the status of "real-valued version of a finite measure".
RemyDegenne
added
the
needs-documentation
RemyDegenne
added
awaiting-review
|
Let's merge this for now. As for the binding power, I have no clue either, so we will see if there are friction points when using the notations, and solve them if/when needed. |
github-actions
bot
added
ready-to-merge
…conditional expectation (#9469) When working in probability theory, the measure on the space is most often implicit. With our current notations for measure spaces, that means writing `volume` in a lot of places. To avoid that and introduce notations closer to the usual practice, this PR defines - `𝔼[X]` for the expected value (integral) of a function `X` over the volume measure, - `P[X]` for the expected value over the measure `P`, - `𝔼[X | hm]` for the conditional expectation with respect to the volume, - `X =ₐₛ Y` for `X =ᵐ[volume] Y` and similarly for `X ≤ᵐ[volume] Y`, - `∂P/∂Q` for `P.rn_deriv Q` All notations are localized to the `probability_theory` namespace.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
When working in probability theory, the measure on the space is most often implicit. With our current notations for measure spaces, that means writing
volumein a lot of places. To avoid that and introduce notations closer to the usual practice, this PR defines𝔼[X]for the expected value (integral) of a functionXover the volume measure,P[X]for the expected value over the measureP,𝔼[X | hm]for the conditional expectation with respect to the volume,X =ₐₛ YforX =ᵐ[volume] Yand similarly forX ≤ᵐ[volume] Y,∂P/∂QforP.rn_deriv QAll notations are localized to the
probability_theorynamespace.I'd like to hear opinions about the notations and since I have no idea of how to set binding powers, I'd like some comments on that as well.