sq — Mathlib · SciLib

English

If f and g are identically distributed, then f^2 and g^2 are identically distributed as well.

Русский

Если f и g имеют одинаковое распределение, то их квадраты тоже имеют одинаковое распределение.

LaTeX

$$sq {f g μ ν} : IdentDistrib f g μ ν → IdentDistrib (fun x => f x ^ 2) (fun x => g x ^ 2) μ ν$$

Lean4

protected theorem sq [Pow γ ℕ] [MeasurablePow γ ℕ] (h : IdentDistrib f g μ ν) :
    IdentDistrib (fun x => f x ^ 2) (fun x => g x ^ 2) μ ν :=
  h.comp (measurable_id.pow_const 2)

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