isGaussian_map — Mathlib

English

There is a measure gammaMeasure(a, r) on ℝ defined by volume.withDensity (gammaPDF a r).

Русский

Существует мера gammaMeasure(a, r) на ℝ, определяемая volume.withDensity (gammaPDF a r).

LaTeX

$$$\gammaMeasure(a,r) = \mathrm{volume}.withDensity(\gammaPDF(a,r))$$$

Lean4

/-- The map of a Gaussian measure by a continuous linear map is Gaussian. -/
instance isGaussian_map (L : E →L[ℝ] F) : IsGaussian (μ.map L) where
  map_eq_gaussianReal
    L' := by
    rw [Measure.map_map (by fun_prop) (by fun_prop)]
    change Measure.map (L'.comp L) μ = _
    rw [IsGaussian.map_eq_gaussianReal (L'.comp L)]
    congr
    · rw [integral_map (by fun_prop) (by fun_prop)]
      simp
    · rw [← variance_id_map (by fun_prop)]
      conv_rhs => rw [← variance_id_map (by fun_prop)]
      rw [Measure.map_map (by fun_prop) (by fun_prop)]
      simp

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