ae_fin_strongly_measurable' — Mathlib

English

The symm operations between lpMeas and LpTrimLie preserve the a.e. equalities after applying the symm map.

Русский

Симметрии между lpMeas и LpTrimLie сохраняют эквивалентности a.e. после применения симм-мапа.

LaTeX

$$$(lpMeasToLpTrimLie\ F\ Real\ p\ μ hm).symm (hf.toLp f) = f$$$

Lean4

/-- We do not get `ae_fin_strongly_measurable f (μ.trim hm)`, since we don't have
`f =ᵐ[μ.trim hm] Lp_meas_to_Lp_trim F 𝕜 p μ hm f` but only the weaker
`f =ᵐ[μ] Lp_meas_to_Lp_trim F 𝕜 p μ hm f`. -/
theorem ae_fin_strongly_measurable' (hm : m ≤ m0) (f : lpMeas F 𝕜 m p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) :
    ∃ g, FinStronglyMeasurable g (μ.trim hm) ∧ f.1 =ᵐ[μ] g :=
  ⟨lpMeasSubgroupToLpTrim F p μ hm f, Lp.finStronglyMeasurable _ hp_ne_zero hp_ne_top,
    (lpMeasSubgroupToLpTrim_ae_eq hm f).symm⟩

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