eLpNorm'_norm_rpow — Mathlib

English

If f is MemLp and g is ≥ almost everywhere with the ENorm relation, then MemLp f p μ.

Русский

Если f принадлежит MemLp и g во множестве a.e. большe ENorm, то MemLp f p μ.

LaTeX

$$$MemLp f p μ \Rightarrow (\forall^{\mathrm{a}} x, ENorm(f x) ≤ ENorm(g x)) ⇒ MemLp g p μ.$$$

Lean4

theorem eLpNorm'_norm_rpow (f : α → F) (p q : ℝ) (hq_pos : 0 < q) :
    eLpNorm' (fun x => ‖f x‖ ^ q) p μ = eLpNorm' f (p * q) μ ^ q := by
  simp_rw [eLpNorm', ← ENNReal.rpow_mul, ← one_div_mul_one_div, one_div, mul_assoc, inv_mul_cancel₀ hq_pos.ne.symm,
    mul_one, ← ofReal_norm_eq_enorm, Real.norm_eq_abs, abs_eq_self.mpr (Real.rpow_nonneg (norm_nonneg _) _), mul_comm p,
    ← ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) hq_pos.le, ENNReal.rpow_mul]

Похожие утверждения