measureRestrict — Mathlib

English

Restriction of a conservative system to an invariant set is conservative with respect to the restricted measure.

Русский

Ограничение консервативной системы до инвариантного множества сохраняет консервативность относительно ограниченной меры.

LaTeX

$$$\mathrm{Conservative}(f,\mu) \wedge \mathrm{MapsTo}(f,s,s) \Rightarrow \mathrm{Conservative}(f,\mu\restriction s).$$$

Lean4

/-- Restriction of a conservative system to an invariant set is a conservative system,
formulated in terms of the restriction of the measure. -/
theorem measureRestrict (h : Conservative f μ) (hs : MapsTo f s s) : Conservative f (μ.restrict s) :=
  .of_absolutelyContinuous h (absolutelyContinuous_of_le restrict_le_self) <| h.toQuasiMeasurePreserving.restrict hs

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