uniformIntegrable_zero_meas — Mathlib

English

If μ is the zero measure, every function family f is uniformly integrable; the uniform integrability condition is trivial in this case.

Русский

Если мера μ равна нулю, любая семейство функций является uniformly integrable.

LaTeX

$$$[MeasureTheory]\ uniformIntegrable\ f p (0:Measure α)$$$

Lean4

theorem uniformIntegrable_zero_meas [MeasurableSpace α] : UniformIntegrable f p (0 : Measure α) :=
  ⟨fun _ => aestronglyMeasurable_zero_measure _, unifIntegrable_zero_meas, 0, fun _ => eLpNorm_measure_zero.le⟩

Похожие утверждения