[Merged by Bors] - feat(measure_theory/lp_space): add snorm_norm_rpow

[RemyDegenne]

The lemma snorm_norm_rpow states snorm (λ x, ∥f x∥ ^ q) p μ = (snorm f (p * ennreal.of_real q) μ) ^ q.

Also add measurability lemmas about pow/rpow.

---

[sgouezel]

bors d+

[bors]

✌️ RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[RemyDegenne]

bors r+

[bors]

Build failed (retrying...):

• Build mathlib

[bryangingechen]

The build seems to be failing on this; try merging master and putting it back on the queue after fixing the build.
bors r-

[bors]

Canceled.

[RemyDegenne]

Ok, I'll try merging master later! Although it looks like every single ready-to-merge PR failed just now, so there might be something wrong elsewhere.

[bryangingechen]

Ok, I'll try merging master later! Although it looks like every single ready-to-merge PR failed just now, so there might be something wrong elsewhere.

Yes, this one was in the batch that failed too: I checked the "Build failed" link and that led me here (though it's entirely possible that there's another PR still on the queue with an issue).

[RemyDegenne]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests