Documentation

Mathlib.Analysis.NormedSpace.ENormedSpace

Extended norm #

In this file we define a structure ENormedSpace š•œ 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 ENormedSpace 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 ENormedSpace (š•œ : 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.

Instances For
    instance ENormedSpace.instCoeFunForallENNReal {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    CoeFun (ENormedSpace š•œ V) fun (x : ENormedSpace š•œ V) => V → ENNReal
    Equations
    theorem ENormedSpace.coeFn_injective {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    theorem ENormedSpace.ext {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] {e₁ eā‚‚ : ENormedSpace š•œ V} (h : āˆ€ (x : V), ↑e₁ x = ↑eā‚‚ x) :
    e₁ = eā‚‚
    @[simp]
    theorem ENormedSpace.coe_inj {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] {e₁ eā‚‚ : ENormedSpace š•œ V} :
    ↑e₁ = ↑eā‚‚ ↔ e₁ = eā‚‚
    @[simp]
    theorem ENormedSpace.map_smul {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENormedSpace š•œ V) (c : š•œ) (x : V) :
    @[simp]
    theorem ENormedSpace.map_zero {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENormedSpace š•œ V) :
    @[simp]
    theorem ENormedSpace.eq_zero_iff {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENormedSpace š•œ V) {x : V} :
    @[simp]
    theorem ENormedSpace.map_neg {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENormedSpace š•œ V) (x : V) :
    ↑e (-x) = ↑e x
    theorem ENormedSpace.map_sub_rev {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENormedSpace š•œ V) (x y : V) :
    ↑e (x - y) = ↑e (y - x)
    theorem ENormedSpace.map_add_le {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENormedSpace š•œ V) (x y : V) :
    theorem ENormedSpace.map_sub_le {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENormedSpace š•œ V) (x y : V) :
    instance ENormedSpace.partialOrder {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    Equations
    noncomputable instance ENormedSpace.instTop {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    Top (ENormedSpace š•œ V)

    The ENormedSpace sending each non-zero vector to infinity.

    Equations
    noncomputable instance ENormedSpace.instInhabited {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    Inhabited (ENormedSpace š•œ V)
    Equations
    theorem ENormedSpace.top_map {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] {x : V} (hx : x ≠ 0) :
    noncomputable instance ENormedSpace.instOrderTop {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    OrderTop (ENormedSpace š•œ V)
    Equations
    noncomputable instance ENormedSpace.instSemilatticeSup {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] :
    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem ENormedSpace.coe_max {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e₁ eā‚‚ : ENormedSpace š•œ V) :
    ↑(e₁ āŠ” eā‚‚) = fun (x : V) => ↑e₁ x āŠ” ↑eā‚‚ x
    theorem ENormedSpace.max_map {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e₁ eā‚‚ : ENormedSpace š•œ V) (x : V) :
    @[reducible, inline]
    abbrev ENormedSpace.emetricSpace {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENormedSpace š•œ V) :

    Structure of an EMetricSpace defined by an extended norm.

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

      The subspace of vectors with finite ENormedSpace.

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

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

        Equations
        theorem ENormedSpace.finite_dist_eq {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENormedSpace š•œ V) (x y : ↄe.finiteSubspace) :
        dist x y = (↑e (↑x - ↑y)).toReal
        theorem ENormedSpace.finite_edist_eq {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENormedSpace š•œ V) (x y : ↄe.finiteSubspace) :
        edist x y = ↑e (↑x - ↑y)
        instance ENormedSpace.normedAddCommGroup {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENormedSpace š•œ V) :

        Normed group instance on e.finiteSubspace.

        Equations
        theorem ENormedSpace.finite_norm_eq {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENormedSpace š•œ V) (x : ↄe.finiteSubspace) :
        ‖x‖ = (↑e ↑x).toReal
        instance ENormedSpace.normedSpace {š•œ : Type u_1} {V : Type u_2} [NormedField š•œ] [AddCommGroup V] [Module š•œ V] (e : ENormedSpace š•œ V) :
        NormedSpace š•œ ↄe.finiteSubspace

        Normed space instance on e.finiteSubspace.

        Equations