div_const — Mathlib

English

Multiplication by a constant on the left preserves identical distribution when f,g are identically distributed.

Русский

Умножение слева на константу сохраняет одинаковое распределение при равенстве f и g по распределению.

LaTeX

$$$\forall c,\ \text{IdentDistrib } f g\ \mu\ nu \Rightarrow \text{IdentDistrib}(x \mapsto c \cdot f(x)) (x \mapsto c \cdot g(x)) \mu \nu$$$

Lean4

@[to_additive]
theorem div_const [Div γ] [MeasurableDiv γ] (h : IdentDistrib f g μ ν) (c : γ) :
    IdentDistrib (fun x => f x / c) (fun x => g x / c) μ ν :=
  h.comp (MeasurableDiv.measurable_div_const c)

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