English
A similar equivalence holds for the norm-based power: f ∈ Lp implies (||f||^q) ∈ Lp/q, etc., with AEStronglyMeasurable assumptions.
Русский
Аналогичная эквивалентность выполняется для нормированной мощности: f ∈ Lp влечет, что (||f||^q) ∈ L^{p/q}, и т.п., при предположении AEStronglyMeasurable.
LaTeX
$$$MemLp\ (\|f\|^q)\ (p/q)\ μ \iff MemLp\ f\ p\ μ$$$
Lean4
theorem memLp_norm_rpow_iff {q : ℝ≥0∞} {f : α → E} (hf : AEStronglyMeasurable f μ) (q_zero : q ≠ 0) (q_top : q ≠ ∞) :
MemLp (fun x : α => ‖f x‖ ^ q.toReal) (p / q) μ ↔ MemLp f p μ :=
by
refine ⟨fun h => ?_, fun h => h.norm_rpow_div q⟩
apply (memLp_norm_iff hf).1
convert h.norm_rpow_div q⁻¹ using 1
· ext x
rw [Real.norm_eq_abs, Real.abs_rpow_of_nonneg (norm_nonneg _), ← Real.rpow_mul (abs_nonneg _), ENNReal.toReal_inv,
mul_inv_cancel₀, abs_of_nonneg (norm_nonneg _), Real.rpow_one]
simp [ENNReal.toReal_eq_zero_iff, q_zero, q_top]
· rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top, mul_one]
