sub — Mathlib

English

If f and g are UnifIntegrable, then f + g is UnifIntegrable, given suitable p and measurability conditions.

Русский

Если f и g — UnifIntegrable, то f + g — тоже UnifIntegrable при некоторых условиях на p и измеримости.

LaTeX

$$$\\operatorname{UnifIntegrable} f p μ \\land \\operatorname{UnifIntegrable} g p μ \\land 1 \\le p \\Rightarrow \\operatorname{UnifIntegrable} (f+g) p μ$$$

Lean4

protected theorem sub (hf : UnifIntegrable f p μ) (hg : UnifIntegrable g p μ) (hp : 1 ≤ p)
    (hf_meas : ∀ i, AEStronglyMeasurable (f i) μ) (hg_meas : ∀ i, AEStronglyMeasurable (g i) μ) :
    UnifIntegrable (f - g) p μ := by
  rw [sub_eq_add_neg]
  exact hf.add hg.neg hp hf_meas fun i => (hg_meas i).neg

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