English
Let f be a μ-a.e. measurable function from α to an ordered space γ with 0. The positive-part construction applied to the associated a.e. equivalence function equals the a.e. equivalence class of the function x ↦ max(f(x), 0), with the induced measurability from the composition of the identity and the constant map.
Русский
Пусть f:α→γ является почти surely измеримой функцией, где γ упорядочено с нулём. Тогда положительная часть соответствующего а.э. эквивалентного отображения равна отображению x↦max(f(x),0) с учётом соответствующей измеримости.
LaTeX
$$$\text{posPart}\; (mk\; f\; hf : α \to_{μ} γ) = mk \ (\lambda x. \max(f(x), 0))\ ( (\text{continuous_id} \;\vee\; \text{continuous_const}).comp_aestronglyMeasurable\ hf )$$$
Lean4
@[simp]
theorem posPart_mk (f : α → γ) (hf) :
posPart (mk f hf : α →ₘ[μ] γ) =
mk (fun x => max (f x) 0) ((continuous_id.max continuous_const).comp_aestronglyMeasurable hf) :=
rfl
