English
For a measurable almost everywhere nonnegative real-valued function f, the Bochner integral equals the real part of the lintegral of ENNReal.ofReal(f).
Русский
Если f≥0 почти всюду и измеримо, то интеграл по Бо́хнеру = toReal(lintegral ENNReal.ofReal(f))
LaTeX
$$$0\\le f\\quad \\Rightarrow\\quad \\int f\,d\\mu = \\operatorname{toReal} \\left( \\int^- f\\,d\\mu \\right)$ для неотрицательного f.$$
Lean4
theorem tendsto_integral_norm_approxOn_sub {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E]
{f : α → E} (fmeas : Measurable f) (hf : Integrable f μ) [SeparableSpace (range f ∪ {0} : Set E)] :
Tendsto (fun n ↦ ∫ x, ‖SimpleFunc.approxOn f fmeas (range f ∪ {0}) 0 (by simp) n x - f x‖ ∂μ) atTop (𝓝 0) :=
by
convert (tendsto_toReal zero_ne_top).comp (tendsto_approxOn_range_L1_enorm fmeas hf) with n
rw [integral_norm_eq_lintegral_enorm]
· simp
· apply (SimpleFunc.aestronglyMeasurable _).sub
apply (stronglyMeasurable_iff_measurable_separable.2 ⟨fmeas, ?_⟩).aestronglyMeasurable
exact .mono (.of_subtype (range f ∪ {0})) subset_union_left
