instNormedAddCommGroup — Mathlib

English

The underlying additive subgroup of the Lp-structure coincides with the Lp space itself.

Русский

Вложенная подгруппа Lp совпадает с самим пространством Lp.

LaTeX

$$$(LpSubmodule \; 𝕜\; E\; p\; μ).toAddSubgroup = Lp\; E\; p\; μ$$$

Lean4

instance instNormedAddCommGroup [hp : Fact (1 ≤ p)] : NormedAddCommGroup (Lp E p μ) :=
  {
    AddGroupNorm.toNormedAddCommGroup
      { toFun := (norm : Lp E p μ → ℝ)
        map_zero' := norm_zero
        neg' := by
          simp only [norm_neg, implies_true] -- squeezed for performance reasons

        add_le' := fun f g =>
          by
          suffices ‖f + g‖ₑ ≤ ‖f‖ₑ + ‖g‖ₑ by
            -- Squeezed for performance reasons
            simpa only [ge_iff_le, enorm, ← ENNReal.coe_add, ENNReal.coe_le_coe] using this
          simp only [Lp.enorm_def]
          exact
            (eLpNorm_congr_ae (AEEqFun.coeFn_add _ _)).trans_le
              (eLpNorm_add_le (Lp.aestronglyMeasurable _) (Lp.aestronglyMeasurable _) hp.out)
        eq_zero_of_map_eq_zero' := fun _ =>
          (norm_eq_zero_iff <| zero_lt_one.trans_le
                hp.1).1 } with
    edist := edist
    edist_dist := Lp.edist_dist }
    -- check no diamond is created

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