English
Restricting a measure μ to a set s defines a linear operator over the semiring ℝ≥0∞ that sends μ to the restricted measure μ|s; this operator is implemented via the outer measure restriction.
Русский
Ограничение меры μ на множество s задаёт линейный оператор над полусложной полугруппой ℝ≥0∞, переводящий μ в ограниченную меру μ|s; оператор реализован через ограничение внешней меры.
LaTeX
$$$\text{restrict}_{\ell}(s):\mathsf{M} \to \mathsf{M},\quad (\text{restrict}_{\ell}(s))(\mu) = \mu\restriction s.$$$
Lean4
/-- Restrict a measure `μ` to a set `s` as an `ℝ≥0∞`-linear map. -/
noncomputable def restrictₗ {m0 : MeasurableSpace α} (s : Set α) : Measure α →ₗ[ℝ≥0∞] Measure α :=
liftLinear (OuterMeasure.restrict s) fun μ s' hs' t =>
by
suffices μ (s ∩ t) = μ (s ∩ t ∩ s') + μ ((s ∩ t) \ s') by
simpa [← Set.inter_assoc, Set.inter_comm _ s, ← inter_diff_assoc]
exact le_toOuterMeasure_caratheodory _ _ hs' _
