mem_lpMeasSubgroup_iff_aestronglyMeasurable

English

Equality almost everywhere under trimmed measure transfers to full measure equality of underlying functions under mild measurability assumptions.

Русский

Существует переход равенства почти всюду на усеченной мере к равенству почти всюду на исходной мере при слабых предположениях измеримости.

LaTeX

$$$(hf, hg)$ соответствуют условиям; \ f =ᵐ[μ trim hm] g \Leftrightarrow f =ᵐ[μ] g$$$

Lean4

theorem mem_lpMeasSubgroup_iff_aestronglyMeasurable {m m0 : MeasurableSpace α} {μ : Measure α} {f : Lp F p μ} :
    f ∈ lpMeasSubgroup F m p μ ↔ AEStronglyMeasurable[m] f μ := by
  rw [← AddSubgroup.mem_carrier, lpMeasSubgroup, Set.mem_setOf_eq]

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