chore(measure_theory/measure/haar_lebesgue): Golf #17782
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
YaelDillies
added
t-measure-probability
fpvandoorn
changed the title
eric-wieser
reviewed
Dec 1, 2022
jcommelin
reviewed
Dec 5, 2022
| have mesymm : measurable e.symm := e.symm.continuous.measurable, | ||
| rw [← map_map mesymm (mg.comp me), ← map_map mg me, ←g.coe_coe, | ||
| map_linear_map_add_haar_pi_eq_smul_add_haar hf (map e μ), measure.map_smul, map_map mesymm me, | ||
| e.symm_comp_self, measure.map_id], |
There was a problem hiding this comment.
This PR looks good to me. Can you please look at the build error below?
There was a problem hiding this comment.
I must be a bit over the limit because it doesn't time out in local.
Note that this PR isn't ready yet as I need to PR the preliminary material separately.
semorrison
added
the
too-late
|
Most interesting things have already made it to master. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Extract a bunch of API from the proof of
map_linear_map_add_haar_eq_smul_add_haarRequested by @sgouezel. I'm particularly interested in this proof because #2819 has a very similar one, and the API necessary to golf one is useful to the other.