lpMeasToLpTrim_ae_eq — Mathlib

English

Let hm be m ≤ m0 and f be an element of lpMeas F 𝕜 m p μ. Then lpMeasToLpTrim F 𝕜 p μ hm f equals f almost everywhere with respect to μ.

Русский

Пусть hm: m ≤ m0 и f ∈ lpMeas F 𝕜 m p μ. Тогда lpMeasToLpTrim F 𝕜 p μ hm f равно f почти по мере μ.

LaTeX

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

Lean4

theorem lpMeasToLpTrim_ae_eq (hm : m ≤ m0) (f : lpMeas F 𝕜 m p μ) : lpMeasToLpTrim F 𝕜 p μ hm f =ᵐ[μ] f :=
  (ae_eq_of_ae_eq_trim (MemLp.coeFn_toLp (memLp_trim_of_mem_lpMeasSubgroup hm f.1 f.mem))).trans
    (mem_lpMeasSubgroup_iff_aestronglyMeasurable.mp f.mem).choose_spec.2.symm

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