hasLaw_fun_mul — Mathlib

English

For a measurable t, the measure equals the average number of occurrences of elements of s in t.

Русский

Для измеримого t мера равна среднему числу вхождений элементов s в t.

LaTeX

$$$$ (\\mathrm{toMeasure\\_ofMultiset\\, apply}\\; s\\; hs).toMeasure\\; t = \\frac{\\sum' x, (s.filter(\\cdot \\in t)).count x}{\\mathrm{Multiset}.card s} $$$$

Lean4

@[to_additive]
theorem hasLaw_fun_mul {M : Type*} [Monoid M] {mM : MeasurableSpace M} [MeasurableMul₂ M] {μ ν : Measure M}
    [SigmaFinite μ] [SigmaFinite ν] {X Y : Ω → M} (hX : HasLaw X μ P) (hY : HasLaw Y ν P) (hXY : IndepFun X Y P) :
    HasLaw (fun ω ↦ X ω * Y ω) (μ ∗ₘ ν) P :=
  hXY.hasLaw_mul hX hY

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