memLp_enorm_iff — Mathlib

English

For AEStronglyMeasurable f, MemLp (‖f‖) p μ is equivalent to MemLp f p μ.

Русский

Для AEStronglyMeasurable f эквивалентны MemLp (‖f‖) p μ и MemLp f p μ.

LaTeX

$$memLp_enorm_iff {f} (hf : AEStronglyMeasurable f μ) : MemLp (‖f‖) p μ ↔ MemLp f p μ.$$

Lean4

theorem memLp_enorm_iff {f : α → ε} (hf : AEStronglyMeasurable f μ) : MemLp (‖f ·‖ₑ) p μ ↔ MemLp f p μ :=
  ⟨fun h => ⟨hf, by rw [← eLpNorm_enorm]; exact h.2⟩, fun h => h.enorm⟩

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