mem_lpMeasSubgroup_toLp_of_trim — Mathlib

English

The lpMeas construct maps to AEStronglyMeasurable elements.

Русский

lpMeas отображает элементы в AEStronglyMeasurable.

LaTeX

$$$f \in lpMeas F 𝕜 p μ \Rightarrow AEStronglyMeasurable[m] f μ$$$

Lean4

/-- If `f` belongs to `Lp` for the measure `μ.trim hm`, then it belongs to the subgroup
`lpMeasSubgroup F m p μ`. -/
theorem mem_lpMeasSubgroup_toLp_of_trim (hm : m ≤ m0) (f : Lp F p (μ.trim hm)) :
    (memLp_of_memLp_trim hm (Lp.memLp f)).toLp f ∈ lpMeasSubgroup F m p μ :=
  by
  let hf_mem_ℒp := memLp_of_memLp_trim hm (Lp.memLp f)
  rw [mem_lpMeasSubgroup_iff_aestronglyMeasurable]
  refine AEStronglyMeasurable.congr ?_ (MemLp.coeFn_toLp hf_mem_ℒp).symm
  exact (Lp.aestronglyMeasurable f).of_trim hm

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