English
If f is AEStronglyMeasurable, then the truncation is integrable.
Русский
Если f является AEStronglyMeasurable, то усечение интегрируемо.
LaTeX
$$Integrable (truncation f A) μ$$
Lean4
/-- If a function is integrable, then the integral of its truncated versions converges to the
integral of the whole function. -/
theorem tendsto_integral_truncation {f : α → ℝ} (hf : Integrable f μ) :
Tendsto (fun A => ∫ x, truncation f A x ∂μ) atTop (𝓝 (∫ x, f x ∂μ)) :=
by
refine tendsto_integral_filter_of_dominated_convergence (fun x => abs (f x)) ?_ ?_ ?_ ?_
· exact Eventually.of_forall fun A ↦ hf.aestronglyMeasurable.truncation
· filter_upwards with A
filter_upwards with x
rw [Real.norm_eq_abs]
exact abs_truncation_le_abs_self _ _ _
· exact hf.abs
· filter_upwards with x
apply tendsto_const_nhds.congr' _
filter_upwards [Ioi_mem_atTop (abs (f x))] with A hA
exact (truncation_eq_self hA).symm
