Documentation
Verification
.
GammaSupport
Search
return to top
source
Imports
Init
Copula.Distribution.GammaLaplace
Mathlib.MeasureTheory.Measure.OpenPos
Imported by
Verification
.
volume_positive_absolutelyContinuous_gamma
Verification
.
gamma_ae_eq_constant_of_continuousOn
← Mathematical handbook
source
theorem
Verification
.
volume_positive_absolutelyContinuous_gamma
{
a
b
:
ℝ
}
(
ha
:
0
<
a
)
(
hb
:
0
<
b
)
:
(
MeasureTheory.volume
.
restrict
(
Set.Ioi
0
)
)
.
AbsolutelyContinuous
(
ProbabilityTheory.gammaMeasure
a
b
)
source
theorem
Verification
.
gamma_ae_eq_constant_of_continuousOn
{
a
b
:
ℝ
}
(
ha
:
0
<
a
)
(
hb
:
0
<
b
)
{
f
:
ℝ
→
ℝ
}
{
c
:
ℝ
}
(
hf
:
ContinuousOn
f
(
Set.Ioi
0
)
)
(
he
:
f
=ᵐ[
ProbabilityTheory.gammaMeasure
a
b
]
fun (
x
:
ℝ
) =>
c
)
(
x
:
ℝ
)
:
x
∈
Set.Ioi
0
→
f
x
=
c