lpMeasSubgroupToLpTrim_ae_eq — Mathlib

English

Equality almost everywhere between lpMeasSubgroupToLpTrim and its base holds.

Русский

a.e. равенство между lpMeasSubgroupToLpTrim и исходным элементом держится.

LaTeX

$$$\text{lpMeasSubgroupToLpTrim}(F,p,μ,hm,f) =ᵐ[μ] f$$$

Lean4

theorem lpMeasSubgroupToLpTrim_ae_eq (hm : m ≤ m0) (f : lpMeasSubgroup F m p μ) :
    lpMeasSubgroupToLpTrim 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

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