lpTrimToLpMeasSubgroup_ae_eq — Mathlib

English

Let hm be a relation of sigma-algebras m ≤ m0. For any f in Lp of the trimmed measure μ trim hm, the lifted version lpTrimToLpMeasSubgroup F p μ hm f agrees μ-almost everywhere with f itself.

Русский

Пусть hm задаёт вложение сигма-алгебр m ≤ m0. Для любого f ∈ Lp(F,p)(μ⟂ HM) отображение lpTrimToLpMeasSubgroup F p μ hm f совпадает μ-почти везде с самим f.

LaTeX

$$$lpTrimToLpMeasSubgroup\ F\ p\ μ\ hm\ f =_{\mu} f$$$

Lean4

theorem lpTrimToLpMeasSubgroup_ae_eq (hm : m ≤ m0) (f : Lp F p (μ.trim hm)) :
    lpTrimToLpMeasSubgroup F p μ hm f =ᵐ[μ] f :=
  MemLp.coeFn_toLp (memLp_of_memLp_trim hm (Lp.memLp f))

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