English
The membership of an Lp-space element in lpMeas equals AEStronglyMeasurable criterion.
Русский
Членство элемента Lp в lpMeas эквивалентно AEStronglyMeasurable критерию.
LaTeX
$$$f \in lpMeas F p μ \iff AEStronglyMeasurable[m] f μ$$$
Lean4
/-- If `f` belongs to `lpMeasSubgroup F m p μ`, then the measurable function it is almost
everywhere equal to (given by `AEMeasurable.mk`) belongs to `ℒp` for the measure `μ.trim hm`. -/
theorem memLp_trim_of_mem_lpMeasSubgroup (hm : m ≤ m0) (f : Lp F p μ) (hf_meas : f ∈ lpMeasSubgroup F m p μ) :
MemLp (mem_lpMeasSubgroup_iff_aestronglyMeasurable.mp hf_meas).choose p (μ.trim hm) :=
by
have hf : AEStronglyMeasurable[m] f μ := mem_lpMeasSubgroup_iff_aestronglyMeasurable.mp hf_meas
let g := hf.choose
obtain ⟨hg, hfg⟩ := hf.choose_spec
change MemLp g p (μ.trim hm)
refine ⟨hg.aestronglyMeasurable, ?_⟩
have h_eLpNorm_fg : eLpNorm g p (μ.trim hm) = eLpNorm f p μ :=
by
rw [eLpNorm_trim hm hg]
exact eLpNorm_congr_ae hfg.symm
rw [h_eLpNorm_fg]
exact Lp.eLpNorm_lt_top f
