English
For ENNReal-valued f and appropriate q, MemLp of the q-th power of the norm is equivalent to MemLp of f with exponent adjustment; a version of memLp_norm_rpow_iff with ENNReal indices.
Русский
Для f, принимающего значения в ENNReal, и подходящего q, MemLp степени норм в виде q-й степени эквивалентно MemLp функции f с поправкой показателя; версия memLp_norm_rpow_iff для ENNReal.
LaTeX
$$MemLp\ (\|f\|^q) (p/q) μ ≡ MemLp\ f\ p μ$$
Lean4
theorem isometry_compMeasurePreserving [Fact (1 ≤ p)] (hf : MeasurePreserving f μ μb) :
Isometry (compMeasurePreserving f hf : Lp E p μb → Lp E p μ) :=
AddMonoidHomClass.isometry_of_norm _ (norm_compMeasurePreserving · hf)