memLp_const_enorm — Mathlib

English

If the EN-norm of c is finite and μ is finite, then the constant function c belongs to MemLp with any p.

Русский

Если EN-норма константы c конечна и μ конечна, то константа c принадлежит MemLp для любого p.

LaTeX

$$MemLp (fun _ : α => c) p μ$$

Lean4

theorem memLp_const_enorm {c : ε'} (hc : ‖c‖ₑ ≠ ⊤) [IsFiniteMeasure μ] : MemLp (fun _ : α ↦ c) p μ :=
  by
  refine ⟨aestronglyMeasurable_const, ?_⟩
  by_cases h0 : p = 0
  · simp [h0]
  by_cases hμ : μ = 0
  · simp [hμ]
  rw [eLpNorm_const c h0 hμ]
  finiteness

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