Documentation

Mathlib.Analysis.Normed.Module.FiniteDimension

Finite dimensional normed spaces over complete fields #

Over a complete nontrivially normed field, in finite dimension, all norms are equivalent and all linear maps are continuous. Moreover, a finite-dimensional subspace is always complete and closed.

Main results: #

Implementation notes #

The fact that all norms are equivalent is not written explicitly, as it would mean having two norms on a single space, which is not the way type classes work. However, if one has a finite-dimensional vector space E with a norm, and a copy E' of this type with another norm, then the identities from E to E' and from E'to E are continuous thanks to LinearMap.continuous_of_finiteDimensional. This gives the desired norm equivalence.

def LinearIsometry.toLinearIsometryEquiv {F : Type u_2} {E₁ : Type u_3} [SeminormedAddCommGroup F] [NormedAddCommGroup E₁] {R₁ : Type u_4} [Field R₁] [Module R₁ E₁] [Module R₁ F] [FiniteDimensional R₁ E₁] [FiniteDimensional R₁ F] (li : E₁ β†’β‚—α΅’[R₁] F) (h : FiniteDimensional.finrank R₁ E₁ = FiniteDimensional.finrank R₁ F) :
E₁ ≃ₗᡒ[R₁] F

A linear isometry between finite dimensional spaces of equal dimension can be upgraded to a linear isometry equivalence.

Equations
  • li.toLinearIsometryEquiv h = { toLinearEquiv := li.linearEquivOfInjective β‹― h, norm_map' := β‹― }
Instances For
    @[simp]
    theorem LinearIsometry.coe_toLinearIsometryEquiv {F : Type u_2} {E₁ : Type u_3} [SeminormedAddCommGroup F] [NormedAddCommGroup E₁] {R₁ : Type u_4} [Field R₁] [Module R₁ E₁] [Module R₁ F] [FiniteDimensional R₁ E₁] [FiniteDimensional R₁ F] (li : E₁ β†’β‚—α΅’[R₁] F) (h : FiniteDimensional.finrank R₁ E₁ = FiniteDimensional.finrank R₁ F) :
    ⇑(li.toLinearIsometryEquiv h) = ⇑li
    @[simp]
    theorem LinearIsometry.toLinearIsometryEquiv_apply {F : Type u_2} {E₁ : Type u_3} [SeminormedAddCommGroup F] [NormedAddCommGroup E₁] {R₁ : Type u_4} [Field R₁] [Module R₁ E₁] [Module R₁ F] [FiniteDimensional R₁ E₁] [FiniteDimensional R₁ F] (li : E₁ β†’β‚—α΅’[R₁] F) (h : FiniteDimensional.finrank R₁ E₁ = FiniteDimensional.finrank R₁ F) (x : E₁) :
    (li.toLinearIsometryEquiv h) x = li x
    def AffineIsometry.toAffineIsometryEquiv {π•œ : Type u_1} {V₁ : Type u_2} {Vβ‚‚ : Type u_3} {P₁ : Type u_4} {Pβ‚‚ : Type u_5} [NormedField π•œ] [NormedAddCommGroup V₁] [SeminormedAddCommGroup Vβ‚‚] [NormedSpace π•œ V₁] [NormedSpace π•œ Vβ‚‚] [MetricSpace P₁] [PseudoMetricSpace Pβ‚‚] [NormedAddTorsor V₁ P₁] [NormedAddTorsor Vβ‚‚ Pβ‚‚] [FiniteDimensional π•œ V₁] [FiniteDimensional π•œ Vβ‚‚] [Inhabited P₁] (li : P₁ →ᡃⁱ[π•œ] Pβ‚‚) (h : FiniteDimensional.finrank π•œ V₁ = FiniteDimensional.finrank π•œ Vβ‚‚) :
    P₁ ≃ᡃⁱ[π•œ] Pβ‚‚

    An affine isometry between finite dimensional spaces of equal dimension can be upgraded to an affine isometry equivalence.

    Equations
    • li.toAffineIsometryEquiv h = AffineIsometryEquiv.mk' (⇑li) (li.linearIsometry.toLinearIsometryEquiv h) default β‹―
    Instances For
      @[simp]
      theorem AffineIsometry.coe_toAffineIsometryEquiv {π•œ : Type u_1} {V₁ : Type u_2} {Vβ‚‚ : Type u_3} {P₁ : Type u_4} {Pβ‚‚ : Type u_5} [NormedField π•œ] [NormedAddCommGroup V₁] [SeminormedAddCommGroup Vβ‚‚] [NormedSpace π•œ V₁] [NormedSpace π•œ Vβ‚‚] [MetricSpace P₁] [PseudoMetricSpace Pβ‚‚] [NormedAddTorsor V₁ P₁] [NormedAddTorsor Vβ‚‚ Pβ‚‚] [FiniteDimensional π•œ V₁] [FiniteDimensional π•œ Vβ‚‚] [Inhabited P₁] (li : P₁ →ᡃⁱ[π•œ] Pβ‚‚) (h : FiniteDimensional.finrank π•œ V₁ = FiniteDimensional.finrank π•œ Vβ‚‚) :
      ⇑(li.toAffineIsometryEquiv h) = ⇑li
      @[simp]
      theorem AffineIsometry.toAffineIsometryEquiv_apply {π•œ : Type u_1} {V₁ : Type u_2} {Vβ‚‚ : Type u_3} {P₁ : Type u_4} {Pβ‚‚ : Type u_5} [NormedField π•œ] [NormedAddCommGroup V₁] [SeminormedAddCommGroup Vβ‚‚] [NormedSpace π•œ V₁] [NormedSpace π•œ Vβ‚‚] [MetricSpace P₁] [PseudoMetricSpace Pβ‚‚] [NormedAddTorsor V₁ P₁] [NormedAddTorsor Vβ‚‚ Pβ‚‚] [FiniteDimensional π•œ V₁] [FiniteDimensional π•œ Vβ‚‚] [Inhabited P₁] (li : P₁ →ᡃⁱ[π•œ] Pβ‚‚) (h : FiniteDimensional.finrank π•œ V₁ = FiniteDimensional.finrank π•œ Vβ‚‚) (x : P₁) :
      (li.toAffineIsometryEquiv h) x = li x
      theorem AffineMap.continuous_of_finiteDimensional {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] {PE : Type u_1} {PF : Type u_2} [MetricSpace PE] [NormedAddTorsor E PE] [MetricSpace PF] [NormedAddTorsor F PF] [FiniteDimensional π•œ E] (f : PE →ᡃ[π•œ] PF) :
      Continuous ⇑f
      theorem AffineEquiv.continuous_of_finiteDimensional {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] {PE : Type u_1} {PF : Type u_2} [MetricSpace PE] [NormedAddTorsor E PE] [MetricSpace PF] [NormedAddTorsor F PF] [FiniteDimensional π•œ E] (f : PE ≃ᡃ[π•œ] PF) :
      Continuous ⇑f
      def AffineEquiv.toHomeomorphOfFiniteDimensional {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] {PE : Type u_1} {PF : Type u_2} [MetricSpace PE] [NormedAddTorsor E PE] [MetricSpace PF] [NormedAddTorsor F PF] [FiniteDimensional π•œ E] (f : PE ≃ᡃ[π•œ] PF) :

      Reinterpret an affine equivalence as a homeomorphism.

      Equations
      • f.toHomeomorphOfFiniteDimensional = { toEquiv := f.toEquiv, continuous_toFun := β‹―, continuous_invFun := β‹― }
      Instances For
        @[simp]
        theorem AffineEquiv.coe_toHomeomorphOfFiniteDimensional {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] {PE : Type u_1} {PF : Type u_2} [MetricSpace PE] [NormedAddTorsor E PE] [MetricSpace PF] [NormedAddTorsor F PF] [FiniteDimensional π•œ E] (f : PE ≃ᡃ[π•œ] PF) :
        ⇑f.toHomeomorphOfFiniteDimensional = ⇑f
        @[simp]
        theorem AffineEquiv.coe_toHomeomorphOfFiniteDimensional_symm {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] {PE : Type u_1} {PF : Type u_2} [MetricSpace PE] [NormedAddTorsor E PE] [MetricSpace PF] [NormedAddTorsor F PF] [FiniteDimensional π•œ E] (f : PE ≃ᡃ[π•œ] PF) :
        ⇑f.toHomeomorphOfFiniteDimensional.symm = ⇑f.symm
        theorem ContinuousLinearMap.continuous_det {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace π•œ] :
        Continuous fun (f : E β†’L[π•œ] E) => f.det
        @[irreducible]

        Any K-Lipschitz map from a subset s of a metric space Ξ± to a finite-dimensional real vector space E' can be extended to a Lipschitz map on the whole space Ξ±, with a slightly worse constant C * K where C only depends on E'. We record a working value for this constant C as lipschitzExtensionConstant E'.

        Equations
        Instances For
          theorem LipschitzOnWith.extend_finite_dimension {Ξ± : Type u_1} [PseudoMetricSpace Ξ±] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {s : Set Ξ±} {f : Ξ± β†’ E'} {K : NNReal} (hf : LipschitzOnWith K f s) :
          βˆƒ (g : Ξ± β†’ E'), LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ Set.EqOn f g s

          Any K-Lipschitz map from a subset s of a metric space Ξ± to a finite-dimensional real vector space E' can be extended to a Lipschitz map on the whole space Ξ±, with a slightly worse constant lipschitzExtensionConstant E' * K.

          theorem LinearMap.exists_antilipschitzWith {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] [FiniteDimensional π•œ E] (f : E β†’β‚—[π•œ] F) (hf : LinearMap.ker f = βŠ₯) :
          βˆƒ K > 0, AntilipschitzWith K ⇑f
          theorem LinearMap.injective_iff_antilipschitz {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] [FiniteDimensional π•œ E] (f : E β†’β‚—[π•œ] F) :
          Function.Injective ⇑f ↔ βˆƒ K > 0, AntilipschitzWith K ⇑f

          A LinearMap on a finite-dimensional space over a complete field is injective iff it is anti-Lipschitz.

          theorem ContinuousLinearMap.isOpen_injective {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] [FiniteDimensional π•œ E] :
          IsOpen {L : E β†’L[π•œ] F | Function.Injective ⇑L}

          The set of injective continuous linear maps E β†’ F is open, if E is finite-dimensional over a complete field.

          theorem LinearIndependent.eventually {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace π•œ] {ΞΉ : Type u_1} [Finite ΞΉ] {f : ΞΉ β†’ E} (hf : LinearIndependent π•œ f) :
          βˆ€αΆ  (g : ΞΉ β†’ E) in nhds f, LinearIndependent π•œ g
          theorem isOpen_setOf_linearIndependent {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace π•œ] {ΞΉ : Type u_1} [Finite ΞΉ] :
          IsOpen {f : ΞΉ β†’ E | LinearIndependent π•œ f}
          theorem isOpen_setOf_nat_le_rank {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] (n : β„•) :
          IsOpen {f : E β†’L[π•œ] F | ↑n ≀ (↑f).rank}
          theorem Basis.opNNNorm_le {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] {ΞΉ : Type u_1} [Fintype ΞΉ] (v : Basis ΞΉ π•œ E) {u : E β†’L[π•œ] F} (M : NNReal) (hu : βˆ€ (i : ΞΉ), β€–u (v i)β€–β‚Š ≀ M) :
          @[deprecated Basis.opNNNorm_le]
          theorem Basis.op_nnnorm_le {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] {ΞΉ : Type u_1} [Fintype ΞΉ] (v : Basis ΞΉ π•œ E) {u : E β†’L[π•œ] F} (M : NNReal) (hu : βˆ€ (i : ΞΉ), β€–u (v i)β€–β‚Š ≀ M) :

          Alias of Basis.opNNNorm_le.

          theorem Basis.opNorm_le {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] {ΞΉ : Type u_1} [Fintype ΞΉ] (v : Basis ΞΉ π•œ E) {u : E β†’L[π•œ] F} {M : ℝ} (hM : 0 ≀ M) (hu : βˆ€ (i : ΞΉ), β€–u (v i)β€– ≀ M) :
          @[deprecated Basis.opNorm_le]
          theorem Basis.op_norm_le {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] {ΞΉ : Type u_1} [Fintype ΞΉ] (v : Basis ΞΉ π•œ E) {u : E β†’L[π•œ] F} {M : ℝ} (hM : 0 ≀ M) (hu : βˆ€ (i : ΞΉ), β€–u (v i)β€– ≀ M) :

          Alias of Basis.opNorm_le.

          theorem Basis.exists_opNNNorm_le {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] {ΞΉ : Type u_1} [Finite ΞΉ] (v : Basis ΞΉ π•œ E) :
          βˆƒ C > 0, βˆ€ {u : E β†’L[π•œ] F} (M : NNReal), (βˆ€ (i : ΞΉ), β€–u (v i)β€–β‚Š ≀ M) β†’ β€–uβ€–β‚Š ≀ C * M

          A weaker version of Basis.opNNNorm_le that abstracts away the value of C.

          @[deprecated Basis.exists_opNNNorm_le]
          theorem Basis.exists_op_nnnorm_le {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] {ΞΉ : Type u_1} [Finite ΞΉ] (v : Basis ΞΉ π•œ E) :
          βˆƒ C > 0, βˆ€ {u : E β†’L[π•œ] F} (M : NNReal), (βˆ€ (i : ΞΉ), β€–u (v i)β€–β‚Š ≀ M) β†’ β€–uβ€–β‚Š ≀ C * M

          Alias of Basis.exists_opNNNorm_le.


          A weaker version of Basis.opNNNorm_le that abstracts away the value of C.

          theorem Basis.exists_opNorm_le {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] {ΞΉ : Type u_1} [Finite ΞΉ] (v : Basis ΞΉ π•œ E) :
          βˆƒ C > 0, βˆ€ {u : E β†’L[π•œ] F} {M : ℝ}, 0 ≀ M β†’ (βˆ€ (i : ΞΉ), β€–u (v i)β€– ≀ M) β†’ β€–uβ€– ≀ C * M

          A weaker version of Basis.opNorm_le that abstracts away the value of C.

          @[deprecated Basis.exists_opNorm_le]
          theorem Basis.exists_op_norm_le {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] {ΞΉ : Type u_1} [Finite ΞΉ] (v : Basis ΞΉ π•œ E) :
          βˆƒ C > 0, βˆ€ {u : E β†’L[π•œ] F} {M : ℝ}, 0 ≀ M β†’ (βˆ€ (i : ΞΉ), β€–u (v i)β€– ≀ M) β†’ β€–uβ€– ≀ C * M

          Alias of Basis.exists_opNorm_le.


          A weaker version of Basis.opNorm_le that abstracts away the value of C.

          theorem AffineSubspace.closed_of_finiteDimensional {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace π•œ] {P : Type u_1} [MetricSpace P] [NormedAddTorsor E P] (s : AffineSubspace π•œ P) [FiniteDimensional π•œ β†₯s.direction] :
          IsClosed ↑s
          theorem exists_norm_le_le_norm_sub_of_finset {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace π•œ] {c : π•œ} (hc : 1 < β€–cβ€–) {R : ℝ} (hR : β€–cβ€– < R) (h : Β¬FiniteDimensional π•œ E) (s : Finset E) :
          βˆƒ (x : E), β€–xβ€– ≀ R ∧ βˆ€ y ∈ s, 1 ≀ β€–y - xβ€–

          In an infinite dimensional space, given a finite number of points, one may find a point with norm at most R which is at distance at least 1 of all these points.

          theorem exists_seq_norm_le_one_le_norm_sub' {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace π•œ] {c : π•œ} (hc : 1 < β€–cβ€–) {R : ℝ} (hR : β€–cβ€– < R) (h : Β¬FiniteDimensional π•œ E) :
          βˆƒ (f : β„• β†’ E), (βˆ€ (n : β„•), β€–f nβ€– ≀ R) ∧ Pairwise fun (m n : β„•) => 1 ≀ β€–f m - f nβ€–

          In an infinite-dimensional normed space, there exists a sequence of points which are all bounded by R and at distance at least 1. For a version not assuming c and R, see exists_seq_norm_le_one_le_norm_sub.

          theorem exists_seq_norm_le_one_le_norm_sub {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace π•œ] (h : Β¬FiniteDimensional π•œ E) :
          βˆƒ (R : ℝ) (f : β„• β†’ E), 1 < R ∧ (βˆ€ (n : β„•), β€–f nβ€– ≀ R) ∧ Pairwise fun (m n : β„•) => 1 ≀ β€–f m - f nβ€–
          theorem FiniteDimensional.of_isCompact_closedBallβ‚€ (π•œ : Type u) [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace π•œ] {r : ℝ} (rpos : 0 < r) (h : IsCompact (Metric.closedBall 0 r)) :

          Riesz's theorem: if a closed ball with center zero of positive radius is compact in a vector space, then the space is finite-dimensional.

          @[deprecated FiniteDimensional.of_isCompact_closedBallβ‚€]
          theorem finiteDimensional_of_isCompact_closedBallβ‚€ (π•œ : Type u) [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace π•œ] {r : ℝ} (rpos : 0 < r) (h : IsCompact (Metric.closedBall 0 r)) :

          Alias of FiniteDimensional.of_isCompact_closedBallβ‚€.


          Riesz's theorem: if a closed ball with center zero of positive radius is compact in a vector space, then the space is finite-dimensional.

          theorem FiniteDimensional.of_isCompact_closedBall (π•œ : Type u) [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace π•œ] {r : ℝ} (rpos : 0 < r) {c : E} (h : IsCompact (Metric.closedBall c r)) :

          Riesz's theorem: if a closed ball of positive radius is compact in a vector space, then the space is finite-dimensional.

          @[deprecated FiniteDimensional.of_isCompact_closedBall]
          theorem finiteDimensional_of_isCompact_closedBall (π•œ : Type u) [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace π•œ] {r : ℝ} (rpos : 0 < r) {c : E} (h : IsCompact (Metric.closedBall c r)) :

          Alias of FiniteDimensional.of_isCompact_closedBall.


          Riesz's theorem: if a closed ball of positive radius is compact in a vector space, then the space is finite-dimensional.

          Riesz's theorem: a locally compact normed vector space is finite-dimensional.

          @[deprecated FiniteDimensional.of_locallyCompactSpace]

          Alias of FiniteDimensional.of_locallyCompactSpace.


          Riesz's theorem: a locally compact normed vector space is finite-dimensional.

          theorem HasCompactSupport.eq_zero_or_finiteDimensional (π•œ : Type u) [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace π•œ] {X : Type u_1} [TopologicalSpace X] [Zero X] [T1Space X] {f : E β†’ X} (hf : HasCompactSupport f) (h'f : Continuous f) :
          f = 0 ∨ FiniteDimensional π•œ E

          If a function has compact support, then either the function is trivial or the space is finite-dimensional.

          theorem HasCompactMulSupport.eq_one_or_finiteDimensional (π•œ : Type u) [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace π•œ] {X : Type u_1} [TopologicalSpace X] [One X] [T1Space X] {f : E β†’ X} (hf : HasCompactMulSupport f) (h'f : Continuous f) :
          f = 1 ∨ FiniteDimensional π•œ E

          If a function has compact multiplicative support, then either the function is trivial or the space is finite-dimensional.

          A locally compact normed vector space is proper.

          @[deprecated ProperSpace.of_locallyCompactSpace]

          Alias of ProperSpace.of_locallyCompactSpace.


          A locally compact normed vector space is proper.

          @[deprecated ProperSpace.of_locallyCompact_module]

          Alias of ProperSpace.of_locallyCompact_module.

          def ContinuousLinearEquiv.piRing {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] [CompleteSpace π•œ] (ΞΉ : Type u_1) [Fintype ΞΉ] [DecidableEq ΞΉ] :
          ((ΞΉ β†’ π•œ) β†’L[π•œ] E) ≃L[π•œ] ΞΉ β†’ E

          Continuous linear equivalence between continuous linear functions π•œβΏ β†’ E and Eⁿ. The spaces π•œβΏ and Eⁿ are represented as ΞΉ β†’ π•œ and ΞΉ β†’ E, respectively, where ΞΉ is a finite type.

          Equations
          Instances For
            theorem continuousOn_clm_apply {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] {X : Type u_1} [TopologicalSpace X] [FiniteDimensional π•œ E] {f : X β†’ E β†’L[π•œ] F} {s : Set X} :
            ContinuousOn f s ↔ βˆ€ (y : E), ContinuousOn (fun (x : X) => (f x) y) s

            A family of continuous linear maps is continuous on s if all its applications are.

            theorem continuous_clm_apply {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type v} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace π•œ F] [CompleteSpace π•œ] {X : Type u_1} [TopologicalSpace X] [FiniteDimensional π•œ E] {f : X β†’ E β†’L[π•œ] F} :
            Continuous f ↔ βˆ€ (y : E), Continuous fun (x : X) => (f x) y
            theorem FiniteDimensional.proper (π•œ : Type u) [NontriviallyNormedField π•œ] (E : Type v) [NormedAddCommGroup E] [NormedSpace π•œ E] [LocallyCompactSpace π•œ] [FiniteDimensional π•œ E] :

            Any finite-dimensional vector space over a locally compact field is proper. We do not register this as an instance to avoid an instance loop when trying to prove the properness of π•œ, and the search for π•œ as an unknown metavariable. Declare the instance explicitly when needed.

            @[instance 900]
            Equations
            • β‹― = β‹―

            A submodule of a locally compact space over a complete field is also locally compact (and even proper).

            Equations
            • β‹― = β‹―
            theorem exists_mem_frontier_infDist_compl_eq_dist {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {x : E} {s : Set E} (hx : x ∈ s) (hs : s β‰  Set.univ) :
            βˆƒ y ∈ frontier s, Metric.infDist x sᢜ = dist x y

            If E is a finite dimensional normed real vector space, x : E, and s is a neighborhood of x that is not equal to the whole space, then there exists a point y ∈ frontier s at distance Metric.infDist x sᢜ from x. See also IsCompact.exists_mem_frontier_infDist_compl_eq_dist.

            theorem IsCompact.exists_mem_frontier_infDist_compl_eq_dist {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] {x : E} {K : Set E} (hK : IsCompact K) (hx : x ∈ K) :
            βˆƒ y ∈ frontier K, Metric.infDist x Kᢜ = dist x y

            If K is a compact set in a nontrivial real normed space and x ∈ K, then there exists a point y of the boundary of K at distance Metric.infDist x Kᢜ from x. See also exists_mem_frontier_infDist_compl_eq_dist.

            theorem summable_norm_iff {Ξ± : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : Ξ± β†’ E} :
            (Summable fun (x : Ξ±) => β€–f xβ€–) ↔ Summable f

            In a finite dimensional vector space over ℝ, the series βˆ‘ x, β€–f xβ€– is unconditionally summable if and only if the series βˆ‘ x, f x is unconditionally summable. One implication holds in any complete normed space, while the other holds only in finite dimensional spaces.

            theorem Summable.norm {Ξ± : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : Ξ± β†’ E} :
            Summable f β†’ Summable fun (x : Ξ±) => β€–f xβ€–

            Alias of the reverse direction of summable_norm_iff.


            In a finite dimensional vector space over ℝ, the series βˆ‘ x, β€–f xβ€– is unconditionally summable if and only if the series βˆ‘ x, f x is unconditionally summable. One implication holds in any complete normed space, while the other holds only in finite dimensional spaces.

            theorem summable_of_isBigO' {ΞΉ : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : ΞΉ β†’ E} {g : ΞΉ β†’ F} (hg : Summable g) (h : f =O[Filter.cofinite] g) :
            theorem Asymptotics.IsBigO.comp_summable {ΞΉ : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [CompleteSpace F] {f : E β†’ F} (hf : f =O[nhds 0] id) {g : ΞΉ β†’ E} (hg : Summable g) :
            theorem summable_of_isBigO_nat' {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : β„• β†’ E} {g : β„• β†’ F} (hg : Summable g) (h : f =O[Filter.atTop] g) :
            theorem summable_of_isEquivalent {ΞΉ : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : ΞΉ β†’ E} {g : ΞΉ β†’ E} (hg : Summable g) (h : Asymptotics.IsEquivalent Filter.cofinite f g) :
            theorem summable_of_isEquivalent_nat {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : β„• β†’ E} {g : β„• β†’ E} (hg : Summable g) (h : Asymptotics.IsEquivalent Filter.atTop f g) :
            theorem IsEquivalent.summable_iff {ΞΉ : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : ΞΉ β†’ E} {g : ΞΉ β†’ E} (h : Asymptotics.IsEquivalent Filter.cofinite f g) :