isGaussian_map_equiv

Mathlib.Probability.Distributions.Gaussian.Basic

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.isGaussian_map_equiv

English

For a > 0 and r > 0, gammaMeasure a r is a probability measure.

Русский

Для a > 0 и r > 0 гамма-мера gammaMeasure a r является вероятностной мерой.

LaTeX

$$$\text{IsProbabilityMeasure}(\gammaMeasure(a,r))$$$

Lean4

instance isGaussian_map_equiv (L : E ≃L[ℝ] F) : IsGaussian (μ.map L) :=
  isGaussian_map (L : E →L[ℝ] F)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru