Documentation
BrownianMotion
.
Gaussian
.
Moment
Search
return to top
source
Imports
Init
Mathlib.Analysis.SpecialFunctions.Sqrt
Mathlib.Probability.Distributions.Gaussian.Real
Imported by
ProbabilityTheory
.
centralMoment_two_mul_gaussianReal
ProbabilityTheory
.
centralMoment_fun_two_mul_gaussianReal
source
theorem
ProbabilityTheory
.
centralMoment_two_mul_gaussianReal
(
μ
:
ℝ
)
(
σ
:
NNReal
)
(
n
:
ℕ
)
:
centralMoment
id
(
2
*
n
)
(
gaussianReal
μ
(
σ
^
2
))
=
↑
σ
^
(
2
*
n
)
*
↑
(
2
*
n
-
1
).
doubleFactorial
source
theorem
ProbabilityTheory
.
centralMoment_fun_two_mul_gaussianReal
(
μ
:
ℝ
)
(
σ
:
NNReal
)
(
n
:
ℕ
)
:
centralMoment
(fun (
x
:
ℝ
) =>
x
)
(
2
*
n
)
(
gaussianReal
μ
(
σ
^
2
))
=
↑
σ
^
(
2
*
n
)
*
↑
(
2
*
n
-
1
).
doubleFactorial