English
If f ∈ Lp(E,p,μ) and q>0, then the q-th power of the EN-norm of f is in Lp/q: the function x ↦ ||f(x)||^q has finite (p/q)-Lp norm.
Русский
Если f ∈ Lp(E,p,μ) и q>0, то функция x ↦ ||f(x)||^q принадлежит L^(p/q): нормa (p/q)-Lp у функции x ↦ ||f(x)||^q конечна.
LaTeX
$$$MemLp\ (\|f\|_E^q)\ (p/q)\ μ$$
Lean4
theorem enorm_rpow_div {f : α → ε} (hf : MemLp f p μ) (q : ℝ≥0∞) : MemLp (‖f ·‖ₑ ^ q.toReal) (p / q) μ :=
by
refine ⟨(hf.1.enorm.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]
by_cases p_zero : p = 0
· simp [p_zero]
rw [ENNReal.div_zero p_zero]
simpa only [ENNReal.rpow_zero, eLpNorm_exponent_top] using (memLp_top_const_enorm (by simp)).2
rw [eLpNorm_enorm_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
