evariance_eq — Mathlib

English

If f and g are identically distributed, then their e-variances with respect to μ and ν are equal.

Русский

Если f и g имеют одинаковое распределение, то их e-variance относительно μ и ν равны.

LaTeX

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

Lean4

theorem evariance_eq {f : α → ℝ} {g : β → ℝ} (h : IdentDistrib f g μ ν) : evariance f μ = evariance g ν :=
  by
  convert (h.sub_const (∫ x, f x ∂μ)).nnnorm.coe_nnreal_ennreal.sq.lintegral_eq
  rw [h.integral_eq]
  rfl

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