cond — Mathlib

English

The conditional measure with respect to s and toMeasurable μ s are equal.

Русский

Условная мера по s равна условной мере по toMeasurable μ s.

LaTeX

$$$\\mu[|(to\\,Measurable\\,μ\\,s)] = \\mu[|s]$$$

Lean4

/-- The conditional probability measure of measure `μ` on set `s` is `μ` restricted to `s`
and scaled by the inverse of `μ s` (to make it a probability measure):
`(μ s)⁻¹ • μ.restrict s`. -/
def cond (s : Set Ω) : Measure Ω :=
  (μ s)⁻¹ • μ.restrict s

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