[Merged by Bors] - feat(analysis/special_functions/pow): prove measurability of rpow for ennreal

[RemyDegenne]

Prove measurability of rpow for an ennreal argument.
Also shorten the proof in the real case.

---

[RemyDegenne]

I removed all the subtypes and use only ite.
That 60 lines proof turned into 10 + a short lemma. Thanks @fpvandoorn !

[fpvandoorn]

If you want, you can simplify the proof further like this: (but feel free to keep the old version if you think that is more readable)

Suggested change

	begin
	refine ennreal.measurable_of_measurable_nnreal_prod _ _,
	{ change measurable (λ (p : ℝ≥0 × ℝ), ↑(p.fst) ^ p.snd),
	simp_rw ennreal.coe_rpow_def,
	refine measurable.ite _ measurable_const nnreal.measurable_rpow.ennreal_coe,
	exact is_measurable.inter (measurable_fst (is_measurable_singleton 0))
	(measurable_snd is_measurable_Iio), },
	{ change measurable (λ (x : ℝ), (⊤ : ennreal) ^ x),
	simp_rw ennreal.top_rpow_def,
	refine measurable.ite is_measurable_Ioi measurable_const _,
	exact measurable.ite (is_measurable_singleton 0) measurable_const measurable_const, },
	end
	begin
	refine ennreal.measurable_of_measurable_nnreal_prod _ _,
	{ simp_rw ennreal.coe_rpow_def,
	refine measurable_const.ite _ nnreal.measurable_rpow.ennreal_coe,
	exact (measurable_fst (is_measurable_singleton 0)).inter (measurable_snd is_measurable_Iio), },
	{ simp_rw ennreal.top_rpow_def,
	refine measurable_const.ite is_measurable_Ioi _,
	exact measurable_const.ite (is_measurable_singleton 0) measurable_const, },
	end

[RemyDegenne]

I don't like the fact that this way to write measurable.ite does not respect the order of the arguments. But that lemma was so close to measurable.piecewise that I did not want to call it is_measurable.ite . Maybe I should?

[RemyDegenne]

But if I call it is_measurable.ite it suggests that the result is an is_measurable statement, so I won't change it. I will leave those measurable.ite _ _ _ as they are (I removed the change lines though).

[fpvandoorn]

I like the current name better than is_measurable.ite. It seems fine to not use the projection notation here.

[fpvandoorn]

LGTM

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

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