English
For the density measure on (0, ∞), the volume of the interval (0, x) is given by a real-valued expression involving x^ (n+1)/(n+1).
Русский
Для плотностной меры на (0,∞) объём интервала (0, x) задаётся выражением x^{n+1}/(n+1).
LaTeX
$$$\\mathrm{volumeIoiPow}\\,(n)\\,(\\mathrm Iio(x)) = \\mathrm{ENNReal.ofReal}( x^{n+1}/(n+1) )$$$
Lean4
theorem volumeIoiPow_apply_Iio (n : ℕ) (x : Ioi (0 : ℝ)) :
volumeIoiPow n (Iio x) = ENNReal.ofReal (x.1 ^ (n + 1) / (n + 1)) :=
by
have hr₀ : 0 ≤ x.1 := le_of_lt x.2
rw [volumeIoiPow, withDensity_apply _ measurableSet_Iio,
setLIntegral_subtype measurableSet_Ioi _ fun a : ℝ ↦ .ofReal (a ^ n), image_subtype_val_Ioi_Iio,
restrict_congr_set Ioo_ae_eq_Ioc, ← ofReal_integral_eq_lintegral_ofReal (intervalIntegrable_pow _).1, ←
integral_of_le hr₀]
· simp
· filter_upwards [ae_restrict_mem measurableSet_Ioc] with y hy
exact pow_nonneg hy.1.le _
