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
  • toFun : V ā†’ ENNReal
  • eq_zero' : āˆ€ (x : V), ā†‘s x = 0 ā†’ x = 0
  • map_add_le' : āˆ€ (x y : V), ā†‘s (x + y) ā‰¤ ā†‘s x + ā†‘s y
  • map_smul_le' : āˆ€ (c : š•œ) (x : V), ā†‘s (c ā€¢ x) ā‰¤ ā†‘ā€–cā€–ā‚Š * ā†‘s x

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.

Instances For
    instance ENorm.instCoeFunENormForAllENNReal {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    CoeFun (ENorm š•œ V) fun x => V ā†’ ENNReal
    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)
    noncomputable instance ENorm.instTopENorm {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    Top (ENorm š•œ V)

    The ENorm sending each non-zero vector to infinity.

    noncomputable instance ENorm.instInhabitedENorm {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    Inhabited (ENorm š•œ V)
    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.instOrderTopENormToLEToPreorderPartialOrder {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    OrderTop (ENorm š•œ V)
    noncomputable instance ENorm.instSemilatticeSupENorm {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    SemilatticeSup (ENorm š•œ V)
    @[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 => 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]
    def 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.

    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.

      Instances For
        instance ENorm.metricSpace {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENorm š•œ V) :

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

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

        Normed group instance on e.finiteSubspace.

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

        Normed space instance on e.finiteSubspace.