[Merged by Bors] - feat: Lemmas about integrals of bounded continuous functions. #7222
Conversation
kkytola
added
WIP
|
|
||
| variable {X : Type*} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] | ||
|
|
||
| theorem NNReal.coe_ennreal_comp_measurable (f : X →ᵇ ℝ≥0) : |
There was a problem hiding this comment.
You are in the BoundedContinuousFunction namespace, and you would like this kind of lemma to be accessible by dot notation, so making it long by prefixing it with NNReal is probably not a good pick. I would just call it measurable_coe_ennreal_comp as there is no ambiguity here.
There was a problem hiding this comment.
Thank you!
I thought that a sub-namespace would be clearer for organization, but I realize that it actually breaks the dot notation.
I wonder, however, if it can become a problem to state many lemmas that are specific to the case of NNReal codomain in the BoundedContinuousFunction namespace. I believe there are good use cases for those specific lemmas in the topology of weak convergence and in the Riesz-Markov-Kakutani representation theorem. But I mildly worry about littering the namespace with such particular cases... I assume that the ..._of_... is the best existing naming convention for specifying the codomain. So for now, essentially in line with your other suggestions, I will add something like ...of_nnreal... to the names (and remove the attempted sub-namespace), except in cases which otherwise are unambiguous like this exact one.
|
✌️ kkytola can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
bors r+ |
This PR adds some lemmas about integrals of bounded continuous functions. The lemmas are collected in a separate file. Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
|
Build failed: |
bors r+ |
This PR adds some lemmas about integrals of bounded continuous functions. The lemmas are collected in a separate file. Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
bors
bot
deleted the
kkytola/integrals_of_bounded_continuous_functions
branch
This PR adds some lemmas about integrals of bounded continuous functions. The lemmas are collected in a separate file.
Existing lemmas about integrals of bounded continuous functions, especially from
MeasureTheory.Measure.FiniteMeasure, are moved to the new file specifically devoted to this purpose.The use case for the newly added lemmas is the proof of the last implication of portmanteau theorem.