Documentation
Verification
.
UnitPowerSubstitution
Search
return to top
source
Imports
Init
Copula.Rank.ConditionalCDF
Mathlib.MeasureTheory.Integral.IntegralEqImproper
Imported by
Verification
.
integral_unit_rpow_substitution
← Mathematical handbook
source
theorem
Verification
.
integral_unit_rpow_substitution
{
θ
:
ℝ
}
(
hθ
:
0
<
θ
)
(
f
:
ℝ
→
ℝ
)
:
∫
(
u
:
↑
unitInterval
)
,
f
(
↑
u
^
θ
)
=
1
/
θ
*
∫
(
t
:
ℝ
)
in
0
..
1
,
t
^
(
1
/
θ
-
1
)
*
f
t