instNormedStarGroupSubtypePreLpMemAddSubgroup

English

If f and g lie in Memℓp with ∞-norm, then their pointwise product f·g lies again in Memℓp with ∞-norm.

Русский

Если f и g принадлежат Memℓp в бесконечной норме, то их точечно произведение f·g снова принадлежит Memℓp в бесконечной норме.

LaTeX

$$$Mem\\ell p f ∞ \\ \\land\\ Mem\\ell p g ∞\\ \\Rightarrow\\ Mem\\ell p (f\\cdot g) ∞$$$

Lean4

instance [hp : Fact (1 ≤ p)] : NormedStarGroup (lp E p) where
  norm_star_le
    f :=
    le_of_eq <| by
      rcases p.trichotomy with (rfl | rfl | h)
      · exfalso
        have := ENNReal.toReal_mono ENNReal.zero_ne_top hp.elim
        norm_num at this
      · simp only [lp.norm_eq_ciSup, lp.star_apply, norm_star]
      · simp only [lp.norm_eq_tsum_rpow h, lp.star_apply, norm_star]

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