variance_eq — Mathlib

English

Under identical distributions, the ordinary variances of f and g are equal.

Русский

При идентичном распределении обычные дисперсии функций f и g равны.

LaTeX

$$$\forall {f : \alpha \to \mathbb{R}} {g : \beta \to \mathbb{R}} (h : IdentDistrib f g μ ν) : variance f μ = variance g ν$$

Lean4

theorem variance_eq {f : α → ℝ} {g : β → ℝ} (h : IdentDistrib f g μ ν) : variance f μ = variance g ν := by
  rw [variance, h.evariance_eq]; rfl

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