MeasureTheory.value_lintegral_res₀

lemma value_lintegral_res₀ {j : Bool} {β : ℝ≥0∞} {γ : ℝ} (hγ : if j then γ > -1 else γ < -1) :  ∫⁻ s : ℝ in res j β, ENNReal.ofReal (s ^ γ) = β ^ (γ + 1) / ENNReal.ofReal |γ + 1| := by  · unfold res    split at hγ <;> rename_i xor_split    · rw [xor_split]      simp only [↓reduceIte]      split_ifs with htop      · rw [htop, top_rpow_def]        split_ifs        · simp [lintegral_rpow_Ioi_top, top_div_of_lt_top]        · linarith        · linarith      · by_cases hzero : β = 0        · rw [hzero, ENNReal.zero_rpow_of_pos (by linarith)]; simp        · have htcinv : 0 < β.toReal := toReal_pos hzero htop          rw [lintegral_rpow_of_gt_abs htcinv.le hγ, ENNReal.ofReal_div_of_pos              (by rw [abs_pos]; linarith), ← ENNReal.ofReal_rpow_of_pos htcinv,              ofReal_toReal_eq_iff.mpr htop]    · simp only [eq_false_of_ne_true xor_split, Bool.false_eq_true, ↓reduceIte]      split_ifs with htop      · rw [htop, top_rpow_of_neg (by linarith)]; simp      · by_cases hzero : β = 0        · rw [hzero, toReal_zero, lintegral_rpow_Ioi_top, zero_rpow_of_neg (by linarith),              top_div_of_lt_top]          exact coe_lt_top        · have htcinv : 0 < β.toReal := toReal_pos hzero htop          rw [lintegral_Ioi_rpow_of_lt_abs htcinv hγ, ofReal_div_of_pos              (by rw [abs_pos]; linarith), ← ofReal_rpow_of_pos htcinv,              ofReal_toReal_eq_iff.mpr htop]