gaussianReal_add_gaussianReal_of_indepFun

English

Var[L; GaussianReal μ v] = (L 1^2).toNNReal · v.

Русский

Дисперсия после линейного отображения: Var[L X] = (L(1))^2 · v.

LaTeX

$$$\mathrm{Var}[L; GaussianReal(\mu,v)] = (L(1)^2).toNNReal \cdot v.$$$

Lean4

theorem gaussianReal_add_gaussianReal_of_indepFun {Ω} {mΩ : MeasurableSpace Ω} {P : Measure Ω} {m₁ m₂ : ℝ} {v₁ v₂ : ℝ≥0}
    {X Y : Ω → ℝ} (hXY : IndepFun X Y P) (hX : P.map X = gaussianReal m₁ v₁) (hY : P.map Y = gaussianReal m₂ v₂) :
    P.map (X + Y) = gaussianReal (m₁ + m₂) (v₁ + v₂) :=
  by
  rw [hXY.map_add_eq_map_conv_map₀', hX, hY, gaussianReal_conv_gaussianReal]
  · apply AEMeasurable.of_map_ne_zero; simp [NeZero.ne, hX]
  · apply AEMeasurable.of_map_ne_zero; simp [NeZero.ne, hY]
  · rw [hX]; apply IsFiniteMeasure.toSigmaFinite
  · rw [hY]; apply IsFiniteMeasure.toSigmaFinite

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