English
Restriction to a set i yields a vector measure on α that measures s by v(s ∩ i) when s is measurable.
Русский
Ограничение до множества i даёт векторную меру, которая измеряет s как v(s ∩ i) при измеримости s.
LaTeX
$$$$ \\bigl(\\mathrm{restrict}\\ v\\ i\\bigr)(s) = v(s \\cap i) \\quad \\text{для } \\mathrm{MeasurableSet}(s). $$$$
Lean4
/-- The restriction of a vector measure on some set. -/
def restrict (v : VectorMeasure α M) (i : Set α) : VectorMeasure α M :=
if hi : MeasurableSet i then
{ measureOf' := fun s => if MeasurableSet s then v (s ∩ i) else 0
empty' := by simp
not_measurable' := fun _ hi => if_neg hi
m_iUnion' := by
intro f hf₁ hf₂
convert v.m_iUnion (fun n => (hf₁ n).inter hi) (hf₂.mono fun i j => Disjoint.mono inf_le_left inf_le_left)
· rw [if_pos (hf₁ _)]
· rw [Set.iUnion_inter, if_pos (MeasurableSet.iUnion hf₁)] }
else 0
