const_div — Mathlib

English

Dividing both sides by a constant preserves identical distribution when f,g are identically distributed.

Русский

Деление обеих величин на константу сохраняет одинаковое распределение.

LaTeX

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

Lean4

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

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