English
If a uniformly integrable family f has components f_n that are almost everywhere equal to g_n, then g is uniformly integrable with the same p and μ.
Русский
Если семейство f с униформной интегрируемостью имеет компоненты f_n, которые равны почти в мере g_n, то g тоже униформно интегрируем по тем же p и μ.
LaTeX
$$$\\operatorname{UnifI} f p μ \\land (\\forall n, f_n =_{μ} g_n) \\Rightarrow \\operatorname{UnifI} g p μ$$$
Lean4
/-- Uniform integrability in the measure theory sense.
A sequence of functions `f` is said to be uniformly integrable if for all `ε > 0`, there exists
some `δ > 0` such that for all sets `s` with measure less than `δ`, the Lp-norm of `f i`
restricted on `s` is less than `ε`.
Uniform integrability is also known as uniformly absolutely continuous integrals. -/
def UnifIntegrable {_ : MeasurableSpace α} (f : ι → α → β) (p : ℝ≥0∞) (μ : Measure α) : Prop :=
∀ ⦃ε : ℝ⦄ (_ : 0 < ε),
∃ (δ : ℝ) (_ : 0 < δ),
∀ i s, MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
