exists_measurable_nonneg — Mathlib

English

If f is AEMeasurable and f(x) ≥ 0 a.e., there exists a measurable g with 0 ≤ g and f =ᵐ g.

Русский

Если f — AЕ-измеримая и f(x) ≥ 0 почти везде, существует измеримая g такая, что 0 ≤ g и f =ᵐ g.

LaTeX

$$$\mathrm{AEMeasurable}(f, \mu) \rightarrow (\forall^\text{ae} x, 0 \le f x) \rightarrow \exists g, \mathrm{Measurable}(g) \land 0 \le g \land f =^\text{ae}_\mu g$$$

Lean4

theorem exists_measurable_nonneg {β} [Preorder β] [Zero β] {mβ : MeasurableSpace β} {f : α → β} (hf : AEMeasurable f μ)
    (f_nn : ∀ᵐ t ∂μ, 0 ≤ f t) : ∃ g, Measurable g ∧ 0 ≤ g ∧ f =ᵐ[μ] g :=
  by
  obtain ⟨G, hG_meas, hG_mem, hG_ae_eq⟩ := hf.exists_ae_eq_range_subset f_nn ⟨0, le_rfl⟩
  exact ⟨G, hG_meas, fun x => hG_mem (mem_range_self x), hG_ae_eq⟩

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