instHasSolidNorm — Mathlib

English

There is an order-preserving additive monoid structure on Lp; i.e., Lp is an ordered additive monoid with left-translation monotonicity.

Русский

В Lp существует упорядоченная аддитивная моноидальная структура; т.е. левое приобразование сохраняет порядок.

LaTeX

$$$\text{IsOrderedAddMonoid}(Lp(E,p,\mu)).$$$

Lean4

instance instHasSolidNorm [Fact (1 ≤ p)] : HasSolidNorm (Lp E p μ) :=
  {
    solid := fun f g hfg => by
      rw [← coeFn_le] at hfg
      simp_rw [Lp.norm_def, ENNReal.toReal_le_toReal (Lp.eLpNorm_ne_top f) (Lp.eLpNorm_ne_top g)]
      refine eLpNorm_mono_ae ?_
      filter_upwards [hfg, Lp.coeFn_abs f, Lp.coeFn_abs g] with x hx hxf hxg
      rw [hxf, hxg] at hx
      exact HasSolidNorm.solid hx }

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