IicSnd — Mathlib

English

Definition of IicSnd: a marginal of ρ restricted to univ × Iic r, projected on α.

Русский

Определение IicSnd: маргинальная мера ρ, ограниченная на univ × Iic r, проецируемая на α.

LaTeX

$$$\mathrm{IicSnd}_{\rho}(r) = (\rho\restriction (\mathrm{univ} \times \mathrm{Iic}(r))).\mathrm{fst}$$$

Lean4

/-- Measure on `α` such that for a measurable set `s`, `ρ.IicSnd r s = ρ (s ×ˢ Iic r)`. -/
noncomputable def IicSnd (r : ℝ) : Measure α :=
  (ρ.restrict (univ ×ˢ Iic r)).fst

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