English
Let f and g be measurable functions with identical distributions under μ and ν, respectively. Then for every natural number n, the random variables f^n and g^n have identical distributions under μ and ν.
Русский
Пусть f и g — измеримые функции, имеющие одинаковые распределения при μ и ν. Тогда для каждого натурального числа n случайные величины f^n и g^n имеют одинаковое распределение относительно μ и ν.
LaTeX
$$$\forall {\alpha, \beta, \gamma} [MeasurableSpace(\alpha)] [MeasurableSpace(\beta)] [MeasurableSpace(\gamma)] {\mu : Measure(\alpha)} {\nu : Measure(\beta)} {f : \alpha \to \gamma} {g : \beta \to \gamma} \big[Pow γ \mathbb{N}\] [MeasurablePow γ \mathbb{N}] \, (IdentDistrib f g μ ν) \Rightarrow \forall {n : \mathbb{N}}, IdentDistrib (fun x => f x ^ n) (fun x => g x ^ n) μ ν$$
Lean4
protected theorem pow [Pow γ ℕ] [MeasurablePow γ ℕ] (h : IdentDistrib f g μ ν) {n : ℕ} :
IdentDistrib (fun x => f x ^ n) (fun x => g x ^ n) μ ν :=
h.comp (measurable_id.pow_const n)
