const_mul — Mathlib

English

If f and g are identically distributed, then dividing both by a constant preserves the identically distributed property.

Русский

Если f и g имеют одинаковое распределение, деление обеих на константу сохраняет это свойство.

LaTeX

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

Lean4

@[to_additive]
theorem const_mul [Mul γ] [MeasurableMul γ] (h : IdentDistrib f g μ ν) (c : γ) :
    IdentDistrib (fun x => c * f x) (fun x => c * g x) μ ν :=
  h.comp (measurable_const_mul c)

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