English
For AEStronglyMeasurable f, and q>0, MemLp of the q-th power of the norm is equivalent to MemLp of f with HDiv(q) scaling; i.e., a norm-based reformulation of the previous equivalence.
Русский
Для AEStronglyMeasurable f и q>0, MemLp функции x ↦ ||f(x)||^q является эквивалентным MemLp функции f с масштабированием по q; т.е. нормообразная формулировка предыдущей эквивалентности.
LaTeX
$$$MemLp\ (\|f\|^q)\ (p/q)\ μ \iff MemLp\ f\ p\ μ$$$
Lean4
theorem memLp_enorm_rpow_iff {q : ℝ≥0∞} {f : α → ε} (hf : AEStronglyMeasurable f μ) (q_zero : q ≠ 0) (q_top : q ≠ ∞) :
MemLp (‖f ·‖ₑ ^ q.toReal) (p / q) μ ↔ MemLp f p μ :=
by
refine ⟨fun h => ?_, fun h => h.enorm_rpow_div q⟩
apply (memLp_enorm_iff hf).1
convert h.enorm_rpow_div q⁻¹ using 1
· ext x
have : q.toReal * q.toReal⁻¹ = 1 :=
CommGroupWithZero.mul_inv_cancel q.toReal <| ENNReal.toReal_ne_zero.mpr ⟨q_zero, q_top⟩
simp [← ENNReal.rpow_mul, this, ENNReal.rpow_one]
· rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top, mul_one]
