Mathlib.Analysis.Normed.Module.FiniteDimension

LinearIsometry.toLinearIsometryEquiv definition

(li : E₁ →ₗᵢ[R₁] F) (h : finrank R₁ E₁ = finrank R₁ F) : E₁ ≃ₗᵢ[R₁] F

Full source

/-- A linear isometry between finite dimensional spaces of equal dimension can be upgraded
    to a linear isometry equivalence. -/
def toLinearIsometryEquiv (li : E₁ →ₗᵢ[R₁] F) (h : finrank R₁ E₁ = finrank R₁ F) :
    E₁ ≃ₗᵢ[R₁] F where
  toLinearEquiv := li.toLinearMap.linearEquivOfInjective li.injective h
  norm_map' := li.norm_map'

Linear isometry to linear isometric equivalence for equal-dimensional spaces

Informal description

Given a linear isometry $ \text{li} \colon E_1 \to F $ between finite-dimensional normed vector spaces over a field $ R_1 $, and assuming that the dimensions of $ E_1 $ and $ F $ over $ R_1 $ are equal, the function constructs a linear isometric equivalence $ E_1 \simeq F $. This equivalence is obtained by upgrading the injective linear isometry $ \text{li} $ to a bijective isometry using the dimension condition.

LinearIsometry.coe_toLinearIsometryEquiv theorem

(li : E₁ →ₗᵢ[R₁] F) (h : finrank R₁ E₁ = finrank R₁ F) : (li.toLinearIsometryEquiv h : E₁ → F) = li

Full source

@[simp]
theorem coe_toLinearIsometryEquiv (li : E₁ →ₗᵢ[R₁] F) (h : finrank R₁ E₁ = finrank R₁ F) :
    (li.toLinearIsometryEquiv h : E₁ → F) = li :=
  rfl

Underlying Function of Linear Isometric Equivalence for Equal-Dimensional Spaces Matches Original Isometry

Informal description

Let $E_1$ and $F$ be finite-dimensional normed vector spaces over a field $R_1$, and let $\text{li} : E_1 \to F$ be a linear isometry. If the dimensions of $E_1$ and $F$ over $R_1$ are equal (i.e., $\text{finrank}_{R_1} E_1 = \text{finrank}_{R_1} F$), then the underlying function of the linear isometric equivalence $\text{li.toLinearIsometryEquiv} h$ (where $h$ is the dimension equality hypothesis) coincides with $\text{li}$ itself.

LinearIsometry.toLinearIsometryEquiv_apply theorem

 (li : E₁ →ₗᵢ[R₁] F) (h : finrank R₁ E₁ = finrank R₁ F) (x : E₁) : (li.toLinearIsometryEquiv h) x = li x

Full source

@[simp]
theorem toLinearIsometryEquiv_apply (li : E₁ →ₗᵢ[R₁] F) (h : finrank R₁ E₁ = finrank R₁ F)
    (x : E₁) : (li.toLinearIsometryEquiv h) x = li x :=
  rfl

Equality of Linear Isometry and its Isometric Equivalence on Elements

Informal description

Let $E_1$ and $F$ be finite-dimensional normed vector spaces over a field $R_1$, and let $\text{li} : E_1 \to F$ be a linear isometry. If the dimensions of $E_1$ and $F$ over $R_1$ are equal, then for any $x \in E_1$, the image of $x$ under the induced linear isometric equivalence $\text{li.toLinearIsometryEquiv} h$ is equal to $\text{li}(x)$.

AffineIsometry.toAffineIsometryEquiv definition

 [Inhabited P₁] (li : P₁ →ᵃⁱ[𝕜] P₂) (h : finrank 𝕜 V₁ = finrank 𝕜 V₂) : P₁ ≃ᵃⁱ[𝕜] P₂

Full source

/-- An affine isometry between finite dimensional spaces of equal dimension can be upgraded
    to an affine isometry equivalence. -/
def toAffineIsometryEquiv [Inhabited P₁] (li : P₁ →ᵃⁱ[𝕜] P₂) (h : finrank 𝕜 V₁ = finrank 𝕜 V₂) :
    P₁ ≃ᵃⁱ[𝕜] P₂ :=
  AffineIsometryEquiv.mk' li (li.linearIsometry.toLinearIsometryEquiv h)
    (Inhabited.default (α := P₁)) fun p => by simp

Affine isometric embedding to equivalence for equal-dimensional spaces

Informal description

Given an affine isometric embedding $ \text{li} \colon P_1 \to P_2 $ between finite-dimensional normed affine spaces over a normed field $ \mathbb{K} $, and assuming that the underlying vector spaces $ V_1 $ and $ V_2 $ have the same finite dimension over $ \mathbb{K} $, the function constructs an affine isometric equivalence $ P_1 \simeq P_2 $. This equivalence is obtained by upgrading the injective affine isometry $ \text{li} $ to a bijective isometry using the dimension condition, with the base point taken as the default inhabitant of $ P_1 $.

AffineIsometry.coe_toAffineIsometryEquiv theorem

 [Inhabited P₁] (li : P₁ →ᵃⁱ[𝕜] P₂) (h : finrank 𝕜 V₁ = finrank 𝕜 V₂) : (li.toAffineIsometryEquiv h : P₁ → P₂) = li

Full source

@[simp]
theorem coe_toAffineIsometryEquiv [Inhabited P₁] (li : P₁ →ᵃⁱ[𝕜] P₂)
    (h : finrank 𝕜 V₁ = finrank 𝕜 V₂) : (li.toAffineIsometryEquiv h : P₁ → P₂) = li :=
  rfl

Equality of Affine Isometric Embedding and its Induced Equivalence

Informal description

Let $P_1$ and $P_2$ be finite-dimensional normed affine spaces over a normed field $\mathbb{K}$, with underlying vector spaces $V_1$ and $V_2$ respectively. Given an affine isometric embedding $\text{li} : P_1 \to P_2$ and assuming $\text{finrank}_{\mathbb{K}} V_1 = \text{finrank}_{\mathbb{K}} V_2$, the induced affine isometric equivalence $\text{li.toAffineIsometryEquiv} h$ satisfies $(\text{li.toAffineIsometryEquiv} h)(x) = \text{li}(x)$ for all $x \in P_1$.

AffineIsometry.toAffineIsometryEquiv_apply theorem

 [Inhabited P₁] (li : P₁ →ᵃⁱ[𝕜] P₂) (h : finrank 𝕜 V₁ = finrank 𝕜 V₂) (x : P₁) : (li.toAffineIsometryEquiv h) x = li x

Full source

@[simp]
theorem toAffineIsometryEquiv_apply [Inhabited P₁] (li : P₁ →ᵃⁱ[𝕜] P₂)
    (h : finrank 𝕜 V₁ = finrank 𝕜 V₂) (x : P₁) : (li.toAffineIsometryEquiv h) x = li x :=
  rfl

Affine Isometric Equivalence Preserves Embedding Images in Equal-Dimensional Spaces

Informal description

Let $P_1$ and $P_2$ be finite-dimensional normed affine spaces over a normed field $\mathbb{K}$, with underlying vector spaces $V_1$ and $V_2$ respectively. Given an affine isometric embedding $\text{li} \colon P_1 \to P_2$ and assuming that $\text{finrank}_{\mathbb{K}} V_1 = \text{finrank}_{\mathbb{K}} V_2$, then for any point $x \in P_1$, the image of $x$ under the induced affine isometric equivalence $\text{li.toAffineIsometryEquiv h}$ is equal to $\text{li}(x)$.

AffineMap.continuous_of_finiteDimensional theorem

(f : PE →ᵃ[𝕜] PF) : Continuous f

Full source

theorem AffineMap.continuous_of_finiteDimensional (f : PE →ᵃ[𝕜] PF) : Continuous f :=
  AffineMap.continuous_linear_iff.1 f.linear.continuous_of_finiteDimensional

Continuity of Affine Maps on Finite-Dimensional Spaces over Complete Fields

Informal description

For any affine map $f \colon PE \to PF$ between finite-dimensional normed affine spaces over a complete nontrivially normed field $\mathbb{K}$, the map $f$ is continuous.

AffineEquiv.continuous_of_finiteDimensional theorem

(f : PE ≃ᵃ[𝕜] PF) : Continuous f

Full source

theorem AffineEquiv.continuous_of_finiteDimensional (f : PE ≃ᵃ[𝕜] PF) : Continuous f :=
  f.toAffineMap.continuous_of_finiteDimensional

Continuity of Affine Equivalences on Finite-Dimensional Spaces over Complete Fields

Informal description

Let $\mathbb{K}$ be a complete nontrivially normed field, and let $PE$ and $PF$ be finite-dimensional normed affine spaces over $\mathbb{K}$. Then any affine equivalence $f \colon PE \to PF$ is continuous.

AffineEquiv.toHomeomorphOfFiniteDimensional definition

(f : PE ≃ᵃ[𝕜] PF) : PE ≃ₜ PF

Full source

/-- Reinterpret an affine equivalence as a homeomorphism. -/
def AffineEquiv.toHomeomorphOfFiniteDimensional (f : PE ≃ᵃ[𝕜] PF) : PE ≃ₜ PF where
  toEquiv := f.toEquiv
  continuous_toFun := f.continuous_of_finiteDimensional
  continuous_invFun :=
    haveI : FiniteDimensional 𝕜 F := f.linear.finiteDimensional
    f.symm.continuous_of_finiteDimensional

Homeomorphism from affine equivalence on finite-dimensional spaces

Informal description

Given a complete nontrivially normed field $\mathbb{K}$ and finite-dimensional normed affine spaces $PE$ and $PF$ over $\mathbb{K}$, any affine equivalence $f \colon PE \to PF$ can be reinterpreted as a homeomorphism between $PE$ and $PF$. This means $f$ is a continuous bijection with a continuous inverse, preserving the topological structure of the spaces.

AffineEquiv.coe_toHomeomorphOfFiniteDimensional theorem

(f : PE ≃ᵃ[𝕜] PF) : ⇑f.toHomeomorphOfFiniteDimensional = f

Full source

@[simp]
theorem AffineEquiv.coe_toHomeomorphOfFiniteDimensional (f : PE ≃ᵃ[𝕜] PF) :
    ⇑f.toHomeomorphOfFiniteDimensional = f :=
  rfl

Equality of Affine Equivalence and its Homeomorphism Representation on Finite-Dimensional Spaces

Informal description

Let $\mathbb{K}$ be a complete nontrivially normed field, and let $PE$ and $PF$ be finite-dimensional normed affine spaces over $\mathbb{K}$. For any affine equivalence $f \colon PE \to PF$, the underlying function of the homeomorphism $f.toHomeomorphOfFiniteDimensional$ equals $f$ itself.

AffineEquiv.coe_toHomeomorphOfFiniteDimensional_symm theorem

(f : PE ≃ᵃ[𝕜] PF) : ⇑f.toHomeomorphOfFiniteDimensional.symm = f.symm

Full source

@[simp]
theorem AffineEquiv.coe_toHomeomorphOfFiniteDimensional_symm (f : PE ≃ᵃ[𝕜] PF) :
    ⇑f.toHomeomorphOfFiniteDimensional.symm = f.symm :=
  rfl

Inverse of Homeomorphism Induced by Affine Equivalence on Finite-Dimensional Spaces

Informal description

For any affine equivalence $f \colon PE \to PF$ between finite-dimensional normed affine spaces $PE$ and $PF$ over a complete nontrivially normed field $\mathbb{K}$, the inverse of the homeomorphism induced by $f$ is equal to the inverse of $f$ itself. In other words, $(f^{\text{homeo}})^{-1} = f^{-1}$.

ContinuousLinearMap.continuous_det theorem

: Continuous fun f : E →L[𝕜] E => f.det

Full source

theorem ContinuousLinearMap.continuous_det : Continuous fun f : E →L[𝕜] E => f.det := by
  change Continuous fun f : E →L[𝕜] E => LinearMap.det (f : E →ₗ[𝕜] E)
  -- TODO: this could be easier with `det_cases`
  by_cases h : ∃ s : Finset E, Nonempty (Basis (↥s) 𝕜 E)
  · rcases h with ⟨s, ⟨b⟩⟩
    haveI : FiniteDimensional 𝕜 E := FiniteDimensional.of_fintype_basis b
    classical
    simp_rw [LinearMap.det_eq_det_toMatrix_of_finset b]
    refine Continuous.matrix_det ?_
    exact
      ((LinearMap.toMatrix b b).toLinearMap.comp
          (ContinuousLinearMap.coeLM 𝕜)).continuous_of_finiteDimensional
  · rw [LinearMap.det]
    simpa only [h, MonoidHom.one_apply, dif_neg, not_false_iff] using continuous_const

Continuity of Determinant for Continuous Linear Endomorphisms on Finite-Dimensional Spaces

Informal description

For any continuous linear endomorphism $f$ of a finite-dimensional normed vector space $E$ over a complete nontrivially normed field $\mathbb{K}$, the determinant function $f \mapsto \det(f)$ is continuous.

lipschitzExtensionConstant definition

Full source

/-- 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'`. -/
irreducible_def lipschitzExtensionConstant (E' : Type*) [NormedAddCommGroup E'] [NormedSpace ℝ E']
  [FiniteDimensional ℝ E'] : ℝ≥0 :=
  let A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
  max (‖A.symm.toContinuousLinearMap‖₊ * ‖A.toContinuousLinearMap‖₊) 1

Lipschitz extension constant for finite-dimensional spaces

Informal description

For any finite-dimensional real normed vector space $ E' $, the constant $ \text{lipschitzExtensionConstant}(E') $ is defined as the maximum between 1 and the product of the operator norms of the continuous linear equivalence $ A $ and its inverse, where $ A $ is the continuous linear equivalence induced by a basis of $ E' $. This constant is used to extend any $ K $-Lipschitz map defined on a subset of a metric space to a Lipschitz map on the whole space, with a Lipschitz constant multiplied by $ \text{lipschitzExtensionConstant}(E') $.

lipschitzExtensionConstant_def theorem

: eta_helper Eq✝ @lipschitzExtensionConstant.{} @(delta% @definition✝)

Full source

/-- 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'`. -/
irreducible_def lipschitzExtensionConstant (E' : Type*) [NormedAddCommGroup E'] [NormedSpace ℝ E']
  [FiniteDimensional ℝ E'] : ℝ≥0 :=
  let A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
  max (‖A.symm.toContinuousLinearMap‖₊ * ‖A.toContinuousLinearMap‖₊) 1

Definition of the Lipschitz Extension Constant for Finite-Dimensional Spaces

Informal description

The constant `lipschitzExtensionConstant E'` is defined as the maximum between 1 and the product of the operator norms of the continuous linear equivalence induced by a basis of a finite-dimensional real normed vector space `E'` and its inverse.

lipschitzExtensionConstant_pos theorem

 (E' : Type*) [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] : 0 < lipschitzExtensionConstant E'

Full source

theorem lipschitzExtensionConstant_pos (E' : Type*) [NormedAddCommGroup E'] [NormedSpace ℝ E']
    [FiniteDimensional ℝ E'] : 0 < lipschitzExtensionConstant E' := by
  rw [lipschitzExtensionConstant]
  exact zero_lt_one.trans_le (le_max_right _ _)

Positivity of the Lipschitz Extension Constant in Finite-Dimensional Spaces

Informal description

For any finite-dimensional real normed vector space $E'$, the Lipschitz extension constant $\text{lipschitzExtensionConstant}(E')$ is strictly positive, i.e., $\text{lipschitzExtensionConstant}(E') > 0$.

LipschitzOnWith.extend_finite_dimension theorem

 {α : Type*} [PseudoMetricSpace α] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E']
  {s : Set α} {f : α → E'} {K : ℝ≥0} (hf : LipschitzOnWith K f s) :
  ∃ g : α → E', LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s

Full source

/-- 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 LipschitzOnWith.extend_finite_dimension {α : Type*} [PseudoMetricSpace α] {E' : Type*}
    [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {s : Set α} {f : α → E'}
    {K : ℝ≥0} (hf : LipschitzOnWith K f s) :
    ∃ g : α → E', LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s := by
  /- This result is already known for spaces `ι → ℝ`. We use a continuous linear equiv between
    `E'` and such a space to transfer the result to `E'`. -/
  let ι : Type _ := Basis.ofVectorSpaceIndex ℝ E'
  let A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
  have LA : LipschitzWith ‖A.toContinuousLinearMap‖₊ A := by apply A.lipschitz
  have L : LipschitzOnWith (‖A.toContinuousLinearMap‖₊ * K) (A ∘ f) s :=
    LA.comp_lipschitzOnWith hf
  obtain ⟨g, hg, gs⟩ :
    ∃ g : α → ι → ℝ, LipschitzWith (‖A.toContinuousLinearMap‖₊ * K) g ∧ EqOn (A ∘ f) g s :=
    L.extend_pi
  refine ⟨A.symm ∘ g, ?_, ?_⟩
  · have LAsymm : LipschitzWith ‖A.symm.toContinuousLinearMap‖₊ A.symm := by
      apply A.symm.lipschitz
    apply (LAsymm.comp hg).weaken
    rw [lipschitzExtensionConstant, ← mul_assoc]
    exact mul_le_mul' (le_max_left _ _) le_rfl
  · intro x hx
    have : A (f x) = g x := gs hx
    simp only [(· ∘ ·), ← this, A.symm_apply_apply]

Lipschitz Extension Theorem for Finite-Dimensional Real Normed Spaces

Informal description

Let $\alpha$ be a metric space and $E'$ a finite-dimensional real normed vector space. For any subset $s \subseteq \alpha$ and any $K$-Lipschitz function $f \colon s \to E'$, there exists an extension $g \colon \alpha \to E'$ of $f$ such that: 1. $g$ is Lipschitz with constant $\text{lipschitzExtensionConstant}(E') \cdot K$, where $\text{lipschitzExtensionConstant}(E')$ is a constant depending only on $E'$. 2. $g$ agrees with $f$ on $s$, i.e., $g(x) = f(x)$ for all $x \in s$.

LinearMap.exists_antilipschitzWith theorem

[FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F) (hf : LinearMap.ker f = ⊥) : ∃ K > 0, AntilipschitzWith K f

Full source

theorem LinearMap.exists_antilipschitzWith [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F)
    (hf : LinearMap.ker f = ⊥) : ∃ K > 0, AntilipschitzWith K f := by
  cases subsingleton_or_nontrivial E
  · exact ⟨1, zero_lt_one, AntilipschitzWith.of_subsingleton⟩
  · rw [LinearMap.ker_eq_bot] at hf
    let e : E ≃L[𝕜] LinearMap.range f := (LinearEquiv.ofInjective f hf).toContinuousLinearEquiv
    exact ⟨_, e.nnnorm_symm_pos, e.antilipschitz⟩

Existence of Antilipschitz Constant for Injective Linear Maps on Finite-Dimensional Spaces

Informal description

Let $E$ and $F$ be vector spaces over a field $\mathbb{K}$, with $E$ being finite-dimensional. For any injective linear map $f \colon E \to F$ (i.e., $\ker f = \{0\}$), there exists a constant $K > 0$ such that $f$ is antilipschitz with constant $K$, meaning that for all $x, y \in E$, \[ \|x - y\| \leq K \|f(x) - f(y)\|. \]

LinearMap.injective_iff_antilipschitz theorem

[FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F) : Injective f ↔ ∃ K > 0, AntilipschitzWith K f

Full source

/-- A `LinearMap` on a finite-dimensional space over a complete field
  is injective iff it is anti-Lipschitz. -/
theorem LinearMap.injective_iff_antilipschitz [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F) :
    InjectiveInjective f ↔ ∃ K > 0, AntilipschitzWith K f := by
  constructor
  · rw [← LinearMap.ker_eq_bot]
    exact f.exists_antilipschitzWith
  · rintro ⟨K, -, H⟩
    exact H.injective

Injective Linear Maps on Finite-Dimensional Spaces are Anti-Lipschitz

Informal description

Let $E$ and $F$ be vector spaces over a complete nontrivially normed field $\mathbb{K}$, with $E$ being finite-dimensional. For a linear map $f \colon E \to F$, the following are equivalent: 1. $f$ is injective. 2. There exists a constant $K > 0$ such that $f$ is anti-Lipschitz with constant $K$, i.e., for all $x, y \in E$, \[ \|x - y\| \leq K \|f(x) - f(y)\|. \]

ContinuousLinearMap.isOpen_injective theorem

[FiniteDimensional 𝕜 E] : IsOpen {L : E →L[𝕜] F | Injective L}

Full source

/-- The set of injective continuous linear maps `E → F` is open,
  if `E` is finite-dimensional over a complete field. -/
theorem ContinuousLinearMap.isOpen_injective [FiniteDimensional 𝕜 E] :
    IsOpen { L : E →L[𝕜] F | Injective L } := by
  rw [isOpen_iff_eventually]
  rintro φ₀ hφ₀
  rcases φ₀.injective_iff_antilipschitz.mp hφ₀ with ⟨K, K_pos, H⟩
  have : ∀ᶠ φ in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹ := eventually_nnnorm_sub_lt _ <| inv_pos_of_pos K_pos
  filter_upwards [this] with φ hφ
  apply φ.injective_iff_antilipschitz.mpr
  exact ⟨(K⁻¹ - ‖φ - φ₀‖₊)⁻¹, inv_pos_of_pos (tsub_pos_of_lt hφ),
    H.add_sub_lipschitzWith (φ - φ₀).lipschitz hφ⟩

Openness of Injective Continuous Linear Maps in Finite-Dimensional Spaces

Informal description

Let $E$ and $F$ be normed vector spaces over a complete nontrivially normed field $\mathbb{K}$, with $E$ finite-dimensional. Then the set of injective continuous linear maps from $E$ to $F$ is open in the space of all continuous linear maps from $E$ to $F$.

LinearIndependent.eventually theorem

{ι} [Finite ι] {f : ι → E} (hf : LinearIndependent 𝕜 f) : ∀ᶠ g in 𝓝 f, LinearIndependent 𝕜 g

Full source

protected theorem LinearIndependent.eventually {ι} [Finite ι] {f : ι → E}
    (hf : LinearIndependent 𝕜 f) : ∀ᶠ g in 𝓝 f, LinearIndependent 𝕜 g := by
  cases nonempty_fintype ι
  classical
  simp only [Fintype.linearIndependent_iff'] at hf ⊢
  rcases LinearMap.exists_antilipschitzWith _ hf with ⟨K, K0, hK⟩
  have : Tendsto (fun g : ι → E => ∑ i, ‖g i - f i‖) (𝓝 f) (𝓝 <| ∑ i, ‖f i - f i‖) :=
    tendsto_finset_sum _ fun i _ =>
      Tendsto.norm <| ((continuous_apply i).tendsto _).sub tendsto_const_nhds
  simp only [sub_self, norm_zero, Finset.sum_const_zero] at this
  refine (this.eventually (gt_mem_nhds <| inv_pos.2 K0)).mono fun g hg => ?_
  replace hg : ∑ i, ‖g i - f i‖₊ < K⁻¹ := by
    rw [← NNReal.coe_lt_coe]
    push_cast
    exact hg
  rw [LinearMap.ker_eq_bot]
  refine (hK.add_sub_lipschitzWith (LipschitzWith.of_dist_le_mul fun v u => ?_) hg).injective
  simp only [dist_eq_norm, LinearMap.lsum_apply, Pi.sub_apply, LinearMap.sum_apply,
    LinearMap.comp_apply, LinearMap.proj_apply, LinearMap.smulRight_apply, LinearMap.id_apply, ←
    Finset.sum_sub_distrib, ← smul_sub, ← sub_smul, NNReal.coe_sum, coe_nnnorm, Finset.sum_mul]
  refine norm_sum_le_of_le _ fun i _ => ?_
  rw [norm_smul, mul_comm]
  gcongr
  exact norm_le_pi_norm (v - u) i

Persistence of Linear Independence in Finite-Dimensional Vector Spaces

Informal description

Let $\mathbb{K}$ be a field, $E$ a vector space over $\mathbb{K}$, and $\iota$ a finite index set. For any linearly independent family of vectors $f \colon \iota \to E$, there exists a neighborhood $\mathcal{N}(f)$ in the topology of pointwise convergence such that every $g \in \mathcal{N}(f)$ is also linearly independent over $\mathbb{K}$.

isOpen_setOf_linearIndependent theorem

{ι : Type*} [Finite ι] : IsOpen {f : ι → E | LinearIndependent 𝕜 f}

Full source

theorem isOpen_setOf_linearIndependent {ι : Type*} [Finite ι] :
    IsOpen { f : ι → E | LinearIndependent 𝕜 f } :=
  isOpen_iff_mem_nhds.2 fun _ => LinearIndependent.eventually

Openness of the Set of Linearly Independent Vector Families in Finite-Dimensional Spaces

Informal description

For any finite index set $\iota$, the set of all families of vectors $f \colon \iota \to E$ that are linearly independent over the field $\mathbb{K}$ is an open subset in the topology of pointwise convergence on the space of all such families.

isOpen_setOf_nat_le_rank theorem

(n : ℕ) : IsOpen {f : E →L[𝕜] F | ↑n ≤ (f : E →ₗ[𝕜] F).rank}

Full source

theorem isOpen_setOf_nat_le_rank (n : ℕ) :
    IsOpen { f : E →L[𝕜] F | ↑n ≤ (f : E →ₗ[𝕜] F).rank } := by
  simp only [LinearMap.le_rank_iff_exists_linearIndependent_finset, setOf_exists, ← exists_prop]
  refine isOpen_biUnion fun t _ => ?_
  have : Continuous fun f : E →L[𝕜] F => fun x : (t : Set E) => f x :=
    continuous_pi fun x => (ContinuousLinearMap.apply 𝕜 F (x : E)).continuous
  exact isOpen_setOf_linearIndependent.preimage this

Openness of the Set of Continuous Linear Maps with Rank at Least $n$

Informal description

For any natural number $n$, the set of continuous linear maps $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$, whose rank (as a linear map) is at least $n$, is an open subset in the operator norm topology.

Basis.opNNNorm_le theorem

 {ι : Type*} [Fintype ι] (v : Basis ι 𝕜 E) {u : E →L[𝕜] F} (M : ℝ≥0) (hu : ∀ i, ‖u (v i)‖₊ ≤ M) :
  ‖u‖₊ ≤ Fintype.card ι • ‖v.equivFunL.toContinuousLinearMap‖₊ * M

Full source

theorem Basis.opNNNorm_le {ι : Type*} [Fintype ι] (v : Basis ι 𝕜 E) {u : E →L[𝕜] F} (M : ℝ≥0)
    (hu : ∀ i, ‖u (v i)‖₊ ≤ M) : ‖u‖₊ ≤ Fintype.card ι • ‖v.equivFunL.toContinuousLinearMap‖₊ * M :=
  u.opNNNorm_le_bound _ fun e => by
    set φ := v.equivFunL.toContinuousLinearMap
    calc
      ‖u e‖₊ = ‖u (∑ i, v.equivFun e i • v i)‖₊ := by rw [v.sum_equivFun]
      _ = ‖∑ i, v.equivFun e i • (u <| v i)‖₊ := by simp [map_sum, LinearMap.map_smul]
      _ ≤ ∑ i, ‖v.equivFun e i • (u <| v i)‖₊ := nnnorm_sum_le _ _
      _ = ∑ i, ‖v.equivFun e i‖₊ * ‖u (v i)‖₊ := by simp only [nnnorm_smul]
      _ ≤ ∑ i, ‖v.equivFun e i‖₊ * M := by gcongr; apply hu
      _ = (∑ i, ‖v.equivFun e i‖₊) * M := by rw [Finset.sum_mul]
      _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M := by
        gcongr
        calc
          ∑ i, ‖v.equivFun e i‖₊ ≤ Fintype.card ι • ‖φ e‖₊ := Pi.sum_nnnorm_apply_le_nnnorm _
          _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) := nsmul_le_nsmul_right (φ.le_opNNNorm e) _
      _ = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊ := by simp only [smul_mul_assoc, mul_right_comm]

Operator Norm Bound via Basis Vectors: $\|u\| \leq |\iota| \cdot \|v^{\text{equivFunL}}\| \cdot M$

Informal description

Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $v = (v_i)_{i \in \iota}$ be a finite basis for $E$ indexed by a finite set $\iota$. For any continuous linear map $u \colon E \to F$ and any nonnegative real number $M \geq 0$, if $\|u(v_i)\| \leq M$ for all basis vectors $v_i$, then the operator norm of $u$ satisfies \[ \|u\| \leq |\iota| \cdot \|v^{\text{equivFunL}}\| \cdot M, \] where $|\iota|$ is the cardinality of $\iota$ and $v^{\text{equivFunL}}$ is the continuous linear equivalence between $E$ and its coordinate space $\mathbb{K}^\iota$ induced by the basis $v$.

Basis.opNorm_le theorem

 {ι : Type*} [Fintype ι] (v : Basis ι 𝕜 E) {u : E →L[𝕜] F} {M : ℝ} (hM : 0 ≤ M) (hu : ∀ i, ‖u (v i)‖ ≤ M) :
  ‖u‖ ≤ Fintype.card ι • ‖v.equivFunL.toContinuousLinearMap‖ * M

Full source

theorem Basis.opNorm_le {ι : Type*} [Fintype ι] (v : Basis ι 𝕜 E) {u : E →L[𝕜] F} {M : ℝ}
    (hM : 0 ≤ M) (hu : ∀ i, ‖u (v i)‖ ≤ M) :
    ‖u‖ ≤ Fintype.card ι • ‖v.equivFunL.toContinuousLinearMap‖ * M := by
  simpa using NNReal.coe_le_coe.mpr (v.opNNNorm_le ⟨M, hM⟩ hu)

Operator Norm Bound via Basis Vectors: $\|u\| \leq |\iota| \cdot \|v^{\text{equivFunL}}\| \cdot M$

Informal description

Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $v = (v_i)_{i \in \iota}$ be a finite basis for $E$ indexed by a finite set $\iota$. For any continuous linear map $u \colon E \to F$ and any nonnegative real number $M \geq 0$, if $\|u(v_i)\| \leq M$ for all basis vectors $v_i$, then the operator norm of $u$ satisfies \[ \|u\| \leq |\iota| \cdot \|v^{\text{equivFunL}}\| \cdot M, \] where $|\iota|$ is the cardinality of $\iota$ and $v^{\text{equivFunL}}$ is the continuous linear equivalence between $E$ and its coordinate space $\mathbb{K}^\iota$ induced by the basis $v$.

Basis.exists_opNNNorm_le theorem

 {ι : Type*} [Finite ι] (v : Basis ι 𝕜 E) :
  ∃ C > (0 : ℝ≥0), ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ i, ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M

Full source

/-- A weaker version of `Basis.opNNNorm_le` that abstracts away the value of `C`. -/
theorem Basis.exists_opNNNorm_le {ι : Type*} [Finite ι] (v : Basis ι 𝕜 E) :
    ∃ C > (0 : ℝ≥0), ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ i, ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M := by
  cases nonempty_fintype ι
  exact
    ⟨max (Fintype.card ι • ‖v.equivFunL.toContinuousLinearMap‖₊) 1,
      zero_lt_one.trans_le (le_max_right _ _), fun {u} M hu =>
      (v.opNNNorm_le M hu).trans <| mul_le_mul_of_nonneg_right (le_max_left _ _) (zero_le M)⟩

Existence of Uniform Operator Norm Bound via Basis Vectors

Informal description

Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $v = (v_i)_{i \in \iota}$ be a finite basis for $E$ indexed by a finite set $\iota$. There exists a constant $C > 0$ such that for any continuous linear map $u \colon E \to F$ and any nonnegative real number $M \geq 0$, if $\|u(v_i)\| \leq M$ for all basis vectors $v_i$, then the operator norm of $u$ satisfies \[ \|u\| \leq C \cdot M. \]

Basis.exists_opNorm_le theorem

 {ι : Type*} [Finite ι] (v : Basis ι 𝕜 E) :
  ∃ C > (0 : ℝ), ∀ {u : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ i, ‖u (v i)‖ ≤ M) → ‖u‖ ≤ C * M

Full source

/-- A weaker version of `Basis.opNorm_le` that abstracts away the value of `C`. -/
theorem Basis.exists_opNorm_le {ι : Type*} [Finite ι] (v : Basis ι 𝕜 E) :
    ∃ C > (0 : ℝ), ∀ {u : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ i, ‖u (v i)‖ ≤ M) → ‖u‖ ≤ C * M := by
  obtain ⟨C, hC, h⟩ := v.exists_opNNNorm_le (F := F)
  refine ⟨C, hC, ?_⟩
  intro u M hM H
  simpa using h ⟨M, hM⟩ H

Existence of Uniform Operator Norm Bound via Basis Vectors

Informal description

Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $v = (v_i)_{i \in \iota}$ be a basis for $E$ indexed by a finite set $\iota$. There exists a constant $C > 0$ such that for any continuous linear map $u \colon E \to F$ and any nonnegative real number $M \geq 0$, if $\|u(v_i)\| \leq M$ for all basis vectors $v_i$, then the operator norm of $u$ satisfies \[ \|u\| \leq C \cdot M. \]

instSecondCountableTopologyContinuousLinearMapIdOfFiniteDimensional instance

[FiniteDimensional 𝕜 E] [SecondCountableTopology F] : SecondCountableTopology (E →L[𝕜] F)

Full source

instance [FiniteDimensional 𝕜 E] [SecondCountableTopology F] :
    SecondCountableTopology (E →L[𝕜] F) := by
  set d := Module.finrank 𝕜 E
  suffices
    ∀ ε > (0 : ℝ), ∃ n : (E →L[𝕜] F) → Fin d → ℕ, ∀ f g : E →L[𝕜] F, n f = n g → dist f g ≤ ε from
    Metric.secondCountable_of_countable_discretization fun ε ε_pos =>
      ⟨Fin d → ℕ, by infer_instance, this ε ε_pos⟩
  intro ε ε_pos
  obtain ⟨u : ℕ → F, hu : DenseRange u⟩ := exists_dense_seq F
  let v := Module.finBasis 𝕜 E
  obtain
    ⟨C : ℝ, C_pos : 0 < C, hC :
      ∀ {φ : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ i, ‖φ (v i)‖ ≤ M) → ‖φ‖ ≤ C * M⟩ :=
    v.exists_opNorm_le (E := E) (F := F)
  have h_2C : 0 < 2 * C := mul_pos zero_lt_two C_pos
  have hε2C : 0 < ε / (2 * C) := div_pos ε_pos h_2C
  have : ∀ φ : E →L[𝕜] F, ∃ n : Fin d → ℕ, ‖φ - (v.constrL <| u ∘ n)‖ ≤ ε / 2 := by
    intro φ
    have : ∀ i, ∃ n, ‖φ (v i) - u n‖ ≤ ε / (2 * C) := by
      simp only [norm_sub_rev]
      intro i
      have : φ (v i) ∈ closure (range u) := hu _
      obtain ⟨n, hn⟩ : ∃ n, ‖u n - φ (v i)‖ < ε / (2 * C) := by
        rw [mem_closure_iff_nhds_basis Metric.nhds_basis_ball] at this
        specialize this (ε / (2 * C)) hε2C
        simpa [dist_eq_norm]
      exact ⟨n, le_of_lt hn⟩
    choose n hn using this
    use n
    replace hn : ∀ i : Fin d, ‖(φ - (v.constrL <| u ∘ n)) (v i)‖ ≤ ε / (2 * C) := by simp [hn]
    have : C * (ε / (2 * C)) = ε / 2 := by
      rw [eq_div_iff (two_ne_zero : (2 : ℝ) ≠ 0), mul_comm, ← mul_assoc,
        mul_div_cancel₀ _ (ne_of_gt h_2C)]
    specialize hC (le_of_lt hε2C) hn
    rwa [this] at hC
  choose n hn using this
  set Φ := fun φ : E →L[𝕜] F => v.constrL <| u ∘ n φ
  change ∀ z, dist z (Φ z) ≤ ε / 2 at hn
  use n
  intro x y hxy
  calc
    dist x y ≤ dist x (Φ x) + dist (Φ x) y := dist_triangle _ _ _
    _ = dist x (Φ x) + dist y (Φ y) := by simp [Φ, hxy, dist_comm]
    _ ≤ ε := by linarith [hn x, hn y]

Second-Countability of Continuous Linear Maps from Finite-Dimensional Spaces

Informal description

For any finite-dimensional normed vector space $E$ over a field $\mathbb{K}$ and any second-countable topological space $F$, the space of continuous linear maps from $E$ to $F$ is second-countable.

AffineSubspace.closed_of_finiteDimensional theorem

 {P : Type*} [MetricSpace P] [NormedAddTorsor E P] (s : AffineSubspace 𝕜 P) [FiniteDimensional 𝕜 s.direction] :
  IsClosed (s : Set P)

Full source

theorem AffineSubspace.closed_of_finiteDimensional {P : Type*} [MetricSpace P]
    [NormedAddTorsor E P] (s : AffineSubspace 𝕜 P) [FiniteDimensional 𝕜 s.direction] :
    IsClosed (s : Set P) :=
  s.isClosed_direction_iff.mp s.direction.closed_of_finiteDimensional

Closedness of Finite-Dimensional Affine Subspaces in Metric Spaces

Informal description

Let $P$ be a metric space with a normed additive torsor structure over a normed space $E$, and let $s$ be an affine subspace of $P$. If the direction vector space of $s$ is finite-dimensional over the field $\mathbb{K}$, then $s$ is a closed subset of $P$.

exists_norm_le_le_norm_sub_of_finset theorem

 {c : 𝕜} (hc : 1 < ‖c‖) {R : ℝ} (hR : ‖c‖ < R) (h : ¬FiniteDimensional 𝕜 E) (s : Finset E) :
  ∃ x : E, ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖

Full source

/-- 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_norm_le_le_norm_sub_of_finset {c : 𝕜} (hc : 1 < ‖c‖) {R : ℝ} (hR : ‖c‖ < R)
    (h : ¬FiniteDimensional 𝕜 E) (s : Finset E) : ∃ x : E, ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖ := by
  let F := Submodule.span 𝕜 (s : Set E)
  haveI : FiniteDimensional 𝕜 F :=
    Module.finite_def.2
      ((Submodule.fg_top _).2 (Submodule.fg_def.2 ⟨s, Finset.finite_toSet _, rfl⟩))
  have Fclosed : IsClosed (F : Set E) := Submodule.closed_of_finiteDimensional _
  have : ∃ x, x ∉ F := by
    contrapose! h
    have : (⊤ : Submodule 𝕜 E) = F := by
      ext x
      simp [h]
    have : FiniteDimensional 𝕜 (⊤ : Submodule 𝕜 E) := by rwa [this]
    exact Module.finite_def.2 ((Submodule.fg_top _).1 (Module.finite_def.1 this))
  obtain ⟨x, xR, hx⟩ : ∃ x : E, ‖x‖ ≤ R ∧ ∀ y : E, y ∈ F → 1 ≤ ‖x - y‖ :=
    riesz_lemma_of_norm_lt hc hR Fclosed this
  have hx' : ∀ y : E, y ∈ F → 1 ≤ ‖y - x‖ := by
    intro y hy
    rw [← norm_neg]
    simpa using hx y hy
  exact ⟨x, xR, fun y hy => hx' _ (Submodule.subset_span hy)⟩

Existence of Unit-Distant Vector from Finite Sets in Infinite-Dimensional Spaces

Informal description

Let $\mathbb{K}$ be a nontrivially normed field with an element $c$ such that $\|c\| > 1$, and let $E$ be an infinite-dimensional normed space over $\mathbb{K}$. For any real number $R > \|c\|$ and any finite set $s \subset E$, there exists a vector $x \in E$ such that $\|x\| \leq R$ and for every $y \in s$, the distance satisfies $\|y - x\| \geq 1$.

exists_seq_norm_le_one_le_norm_sub' theorem

 {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‖

Full source

/-- 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' {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‖ := by
  have : IsSymm E fun x y : E => 1 ≤ ‖x - y‖ := by
    constructor
    intro x y hxy
    rw [← norm_neg]
    simpa
  apply
    exists_seq_of_forall_finset_exists' (fun x : E => ‖x‖ ≤ R) fun (x : E) (y : E) => 1 ≤ ‖x - y‖
  rintro s -
  exact exists_norm_le_le_norm_sub_of_finset hc hR h s

Existence of Bounded, Unit-Distant Sequence in Infinite-Dimensional Normed Spaces

Informal description

Let $\mathbb{K}$ be a nontrivially normed field with an element $c$ such that $\|c\| > 1$, and let $E$ be an infinite-dimensional normed space over $\mathbb{K}$. For any real number $R > \|c\|$, there exists a sequence $(f_n)_{n \in \mathbb{N}}$ in $E$ such that $\|f_n\| \leq R$ for all $n \in \mathbb{N}$ and $\|f_m - f_n\| \geq 1$ for all distinct $m, n \in \mathbb{N}$.

exists_seq_norm_le_one_le_norm_sub theorem

 (h : ¬FiniteDimensional 𝕜 E) : ∃ (R : ℝ) (f : ℕ → E), 1 < R ∧ (∀ n, ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖

Full source

theorem exists_seq_norm_le_one_le_norm_sub (h : ¬FiniteDimensional 𝕜 E) :
    ∃ (R : ℝ) (f : ℕ → E), 1 < R ∧ (∀ n, ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖ := by
  obtain ⟨c, hc⟩ : ∃ c : 𝕜, 1 < ‖c‖ := NormedField.exists_one_lt_norm 𝕜
  have A : ‖c‖ < ‖c‖ + 1 := by linarith
  rcases exists_seq_norm_le_one_le_norm_sub' hc A h with ⟨f, hf⟩
  exact ⟨‖c‖ + 1, f, hc.trans A, hf.1, hf.2⟩

Existence of Bounded, Unit-Distant Sequence in Infinite-Dimensional Normed Spaces

Informal description

Let $E$ be an infinite-dimensional normed space over a field $\mathbb{K}$. Then there exists a real number $R > 1$ and a sequence $(f_n)_{n \in \mathbb{N}}$ in $E$ such that $\|f_n\| \leq R$ for all $n \in \mathbb{N}$ and $\|f_m - f_n\| \geq 1$ for all distinct $m, n \in \mathbb{N}$.

FiniteDimensional.of_isCompact_closedBall₀ theorem

{r : ℝ} (rpos : 0 < r) (h : IsCompact (Metric.closedBall (0 : E) r)) : FiniteDimensional 𝕜 E

Full source

/-- **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₀ {r : ℝ} (rpos : 0 < r)
    (h : IsCompact (Metric.closedBall (0 : E) r)) : FiniteDimensional 𝕜 E := by
  by_contra hfin
  obtain ⟨R, f, Rgt, fle, lef⟩ :
    ∃ (R : ℝ) (f : ℕ → E), 1 < R ∧ (∀ n, ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖ :=
    exists_seq_norm_le_one_le_norm_sub hfin
  have rRpos : 0 < r / R := div_pos rpos (zero_lt_one.trans Rgt)
  obtain ⟨c, hc⟩ : ∃ c : 𝕜, 0 < ‖c‖ ∧ ‖c‖ < r / R := NormedField.exists_norm_lt _ rRpos
  let g := fun n : ℕ => c • f n
  have A : ∀ n, g n ∈ Metric.closedBall (0 : E) r := by
    intro n
    simp only [g, norm_smul, dist_zero_right, Metric.mem_closedBall]
    calc
      ‖c‖ * ‖f n‖ ≤ r / R * R := by
        gcongr
        · exact hc.2.le
        · apply fle
      _ = r := by field_simp [(zero_lt_one.trans Rgt).ne']
  obtain ⟨x : E, _ : x ∈ Metric.closedBall (0 : E) r, φ : ℕ → ℕ, φmono : StrictMono φ,
    φlim : Tendsto (g ∘ φ) atTop (𝓝 x)⟩ := h.tendsto_subseq A
  have B : CauchySeq (g ∘ φ) := φlim.cauchySeq
  obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ n : ℕ, N ≤ n → dist ((g ∘ φ) n) ((g ∘ φ) N) < ‖c‖ :=
    Metric.cauchySeq_iff'.1 B ‖c‖ hc.1
  apply lt_irrefl ‖c‖
  calc
    ‖c‖ ≤ dist (g (φ (N + 1))) (g (φ N)) := by
      conv_lhs => rw [← mul_one ‖c‖]
      simp only [g, dist_eq_norm, ← smul_sub, norm_smul]
      gcongr
      apply lef (ne_of_gt _)
      exact φmono (Nat.lt_succ_self N)
    _ < ‖c‖ := hN (N + 1) (Nat.le_succ N)

Riesz's Theorem: Compactness of Closed Ball Implies Finite-Dimensionality

Informal description

Let $E$ be a normed vector space over a field $\mathbb{K}$ and let $r > 0$ be a positive real number. If the closed ball $\overline{B}(0, r)$ centered at the origin with radius $r$ is compact, then $E$ is finite-dimensional over $\mathbb{K}$.

FiniteDimensional.of_isCompact_closedBall theorem

{r : ℝ} (rpos : 0 < r) {c : E} (h : IsCompact (Metric.closedBall c r)) : FiniteDimensional 𝕜 E

Full source

/-- **Riesz's theorem**: if a closed ball of positive radius is compact in a vector space, then the
space is finite-dimensional. -/
theorem FiniteDimensional.of_isCompact_closedBall {r : ℝ} (rpos : 0 < r) {c : E}
    (h : IsCompact (Metric.closedBall c r)) : FiniteDimensional 𝕜 E :=
  .of_isCompact_closedBall₀ 𝕜 rpos <| by simpa using h.vadd (-c)

Riesz's Theorem: Compactness of Closed Ball Implies Finite-Dimensionality (General Case)

Informal description

Let $E$ be a normed vector space over a field $\mathbb{K}$ and let $r > 0$ be a positive real number. For any point $c \in E$, if the closed ball $\overline{B}(c, r)$ centered at $c$ with radius $r$ is compact, then $E$ is finite-dimensional over $\mathbb{K}$.

FiniteDimensional.of_locallyCompactSpace theorem

[LocallyCompactSpace E] : FiniteDimensional 𝕜 E

Full source

/-- **Riesz's theorem**: a locally compact normed vector space is finite-dimensional. -/
theorem FiniteDimensional.of_locallyCompactSpace [LocallyCompactSpace E] :
    FiniteDimensional 𝕜 E :=
  let ⟨_r, rpos, hr⟩ := exists_isCompact_closedBall (0 : E)
  .of_isCompact_closedBall₀ 𝕜 rpos hr

Riesz's Theorem: Locally Compact Normed Spaces are Finite-Dimensional

Informal description

If a normed vector space $E$ over a field $\mathbb{K}$ is locally compact, then $E$ is finite-dimensional over $\mathbb{K}$.

ProperSpace.of_locallyCompactSpace theorem

 (𝕜 : Type*) [NontriviallyNormedField 𝕜] {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
  [LocallyCompactSpace E] : ProperSpace E

Full source

/-- A locally compact normed vector space is proper. -/
lemma ProperSpace.of_locallyCompactSpace (𝕜 : Type*) [NontriviallyNormedField 𝕜]
    {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [LocallyCompactSpace E] :
    ProperSpace E := by
  rcases exists_isCompact_closedBall (0 : E) with ⟨r, rpos, hr⟩
  rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
  have hC : ∀ n, IsCompact (closedBall (0 : E) (‖c‖^n * r)) := fun n ↦ by
    have : c ^ n ≠ 0 := pow_ne_zero _ <| fun h ↦ by simp [h, zero_le_one.not_lt] at hc
    simpa [_root_.smul_closedBall' this] using hr.smul (c ^ n)
  have hTop : Tendsto (fun n ↦ ‖c‖^n * r) atTop atTop :=
    Tendsto.atTop_mul_const rpos (tendsto_pow_atTop_atTop_of_one_lt hc)
  exact .of_seq_closedBall hTop (Eventually.of_forall hC)

Locally Compact Normed Spaces are Proper

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $E$ be a seminormed additive commutative group equipped with a normed space structure over $\mathbb{K}$. If $E$ is locally compact, then $E$ is a proper space (i.e., all closed balls in $E$ are compact).

ProperSpace.of_locallyCompact_module theorem

[Nontrivial E] [LocallyCompactSpace E] : ProperSpace 𝕜

Full source

lemma ProperSpace.of_locallyCompact_module [Nontrivial E] [LocallyCompactSpace E] :
    ProperSpace 𝕜 :=
  have : LocallyCompactSpace 𝕜 := by
    obtain ⟨v, hv⟩ : ∃ v : E, v ≠ 0 := exists_ne 0
    let L : 𝕜 → E := fun t ↦ t • v
    have : IsClosedEmbedding L := isClosedEmbedding_smul_left hv
    apply IsClosedEmbedding.locallyCompactSpace this
  .of_locallyCompactSpace 𝕜

Properness of the Field from Local Compactness of a Nontrivial Normed Space

Informal description

Let $\mathbb{K}$ be a nontrivially normed field and $E$ be a nontrivial normed space over $\mathbb{K}$. If $E$ is locally compact, then $\mathbb{K}$ is a proper space (i.e., all closed balls in $\mathbb{K}$ are compact).

ContinuousLinearEquiv.piRing definition

(ι : Type*) [Fintype ι] [DecidableEq ι] : ((ι → 𝕜) →L[𝕜] E) ≃L[𝕜] ι → E

Full source

/-- 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. -/
def ContinuousLinearEquiv.piRing (ι : Type*) [Fintype ι] [DecidableEq ι] :
    ((ι → 𝕜) →L[𝕜] E) ≃L[𝕜] ι → E :=
  { LinearMap.toContinuousLinearMap.symm.trans (LinearEquiv.piRing 𝕜 E ι 𝕜) with
    continuous_toFun := by
      refine continuous_pi fun i => ?_
      exact (ContinuousLinearMap.apply 𝕜 E (Pi.single i 1)).continuous
    continuous_invFun := by
      simp_rw [LinearEquiv.invFun_eq_symm, LinearEquiv.trans_symm, LinearEquiv.symm_symm]
      -- Note: added explicit type and removed `change` that tried to achieve the same
      refine AddMonoidHomClass.continuous_of_bound
        (LinearMap.toContinuousLinearMap.toLinearMap.comp
            (LinearEquiv.piRing 𝕜 E ι 𝕜).symm.toLinearMap)
        (Fintype.card ι : ℝ) fun g => ?_
      rw [← nsmul_eq_mul]
      refine opNorm_le_bound _ (nsmul_nonneg (norm_nonneg g) (Fintype.card ι)) fun t => ?_
      simp_rw [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_apply,
        LinearMap.coe_toContinuousLinearMap', LinearEquiv.piRing_symm_apply]
      apply le_trans (norm_sum_le _ _)
      rw [smul_mul_assoc]
      refine Finset.sum_le_card_nsmul _ _ _ fun i _ => ?_
      rw [norm_smul, mul_comm]
      gcongr <;> apply norm_le_pi_norm }

Continuous linear equivalence between function spaces $\mathcal{L}(\mathbb{K}^\iota, E)$ and $E^\iota$

Informal description

Given a finite index set $\iota$, a nontrivially normed field $\mathbb{K}$, and a normed space $E$ over $\mathbb{K}$, there is a continuous linear equivalence between the space of continuous linear maps from $\iota \to \mathbb{K}$ to $E$ and the space of functions $\iota \to E$. Specifically: - The forward map takes a continuous linear map $f : (\iota \to \mathbb{K}) \to E$ to the function $\lambda i, f(\text{single}_i(1))$, where $\text{single}_i(1)$ is the function that is $1$ at $i$ and $0$ elsewhere. - The inverse map takes a function $g : \iota \to E$ to the continuous linear map $\lambda h, \sum_{i} h(i) \cdot g(i)$.

continuousOn_clm_apply theorem

 {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E] {f : X → E →L[𝕜] F} {s : Set X} :
  ContinuousOn f s ↔ ∀ y, ContinuousOn (fun x => f x y) s

Full source

/-- A family of continuous linear maps is continuous on `s` if all its applications are. -/
theorem continuousOn_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]
    {f : X → E →L[𝕜] F} {s : Set X} : ContinuousOnContinuousOn f s ↔ ∀ y, ContinuousOn (fun x => f x y) s := by
  refine ⟨fun h y => (ContinuousLinearMap.apply 𝕜 F y).continuous.comp_continuousOn h, fun h => ?_⟩
  let d := finrank 𝕜 E
  have hd : d = finrank 𝕜 (Fin d → 𝕜) := (finrank_fin_fun 𝕜).symm
  let e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq hd
  let e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F :=
    (e₁.arrowCongr (1 : F ≃L[𝕜] F)).trans (ContinuousLinearEquiv.piRing (Fin d))
  rw [← f.id_comp, ← e₂.symm_comp_self]
  exact e₂.symm.continuous.comp_continuousOn (continuousOn_pi.mpr fun i => h _)

Componentwise Continuity Criterion for Continuous Linear Maps on Finite-Dimensional Domains

Informal description

Let $X$ be a topological space, $\mathbb{K}$ a nontrivially normed field, $E$ a finite-dimensional vector space over $\mathbb{K}$, and $F$ a normed space over $\mathbb{K}$. For a function $f \colon X \to \mathcal{L}(E, F)$ (where $\mathcal{L}(E, F)$ denotes the space of continuous linear maps from $E$ to $F$) and a subset $s \subseteq X$, the following are equivalent: 1. $f$ is continuous on $s$. 2. For every $y \in E$, the function $x \mapsto f(x)(y)$ is continuous on $s$.

continuous_clm_apply theorem

 {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E] {f : X → E →L[𝕜] F} : Continuous f ↔ ∀ y, Continuous (f · y)

Full source

theorem continuous_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]
    {f : X → E →L[𝕜] F} : ContinuousContinuous f ↔ ∀ y, Continuous (f · y) := by
  simp_rw [continuous_iff_continuousOn_univ, continuousOn_clm_apply]

Continuity of a Family of Continuous Linear Maps in Finite Dimensions

Informal description

Let $X$ be a topological space, $E$ a finite-dimensional vector space over a field $\mathbb{K}$, and $F$ a normed space over $\mathbb{K}$. For a function $f \colon X \to \mathcal{L}(E, F)$ (where $\mathcal{L}(E, F)$ denotes the space of continuous linear maps from $E$ to $F$), the following are equivalent: 1. $f$ is continuous. 2. For every $y \in E$, the function $x \mapsto f(x)(y)$ is continuous.

FiniteDimensional.proper theorem

[FiniteDimensional 𝕜 E] : ProperSpace E

Full source

/-- 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. -/
theorem FiniteDimensional.proper [FiniteDimensional 𝕜 E] : ProperSpace E := by
  have : ProperSpace 𝕜 := .of_locallyCompactSpace 𝕜
  set e := ContinuousLinearEquiv.ofFinrankEq (@finrank_fin_fun 𝕜 _ _ (finrank 𝕜 E)).symm
  exact e.symm.antilipschitz.properSpace e.symm.continuous e.symm.surjective

Finite-dimensional vector spaces over locally compact fields are proper

Informal description

Let $\mathbb{K}$ be a locally compact field and $E$ be a finite-dimensional vector space over $\mathbb{K}$. Then $E$ is a proper space, meaning that all closed balls in $E$ are compact.

FiniteDimensional.proper_real instance

(E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : ProperSpace E

Full source

instance (priority := 900) FiniteDimensional.proper_real (E : Type u) [NormedAddCommGroup E]
    [NormedSpace ℝ E] [FiniteDimensional ℝ E] : ProperSpace E :=
  FiniteDimensional.proper ℝ E

Properness of Finite-Dimensional Real Normed Spaces

Informal description

Every finite-dimensional real normed vector space $E$ is proper, meaning that all closed balls in $E$ are compact.

instProperSpaceSubtypeMemSubmoduleOfCompleteSpaceOfLocallyCompactSpace instance

 {𝕜 E : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [LocallyCompactSpace E] (S : Submodule 𝕜 E) : ProperSpace S

Full source

/-- A submodule of a locally compact space over a complete field is also locally compact (and even
proper). -/
instance {𝕜 E : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [LocallyCompactSpace E] (S : Submodule 𝕜 E) :
    ProperSpace S := by
  nontriviality E
  have : ProperSpace 𝕜 := .of_locallyCompact_module 𝕜 E
  have : FiniteDimensional 𝕜 E := .of_locallyCompactSpace 𝕜
  exact FiniteDimensional.proper 𝕜 S

Properness of Submodules in Locally Compact Normed Spaces over Complete Fields

Informal description

For any nontrivially normed field $\mathbb{K}$ that is complete, any normed vector space $E$ over $\mathbb{K}$ that is locally compact, and any submodule $S$ of $E$, the subspace $S$ is a proper space (i.e., all closed balls in $S$ are compact).

exists_mem_frontier_infDist_compl_eq_dist theorem

 {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {x : E} {s : Set E} (hx : x ∈ s)
  (hs : s ≠ univ) : ∃ y ∈ frontier s, Metric.infDist x sᶜ = dist x y

Full source

/-- 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 exists_mem_frontier_infDist_compl_eq_dist {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [FiniteDimensional ℝ E] {x : E} {s : Set E} (hx : x ∈ s) (hs : s ≠ univ) :
    ∃ y ∈ frontier s, Metric.infDist x sᶜ = dist x y := by
  rcases Metric.exists_mem_closure_infDist_eq_dist (nonempty_compl.2 hs) x with ⟨y, hys, hyd⟩
  rw [closure_compl] at hys
  refine ⟨y, ⟨Metric.closedBall_infDist_compl_subset_closure hx <|
    Metric.mem_closedBall.2 <| ge_of_eq ?_, hys⟩, hyd⟩
  rwa [dist_comm]

Existence of Frontier Point Achieving Minimal Distance to Complement in Finite-Dimensional Spaces

Informal description

Let $E$ be a finite-dimensional real normed vector space, $x \in E$ a point, and $s \subseteq E$ a neighborhood of $x$ such that $s \neq E$. Then there exists a point $y$ in the frontier (boundary) of $s$ such that the infimum distance from $x$ to the complement of $s$ equals the distance between $x$ and $y$, i.e., \[ \inf_{z \in s^c} d(x, z) = d(x, y). \]

IsCompact.exists_mem_frontier_infDist_compl_eq_dist theorem

 {E : Type*} [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

Full source

/-- 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`. -/
nonrec theorem IsCompact.exists_mem_frontier_infDist_compl_eq_dist {E : Type*}
    [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 := by
  obtain hx' | hx' : x ∈ interior K ∪ frontier K := by
    rw [← closure_eq_interior_union_frontier]
    exact subset_closure hx
  · rw [mem_interior_iff_mem_nhds, Metric.nhds_basis_closedBall.mem_iff] at hx'
    rcases hx' with ⟨r, hr₀, hrK⟩
    have : FiniteDimensional ℝ E :=
      .of_isCompact_closedBall ℝ hr₀
        (hK.of_isClosed_subset Metric.isClosed_closedBall hrK)
    exact exists_mem_frontier_infDist_compl_eq_dist hx hK.ne_univ
  · refine ⟨x, hx', ?_⟩
    rw [frontier_eq_closure_inter_closure] at hx'
    rw [Metric.infDist_zero_of_mem_closure hx'.2, dist_self]

Existence of Boundary Point Achieving Minimal Distance to Complement in Compact Sets

Informal description

Let $E$ be a nontrivial real normed vector space, $K \subseteq E$ a compact set, and $x \in K$ a point. Then there exists a point $y$ in the frontier (boundary) of $K$ such that the infimum distance from $x$ to the complement of $K$ equals the distance between $x$ and $y$, i.e., \[ \inf_{z \in K^c} d(x, z) = d(x, y). \]

summable_norm_iff theorem

 {α E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : α → E} :
  (Summable fun x => ‖f x‖) ↔ Summable f

Full source

/-- 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_iff {α E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] {f : α → E} : (Summable fun x => ‖f x‖) ↔ Summable f := by
  refine ⟨Summable.of_norm, fun hf ↦ ?_⟩
  -- First we use a finite basis to reduce the problem to the case `E = Fin N → ℝ`
  suffices ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x => ‖g x‖ by
    obtain v := Module.finBasis ℝ E
    set e := v.equivFunL
    have H : Summable fun x => ‖e (f x)‖ := this (e.summable.2 hf)
    refine .of_norm_bounded _ (H.mul_left ↑‖(e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊) fun i ↦ ?_
    simpa using (e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E).le_opNorm (e <| f i)
  clear! E
  -- Now we deal with `g : α → Fin N → ℝ`
  intro N g hg
  have : ∀ i, Summable fun x => ‖g x i‖ := fun i => (Pi.summable.1 hg i).abs
  refine .of_norm_bounded _ (summable_sum fun i (_ : i ∈ Finset.univ) => this i) fun x => ?_
  rw [norm_norm, pi_norm_le_iff_of_nonneg]
  · refine fun i => Finset.single_le_sum (f := fun i => ‖g x i‖) (fun i _ => ?_) (Finset.mem_univ i)
    exact norm_nonneg (g x i)
  · exact Finset.sum_nonneg fun _ _ => norm_nonneg _

Summability Equivalence: $\sum \|f(x)\|$ Converges iff $\sum f(x)$ Converges in Finite Dimensions

Informal description

For a finite-dimensional real normed vector space $E$ and a function $f \colon \alpha \to E$, the series $\sum_{x} \|f(x)\|$ is summable if and only if the series $\sum_{x} f(x)$ is summable.

summable_of_sum_range_norm_le theorem

 {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {c : ℝ} {f : ℕ → E}
  (h : ∀ n, ∑ i ∈ Finset.range n, ‖f i‖ ≤ c) : Summable f

Full source

theorem summable_of_sum_range_norm_le {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] {c : ℝ} {f : ℕ → E} (h : ∀ n, ∑ i ∈ Finset.range n, ‖f i‖ ≤ c) :
    Summable f :=
  summable_norm_iff.mp <| summable_of_sum_range_le (fun _ ↦ norm_nonneg _)  h

Summability from Bounded Partial Norm Sums in Finite Dimensions

Informal description

Let $E$ be a finite-dimensional real normed vector space, and let $f \colon \mathbb{N} \to E$ be a sequence of vectors in $E$. If there exists a constant $c \in \mathbb{R}$ such that for every $n \in \mathbb{N}$, the partial sum $\sum_{i=0}^{n-1} \|f(i)\|$ is bounded by $c$, then the series $\sum_{i=0}^\infty f(i)$ is summable in $E$.

summable_of_isBigO' theorem

 {ι E F : Type*} [NormedAddCommGroup E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F]
  [FiniteDimensional ℝ F] {f : ι → E} {g : ι → F} (hg : Summable g) (h : f =O[cofinite] g) : Summable f

Full source

theorem summable_of_isBigO' {ι E F : Type*} [NormedAddCommGroup E] [CompleteSpace E]
    [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : ι → E} {g : ι → F}
    (hg : Summable g) (h : f =O[cofinite] g) : Summable f :=
  summable_of_isBigO hg.norm h.norm_right

Summability from Big-O Condition Relative to Cofinite Filter

Informal description

Let $E$ be a complete normed additive commutative group, $F$ a finite-dimensional real normed vector space, and $f \colon \iota \to E$, $g \colon \iota \to F$ functions. If $g$ is summable and $f$ is big-O of $g$ with respect to the cofinite filter (i.e., there exist constants $C, N$ such that for all but finitely many $i \in \iota$, $\|f(i)\| \leq C \|g(i)\|$), then $f$ is summable.

Asymptotics.IsBigO.comp_summable theorem

 {ι E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F]
  [CompleteSpace F] {f : E → F} (hf : f =O[𝓝 0] id) {g : ι → E} (hg : Summable g) : Summable (f ∘ g)

Full source

lemma Asymptotics.IsBigO.comp_summable {ι E F : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    [NormedAddCommGroup F] [CompleteSpace F]
    {f : E → F} (hf : f =O[𝓝 0] id) {g : ι → E} (hg : Summable g) : Summable (f ∘ g) :=
  .of_norm <| hf.comp_summable_norm hg.norm

Summability of Big-O Composition with Summable Sequence

Informal description

Let $E$ and $F$ be normed additive commutative groups over $\mathbb{R}$, with $E$ finite-dimensional and $F$ complete. Given a function $f \colon E \to F$ that is big-O of the identity function near $0$ (i.e., $\|f(x)\| \leq C\|x\|$ for some $C > 0$ and all $x$ in a neighborhood of $0$), and a summable sequence $g \colon \iota \to E$, the composition $f \circ g \colon \iota \to F$ is also summable.

summable_of_isBigO_nat' theorem

 {E F : Type*} [NormedAddCommGroup E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F]
  {f : ℕ → E} {g : ℕ → F} (hg : Summable g) (h : f =O[atTop] g) : Summable f

Full source

theorem summable_of_isBigO_nat' {E F : Type*} [NormedAddCommGroup E] [CompleteSpace E]
    [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : ℕ → E} {g : ℕ → F}
    (hg : Summable g) (h : f =O[atTop] g) : Summable f :=
  summable_of_isBigO_nat hg.norm h.norm_right

Summability from Big-O Condition on Sequences in Complete and Finite-Dimensional Spaces

Informal description

Let $E$ and $F$ be normed additive commutative groups, where $E$ is complete and $F$ is a finite-dimensional normed space over $\mathbb{R}$. Given sequences $f: \mathbb{N} \to E$ and $g: \mathbb{N} \to F$, if $g$ is summable and $f$ is big-O of $g$ at infinity (i.e., there exists $C > 0$ and $N \in \mathbb{N}$ such that $\|f(n)\| \leq C\|g(n)\|$ for all $n \geq N$), then $f$ is summable.

summable_of_isEquivalent theorem

 {ι E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : ι → E} {g : ι → E}
  (hg : Summable g) (h : f ~[cofinite] g) : Summable f

Full source

theorem summable_of_isEquivalent {ι E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] {f : ι → E} {g : ι → E} (hg : Summable g) (h : f ~[cofinite] g) :
    Summable f :=
  hg.trans_sub (summable_of_isBigO' hg h.isLittleO.isBigO)

Summability of Asymptotically Equivalent Functions in Finite-Dimensional Spaces

Informal description

Let $E$ be a finite-dimensional real normed vector space, and let $f, g \colon \iota \to E$ be functions. If $g$ is summable and $f$ is asymptotically equivalent to $g$ with respect to the cofinite filter (i.e., $\lim_{i \to \infty} \frac{\|f(i) - g(i)\|}{\|g(i)\|} = 0$ and $g(i) \neq 0$ for all but finitely many $i$), then $f$ is summable.

summable_of_isEquivalent_nat theorem

 {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : ℕ → E} {g : ℕ → E} (hg : Summable g)
  (h : f ~[atTop] g) : Summable f

Full source

theorem summable_of_isEquivalent_nat {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] {f : ℕ → E} {g : ℕ → E} (hg : Summable g) (h : f ~[atTop] g) :
    Summable f :=
  hg.trans_sub (summable_of_isBigO_nat' hg h.isLittleO.isBigO)

Summability of Asymptotically Equivalent Sequences in Finite-Dimensional Real Normed Spaces

Informal description

Let $E$ be a finite-dimensional real normed vector space, and let $f, g : \mathbb{N} \to E$ be sequences. If $g$ is summable and $f$ is asymptotically equivalent to $g$ at infinity (i.e., $\lim_{n \to \infty} \frac{\|f(n) - g(n)\|}{\|g(n)\|} = 0$), then $f$ is summable.

IsEquivalent.summable_iff theorem

 {ι E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : ι → E} {g : ι → E}
  (h : f ~[cofinite] g) : Summable f ↔ Summable g

Full source

theorem IsEquivalent.summable_iff {ι E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] {f : ι → E} {g : ι → E} (h : f ~[cofinite] g) :
    SummableSummable f ↔ Summable g :=
  ⟨fun hf => summable_of_isEquivalent hf h.symm, fun hg => summable_of_isEquivalent hg h⟩

Summability Criterion for Asymptotically Equivalent Functions in Finite-Dimensional Spaces

Informal description

Let $E$ be a finite-dimensional real normed vector space, and let $f, g \colon \iota \to E$ be functions. If $f$ is asymptotically equivalent to $g$ with respect to the cofinite filter (i.e., $\lim_{i \to \infty} \frac{\|f(i) - g(i)\|}{\|g(i)\|} = 0$ and $g(i) \neq 0$ for all but finitely many $i$), then $f$ is summable if and only if $g$ is summable.

IsEquivalent.summable_iff_nat theorem

 {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : ℕ → E} {g : ℕ → E}
  (h : f ~[atTop] g) : Summable f ↔ Summable g

Full source

theorem IsEquivalent.summable_iff_nat {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] {f : ℕ → E} {g : ℕ → E} (h : f ~[atTop] g) : SummableSummable f ↔ Summable g :=
  ⟨fun hf => summable_of_isEquivalent_nat hf h.symm, fun hg => summable_of_isEquivalent_nat hg h⟩

Summability Equivalence for Asymptotically Equivalent Sequences in Finite-Dimensional Spaces

Informal description

Let $E$ be a finite-dimensional real normed vector space, and let $f, g \colon \mathbb{N} \to E$ be sequences. If $f$ is asymptotically equivalent to $g$ at infinity (i.e., $\lim_{n \to \infty} \frac{\|f(n) - g(n)\|}{\|g(n)\|} = 0$), then $f$ is summable if and only if $g$ is summable.

Mathlib.Analysis.Normed.Module.FiniteDimension

Main results:

Implementation notes