star_mem — Mathlib

English

If f lies in Memℓp, then its star, star f, also lies in Memℓp.

Русский

Если f принадлежит Memℓp, то и star f принадлежит Memℓp.

LaTeX

$$$Mem\\ell p (star f) p\\;\\Rightarrow\\; Mem\\ell p f p$ and $Mem\\ell p (star f) p$$$

Lean4

theorem _root_.Memℓp.star_mem {f : ∀ i, E i} (hf : Memℓp f p) : Memℓp (star f) p :=
  by
  rcases p.trichotomy with (rfl | rfl | hp)
  · apply memℓp_zero
    simp [hf.finite_dsupport]
  · apply memℓp_infty
    simpa using hf.bddAbove
  · apply memℓp_gen
    simpa using hf.summable hp

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