Documentation

Mathlib.Analysis.NormedSpace.ENorm

Extended norm #

In this file we define a structure ENorm š•œ V representing an extended norm (i.e., a norm that can take the value āˆž) on a vector space V over a normed field š•œ. We do not use class for an ENorm because the same space can have more than one extended norm. For example, the space of measurable functions f : Ī± ā†’ ā„ has a family of L_p extended norms.

We prove some basic inequalities, then define

The last definition is an instance because the type involves e.

Implementation notes #

We do not define extended normed groups. They can be added to the chain once someone will need them.

Tags #

normed space, extended norm

structure ENorm (š•œ : Type u_1) (V : Type u_2) [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
Type u_2

Extended norm on a vector space. As in the case of normed spaces, we require only ā€–c ā€¢ xā€– ā‰¤ ā€–cā€– * ā€–xā€– in the definition, then prove an equality in map_smul.

  • toFun : V ā†’ ENNReal
  • eq_zero' : āˆ€ (x : V), ā†‘self x = 0 ā†’ x = 0
  • map_add_le' : āˆ€ (x y : V), ā†‘self (x + y) ā‰¤ ā†‘self x + ā†‘self y
  • map_smul_le' : āˆ€ (c : š•œ) (x : V), ā†‘self (c ā€¢ x) ā‰¤ ā†‘ā€–cā€–ā‚Š * ā†‘self x
Instances For
    theorem ENorm.eq_zero' {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (self : ENorm š•œ V) (x : V) :
    ā†‘self x = 0 ā†’ x = 0
    theorem ENorm.map_add_le' {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (self : ENorm š•œ V) (x : V) (y : V) :
    ā†‘self (x + y) ā‰¤ ā†‘self x + ā†‘self y
    theorem ENorm.map_smul_le' {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (self : ENorm š•œ V) (c : š•œ) (x : V) :
    ā†‘self (c ā€¢ x) ā‰¤ ā†‘ā€–cā€–ā‚Š * ā†‘self x
    instance ENorm.instCoeFunForallENNReal {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    CoeFun (ENorm š•œ V) fun (x : ENorm š•œ V) => V ā†’ ENNReal
    Equations
    • ENorm.instCoeFunForallENNReal = { coe := ENorm.toFun }
    theorem ENorm.coeFn_injective {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    Function.Injective ENorm.toFun
    theorem ENorm.ext {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] {eā‚ : ENorm š•œ V} {eā‚‚ : ENorm š•œ V} (h : āˆ€ (x : V), ā†‘eā‚ x = ā†‘eā‚‚ x) :
    eā‚ = eā‚‚
    theorem ENorm.ext_iff {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] {eā‚ : ENorm š•œ V} {eā‚‚ : ENorm š•œ V} :
    eā‚ = eā‚‚ ā†” āˆ€ (x : V), ā†‘eā‚ x = ā†‘eā‚‚ x
    @[simp]
    theorem ENorm.coe_inj {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] {eā‚ : ENorm š•œ V} {eā‚‚ : ENorm š•œ V} :
    ā†‘eā‚ = ā†‘eā‚‚ ā†” eā‚ = eā‚‚
    @[simp]
    theorem ENorm.map_smul {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENorm š•œ V) (c : š•œ) (x : V) :
    ā†‘e (c ā€¢ x) = ā†‘ā€–cā€–ā‚Š * ā†‘e x
    @[simp]
    theorem ENorm.map_zero {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENorm š•œ V) :
    ā†‘e 0 = 0
    @[simp]
    theorem ENorm.eq_zero_iff {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENorm š•œ V) {x : V} :
    ā†‘e x = 0 ā†” x = 0
    @[simp]
    theorem ENorm.map_neg {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENorm š•œ V) (x : V) :
    ā†‘e (-x) = ā†‘e x
    theorem ENorm.map_sub_rev {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENorm š•œ V) (x : V) (y : V) :
    ā†‘e (x - y) = ā†‘e (y - x)
    theorem ENorm.map_add_le {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENorm š•œ V) (x : V) (y : V) :
    ā†‘e (x + y) ā‰¤ ā†‘e x + ā†‘e y
    theorem ENorm.map_sub_le {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENorm š•œ V) (x : V) (y : V) :
    ā†‘e (x - y) ā‰¤ ā†‘e x + ā†‘e y
    instance ENorm.partialOrder {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    PartialOrder (ENorm š•œ V)
    Equations
    noncomputable instance ENorm.instTop {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    Top (ENorm š•œ V)

    The ENorm sending each non-zero vector to infinity.

    Equations
    • ENorm.instTop = { top := { toFun := fun (x : V) => if x = 0 then 0 else āŠ¤, eq_zero' := ā‹Æ, map_add_le' := ā‹Æ, map_smul_le' := ā‹Æ } }
    noncomputable instance ENorm.instInhabited {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    Inhabited (ENorm š•œ V)
    Equations
    • ENorm.instInhabited = { default := āŠ¤ }
    theorem ENorm.top_map {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] {x : V} (hx : x ā‰  0) :
    ā†‘āŠ¤ x = āŠ¤
    noncomputable instance ENorm.instOrderTop {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    OrderTop (ENorm š•œ V)
    Equations
    noncomputable instance ENorm.instSemilatticeSup {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    SemilatticeSup (ENorm š•œ V)
    Equations
    • ENorm.instSemilatticeSup = let __src := ENorm.partialOrder; SemilatticeSup.mk ā‹Æ ā‹Æ ā‹Æ
    @[simp]
    theorem ENorm.coe_max {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (eā‚ : ENorm š•œ V) (eā‚‚ : ENorm š•œ V) :
    ā†‘(eā‚ āŠ” eā‚‚) = fun (x : V) => max (ā†‘eā‚ x) (ā†‘eā‚‚ x)
    theorem ENorm.max_map {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (eā‚ : ENorm š•œ V) (eā‚‚ : ENorm š•œ V) (x : V) :
    ā†‘(eā‚ āŠ” eā‚‚) x = max (ā†‘eā‚ x) (ā†‘eā‚‚ x)
    @[reducible, inline]
    abbrev ENorm.emetricSpace {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENorm š•œ V) :

    Structure of an EMetricSpace defined by an extended norm.

    Equations
    Instances For
      def ENorm.finiteSubspace {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENorm š•œ V) :
      Subspace š•œ V

      The subspace of vectors with finite enorm.

      Equations
      • e.finiteSubspace = { carrier := {x : V | ā†‘e x < āŠ¤}, add_mem' := ā‹Æ, zero_mem' := ā‹Æ, smul_mem' := ā‹Æ }
      Instances For
        instance ENorm.metricSpace {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENorm š•œ V) :
        MetricSpace ā†„e.finiteSubspace

        Metric space structure on e.finiteSubspace. We use EMetricSpace.toMetricSpace to ensure that this definition agrees with e.emetricSpace.

        Equations
        theorem ENorm.finite_dist_eq {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENorm š•œ V) (x : ā†„e.finiteSubspace) (y : ā†„e.finiteSubspace) :
        dist x y = (ā†‘e (ā†‘x - ā†‘y)).toReal
        theorem ENorm.finite_edist_eq {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENorm š•œ V) (x : ā†„e.finiteSubspace) (y : ā†„e.finiteSubspace) :
        edist x y = ā†‘e (ā†‘x - ā†‘y)
        instance ENorm.normedAddCommGroup {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENorm š•œ V) :
        NormedAddCommGroup ā†„e.finiteSubspace

        Normed group instance on e.finiteSubspace.

        Equations
        theorem ENorm.finite_norm_eq {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENorm š•œ V) (x : ā†„e.finiteSubspace) :
        ā€–xā€– = (ā†‘e ā†‘x).toReal
        instance ENorm.normedSpace {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENorm š•œ V) :
        NormedSpace š•œ ā†„e.finiteSubspace

        Normed space instance on e.finiteSubspace.

        Equations