mul_const — Mathlib

English

If f and g are identically distributed, then multiplying 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) \cdot c) (x \mapsto g(x) \cdot c) \mu \nu$$$

Lean4

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

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