From 8d40e8d026894b969684c8e93de9577d5d97942b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Fri, 20 Nov 2020 07:52:25 +0000 Subject: [PATCH] feat(analysis/special_functions/pow): add ennreal.to_nnreal_rpow (#5042) cut ennreal.to_real_rpow into two lemmas: to_nnreal_rpow and to_real_rpow --- src/analysis/special_functions/pow.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/analysis/special_functions/pow.lean b/src/analysis/special_functions/pow.lean index 31a245a36db59..0ebfdc9d99745 100644 --- a/src/analysis/special_functions/pow.lean +++ b/src/analysis/special_functions/pow.lean @@ -1422,8 +1422,7 @@ begin nnreal.one_le_rpow_of_pos_of_le_one_of_nonpos hx1 hx2 (le_of_lt hz)], end -lemma to_real_rpow (x : ennreal) (z : ℝ) : - (x.to_real) ^ z = (x ^ z).to_real := +lemma to_nnreal_rpow (x : ennreal) (z : ℝ) : (x.to_nnreal) ^ z = (x ^ z).to_nnreal := begin rcases lt_trichotomy z 0 with H|H|H, { cases x, { simp [H, ne_of_lt] }, @@ -1435,6 +1434,9 @@ begin simp [coe_rpow_of_nonneg _ (le_of_lt H)] } end +lemma to_real_rpow (x : ennreal) (z : ℝ) : (x.to_real) ^ z = (x ^ z).to_real := +by rw [ennreal.to_real, ennreal.to_real, ←nnreal.coe_rpow, ennreal.to_nnreal_rpow] + end ennreal section measurability_ennreal