[GOAL]
⊢ MeasurablePow ℝ≥0∞ ℝ
[PROOFSTEP]
refine' ⟨ENNReal.measurable_of_measurable_nnreal_prod _ _⟩
[GOAL]
case refine'_1
⊢ Measurable fun p => (↑p.fst, p.snd).fst ^ (↑p.fst, p.snd).snd
[PROOFSTEP]
simp_rw [ENNReal.coe_rpow_def]
[GOAL]
case refine'_1
⊢ Measurable fun p => if p.fst = 0 ∧ p.snd < 0 then ⊤ else ↑(p.fst ^ p.snd)
[PROOFSTEP]
refine' Measurable.ite _ measurable_const (measurable_fst.pow measurable_snd).coe_nnreal_ennreal
[GOAL]
case refine'_1
⊢ MeasurableSet {a | a.fst = 0 ∧ a.snd < 0}
[PROOFSTEP]
exact MeasurableSet.inter (measurable_fst (measurableSet_singleton 0)) (measurable_snd measurableSet_Iio)
[GOAL]
case refine'_2
⊢ Measurable fun x => (⊤, x).fst ^ (⊤, x).snd
[PROOFSTEP]
simp_rw [ENNReal.top_rpow_def]
[GOAL]
case refine'_2
⊢ Measurable fun x => if 0 < x then ⊤ else if x = 0 then 1 else 0
[PROOFSTEP]
refine' Measurable.ite measurableSet_Ioi measurable_const _
[GOAL]
case refine'_2
⊢ Measurable fun x => if x = 0 then 1 else 0
[PROOFSTEP]
exact Measurable.ite (measurableSet_singleton 0) measurable_const measurable_const
