English
For AEStronglyMeasurable f and q>0, f ∈ Lp if and only if the q-th power of the EN-norm function of f lies in Lp/q; there is a precise equivalence of these MemLp conditions under the q-power transform.
Русский
Для AEStronglyMeasurable f и q>0, f ∈ Lp тогда и только тогда, когда функция x ↦ ||f(x)||^q принадлежит L^{p/q}; существует точное эквивалентное соответствие через преобразование q-й степени.
LaTeX
$$$MemLp(f,p,μ) \iff MemLp(\|f\|^q, p/q, μ)$$$
Lean4
theorem norm_rpow_div {f : α → E} (hf : MemLp f p μ) (q : ℝ≥0∞) : MemLp (fun x : α => ‖f x‖ ^ q.toReal) (p / q) μ :=
by
refine ⟨(hf.1.norm.aemeasurable.pow_const q.toReal).aestronglyMeasurable, ?_⟩
by_cases q_top : q = ∞
· simp [q_top]
by_cases q_zero : q = 0
· simp only [q_zero, ENNReal.toReal_zero, Real.rpow_zero]
by_cases p_zero : p = 0
· simp [p_zero]
rw [ENNReal.div_zero p_zero]
exact (memLp_top_const (1 : ℝ)).2
rw [eLpNorm_norm_rpow _ (ENNReal.toReal_pos q_zero q_top)]
apply ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg
rw [ENNReal.ofReal_toReal q_top, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top, mul_one]
exact hf.2.ne
