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