nonUnitalNormedRing

Mathlib.Analysis.Normed.Lp.lpSpace

URI: https://scilib.ai/kg/mathlib#lp.nonUnitalNormedRing

Lean4

instance nonUnitalNormedRing : NonUnitalNormedRing (lp B ∞) :=
  { lp.normedAddCommGroup, lp.nonUnitalRing with
    norm_mul_le f
      g :=
      lp.norm_le_of_forall_le (by positivity) fun i ↦
        calc
          ‖(f * g) i‖ ≤ ‖f i‖ * ‖g i‖ := norm_mul_le _ _
          _ ≤ ‖f‖ * ‖g‖ :=
            mul_le_mul (lp.norm_apply_le_norm ENNReal.top_ne_zero f i) (lp.norm_apply_le_norm ENNReal.top_ne_zero g i)
              (norm_nonneg _) (norm_nonneg _) }

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru