English
Restriction of a vector measure to a smaller σ-algebra preserves measurability on measurable sets after trimming.
Русский
Ограничение векторной меры к меньшему σ-алгебре сохраняет измеримость на измеримых множествах после тримирования.
LaTeX
$$$ (vtrim\\ hle) i = v i \\quad \\text{for } i \\text{ measurable in } m$$$
Lean4
/-- Restriction of a vector measure onto a sub-σ-algebra. -/
@[simps]
def trim {m n : MeasurableSpace α} (v : VectorMeasure α M) (hle : m ≤ n) : @VectorMeasure α m M _ _ :=
@VectorMeasure.mk α m M _ _ (fun i => if MeasurableSet[m] i then v i else 0)
(by dsimp only; rw [if_pos (@MeasurableSet.empty _ m), v.empty]) (fun i hi => by dsimp only; rw [if_neg hi])
(fun f hf₁ hf₂ => by
dsimp only
have hf₁' : ∀ k, MeasurableSet[n] (f k) := fun k => hle _ (hf₁ k)
convert v.m_iUnion hf₁' hf₂ using 1
· ext n
rw [if_pos (hf₁ n)]
· rw [if_pos (@MeasurableSet.iUnion _ _ m _ _ hf₁)])
