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
    instance ENorm.instCoeFunENormForAllENNReal {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    CoeFun (ENorm š•œ V) fun (x : ENorm š•œ V) => V → ENNReal
    Equations
    • ENorm.instCoeFunENormForAllENNReal = { 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.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.

    Equations
    • One or more equations did not get rendered due to their size.
    noncomputable instance ENorm.instInhabitedENorm {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    Inhabited (ENorm š•œ V)
    Equations
    • ENorm.instInhabitedENorm = { 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.instOrderTopENormToLEToPreorderPartialOrder {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    OrderTop (ENorm š•œ V)
    Equations
    noncomputable instance ENorm.instSemilatticeSupENorm {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    SemilatticeSup (ENorm š•œ V)
    Equations
    • One or more equations did not get rendered due to their size.
    @[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]
    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.

    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
      • One or more equations did not get rendered due to their size.
      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.

        Equations
        theorem ENorm.finite_dist_eq {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENorm š•œ V) (x : ↄ(ENorm.finiteSubspace e)) (y : ↄ(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 : ↄ(ENorm.finiteSubspace e)) (y : ↄ(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.

        Equations
        theorem ENorm.finite_norm_eq {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENorm š•œ V) (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) :
        NormedSpace š•œ ↄ(ENorm.finiteSubspace e)

        Normed space instance on e.finiteSubspace.

        Equations