eLpNorm'_enorm_rpow — Mathlib

English

If a.e. f=g, then MemLp f p μ follows from MemLp g p μ via ae_eq lemma.

Русский

Если f=ae g, то MemLp f p μ следует из MemLp g p μ через ae_eq.

LaTeX

$$$(f=^a_e g)\\Rightarrow MemLp f p μ \Leftrightarrow MemLp g p μ.$$$

Lean4

theorem eLpNorm'_enorm_rpow (f : α → ε) (p q : ℝ) (hq_pos : 0 < q) :
    eLpNorm' (‖f ·‖ₑ ^ 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, enorm_eq_self, ← ENNReal.rpow_mul, mul_comm]

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