Documentation

Mathlib.Analysis.NormedSpace.Dual

The topological dual of a normed space #

In this file we define the topological dual NormedSpace.Dual of a normed space, and the continuous linear map NormedSpace.inclusionInDoubleDual from a normed space into its double dual.

For base field ๐•œ = โ„ or ๐•œ = โ„‚, this map is actually an isometric embedding; we provide a version NormedSpace.inclusionInDoubleDualLi of the map which is of type a bundled linear isometric embedding, E โ†’โ‚—แตข[๐•œ] (Dual ๐•œ (Dual ๐•œ E)).

Since a lot of elementary properties don't require eq_of_dist_eq_zero we start setting up the theory for SeminormedAddCommGroup and we specialize to NormedAddCommGroup when needed.

Main definitions #

Tags #

dual

@[inline, reducible]
abbrev NormedSpace.Dual (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] :
Type (max u_2 u_1)

The topological dual of a seminormed space E.

Instances For
    def NormedSpace.inclusionInDoubleDual (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] :
    E โ†’L[๐•œ] NormedSpace.Dual ๐•œ (NormedSpace.Dual ๐•œ E)

    The inclusion of a normed space in its double (topological) dual, considered as a bounded linear map.

    Instances For
      @[simp]
      theorem NormedSpace.dual_def (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] (x : E) (f : NormedSpace.Dual ๐•œ E) :
      โ†‘(โ†‘(NormedSpace.inclusionInDoubleDual ๐•œ E) x) f = โ†‘f x
      def NormedSpace.dualPairing (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] :
      NormedSpace.Dual ๐•œ E โ†’โ‚—[๐•œ] E โ†’โ‚—[๐•œ] ๐•œ

      The dual pairing as a bilinear form.

      Instances For
        @[simp]
        theorem NormedSpace.dualPairing_apply (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] {v : NormedSpace.Dual ๐•œ E} {x : E} :
        โ†‘(โ†‘(NormedSpace.dualPairing ๐•œ E) v) x = โ†‘v x
        theorem NormedSpace.norm_le_dual_bound (๐•œ : Type v) [IsROrC ๐•œ] {E : Type u} [NormedAddCommGroup E] [NormedSpace ๐•œ E] (x : E) {M : โ„} (hMp : 0 โ‰ค M) (hM : โˆ€ (f : NormedSpace.Dual ๐•œ E), โ€–โ†‘f xโ€– โ‰ค M * โ€–fโ€–) :

        If one controls the norm of every f x, then one controls the norm of x. Compare ContinuousLinearMap.op_norm_le_bound.

        theorem NormedSpace.eq_zero_of_forall_dual_eq_zero (๐•œ : Type v) [IsROrC ๐•œ] {E : Type u} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} (h : โˆ€ (f : NormedSpace.Dual ๐•œ E), โ†‘f x = 0) :
        x = 0
        theorem NormedSpace.eq_zero_iff_forall_dual_eq_zero (๐•œ : Type v) [IsROrC ๐•œ] {E : Type u} [NormedAddCommGroup E] [NormedSpace ๐•œ E] (x : E) :
        x = 0 โ†” โˆ€ (g : NormedSpace.Dual ๐•œ E), โ†‘g x = 0
        theorem NormedSpace.eq_iff_forall_dual_eq (๐•œ : Type v) [IsROrC ๐•œ] {E : Type u} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {x : E} {y : E} :
        x = y โ†” โˆ€ (g : NormedSpace.Dual ๐•œ E), โ†‘g x = โ†‘g y

        See also geometric_hahn_banach_point_point.

        def NormedSpace.inclusionInDoubleDualLi (๐•œ : Type v) [IsROrC ๐•œ] {E : Type u} [NormedAddCommGroup E] [NormedSpace ๐•œ E] :

        The inclusion of a normed space in its double dual is an isometry onto its image.

        Instances For
          def NormedSpace.polar (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] :
          Set E โ†’ Set (NormedSpace.Dual ๐•œ E)

          Given a subset s in a normed space E (over a field ๐•œ), the polar polar ๐•œ s is the subset of Dual ๐•œ E consisting of those functionals which evaluate to something of norm at most one at all points z โˆˆ s.

          Instances For
            theorem NormedSpace.mem_polar_iff (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] {x' : NormedSpace.Dual ๐•œ E} (s : Set E) :
            x' โˆˆ NormedSpace.polar ๐•œ s โ†” โˆ€ (z : E), z โˆˆ s โ†’ โ€–โ†‘x' zโ€– โ‰ค 1
            @[simp]
            theorem NormedSpace.polar_univ (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] :
            NormedSpace.polar ๐•œ Set.univ = {0}
            theorem NormedSpace.isClosed_polar (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] (s : Set E) :
            @[simp]
            theorem NormedSpace.polar_closure (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] (s : Set E) :
            NormedSpace.polar ๐•œ (closure s) = NormedSpace.polar ๐•œ s
            theorem NormedSpace.smul_mem_polar {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] {s : Set E} {x' : NormedSpace.Dual ๐•œ E} {c : ๐•œ} (hc : โˆ€ (z : E), z โˆˆ s โ†’ โ€–โ†‘x' zโ€– โ‰ค โ€–cโ€–) :

            If x' is a dual element such that the norms โ€–x' zโ€– are bounded for z โˆˆ s, then a small scalar multiple of x' is in polar ๐•œ s.

            theorem NormedSpace.polar_ball_subset_closedBall_div {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] {c : ๐•œ} (hc : 1 < โ€–cโ€–) {r : โ„} (hr : 0 < r) :
            theorem NormedSpace.polar_closedBall {๐•œ : Type u_3} {E : Type u_4} [IsROrC ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] {r : โ„} (hr : 0 < r) :

            The polar of closed ball in a normed space E is the closed ball of the dual with inverse radius.

            theorem NormedSpace.isBounded_polar_of_mem_nhds_zero (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] {s : Set E} (s_nhd : s โˆˆ nhds 0) :

            Given a neighborhood s of the origin in a normed space E, the dual norms of all elements of the polar polar ๐•œ s are bounded by a constant.