English
Given a vector measure v on α and a function f : α → β, the pushforward vector measure v.map f is defined by (v.map f)(S) = v(f^{-1}(S)) for measurable S; if f is not measurable, the pushforward is the zero vector measure.
Русский
Для векторной меры v на α и отображения f : α → β отображение v.map f задаётся как векторная мера, для множества измеримогоS выполняется (v.map f)(S) = v(f^{-1}(S)); если f не измеримо, получаем нулевую векторную меру.
LaTeX
$$$$ (v.map f)(S) = v(f^{-1}(S)) \\quad\\text{при } S \\text{ измеримо}, \\quad \\text{и если } f \\text{ не измеримо, то } v.map f = 0. $$$$
Lean4
/-- The pushforward of a vector measure along a function. -/
def map (v : VectorMeasure α M) (f : α → β) : VectorMeasure β M :=
if hf : Measurable f then
{ measureOf' := fun s => if MeasurableSet s then v (f ⁻¹' s) else 0
empty' := by simp
not_measurable' := fun _ hi => if_neg hi
m_iUnion' := by
intro g hg₁ hg₂
convert v.m_iUnion (fun i => hf (hg₁ i)) fun i j hij => (hg₂ hij).preimage _
· rw [if_pos (hg₁ _)]
· rw [Set.preimage_iUnion, if_pos (MeasurableSet.iUnion hg₁)] }
else 0
