Operators on complete normed spaces #

This file contains statements about norms of operators on complete normed spaces, such as a version of the Banach-Alaoglu theorem (ContinuousLinearMap.isCompact_image_coe_closedBall).

source

noncomputable def ContinuousLinearMap.ofMemClosureImageCoeBounded {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] (f : E' → F) {s : Set (E' →SL[σ₁₂] F)} (hs : Bornology.IsBounded s) (hf : f ∈ closure (DFunLike.coe '' s)) :

E' →SL[σ₁₂] F

Construct a bundled continuous (semi)linear map from a map f : E → F and a proof of the fact that it belongs to the closure of the image of a bounded set s : Set (E →SL[σ₁₂] F) under coercion to function. Coercion to function of the result is definitionally equal to f.

Equations

ContinuousLinearMap.ofMemClosureImageCoeBounded f hs hf = LinearMap.mkContinuousOfExistsBound (linearMapOfMemClosureRangeCoe f ⋯) ⋯

Instances For

source

@[simp]

theorem ContinuousLinearMap.ofMemClosureImageCoeBounded_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] (f : E' → F) {s : Set (E' →SL[σ₁₂] F)} (hs : Bornology.IsBounded s) (hf : f ∈ closure (DFunLike.coe '' s)) :

⇑(ContinuousLinearMap.ofMemClosureImageCoeBounded f hs hf) = f

source

noncomputable def ContinuousLinearMap.ofTendstoOfBoundedRange {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] {α : Type u_12} {l : Filter α} [Filter.NeBot l] (f : E' → F) (g : α → E' →SL[σ₁₂] F) (hf : Filter.Tendsto (fun (a : α) (x : E') => (g a) x) l (nhds f)) (hg : Bornology.IsBounded (Set.range g)) :

E' →SL[σ₁₂] F

Let f : E → F be a map, let g : α → E →SL[σ₁₂] F be a family of continuous (semi)linear maps that takes values in a bounded set and converges to f pointwise along a nontrivial filter. Then f is a continuous (semi)linear map.

Equations

ContinuousLinearMap.ofTendstoOfBoundedRange f g hf hg = ContinuousLinearMap.ofMemClosureImageCoeBounded f hg ⋯

Instances For

source

@[simp]

theorem ContinuousLinearMap.ofTendstoOfBoundedRange_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] {α : Type u_12} {l : Filter α} [Filter.NeBot l] (f : E' → F) (g : α → E' →SL[σ₁₂] F) (hf : Filter.Tendsto (fun (a : α) (x : E') => (g a) x) l (nhds f)) (hg : Bornology.IsBounded (Set.range g)) :

⇑(ContinuousLinearMap.ofTendstoOfBoundedRange f g hf hg) = f

source

theorem ContinuousLinearMap.tendsto_of_tendsto_pointwise_of_cauchySeq {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] {f : ℕ → E' →SL[σ₁₂] F} {g : E' →SL[σ₁₂] F} (hg : Filter.Tendsto (fun (n : ℕ) (x : E') => (f n) x) Filter.atTop (nhds ⇑g)) (hf : CauchySeq f) :

Filter.Tendsto f Filter.atTop (nhds g)

If a Cauchy sequence of continuous linear map converges to a continuous linear map pointwise, then it converges to the same map in norm. This lemma is used to prove that the space of continuous linear maps is complete provided that the codomain is a complete space.

source

noncomputable instance ContinuousLinearMap.instCompleteSpaceContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToAddCommMonoidToAddCommGroupToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupToAddCommMonoidToAddCommGroupToModuleToModuleUniformSpaceToAddCommGroupTo_uniformAddGroup {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] [CompleteSpace F] :

CompleteSpace (E' →SL[σ₁₂] F)

If the target space is complete, the space of continuous linear maps with its norm is also complete. This works also if the source space is seminormed.

Equations

⋯ = ⋯

source

theorem ContinuousLinearMap.isCompact_closure_image_coe_of_bounded {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] [ProperSpace F] {s : Set (E' →SL[σ₁₂] F)} (hb : Bornology.IsBounded s) :

IsCompact (closure (DFunLike.coe '' s))

Let s be a bounded set in the space of continuous (semi)linear maps E →SL[σ] F taking values in a proper space. Then s interpreted as a set in the space of maps E → F with topology of pointwise convergence is precompact: its closure is a compact set.

source

theorem ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] [ProperSpace F] {s : Set (E' →SL[σ₁₂] F)} (hb : Bornology.IsBounded s) (hc : IsClosed (DFunLike.coe '' s)) :

IsCompact (DFunLike.coe '' s)

Let s be a bounded set in the space of continuous (semi)linear maps E →SL[σ] F taking values in a proper space. If s interpreted as a set in the space of maps E → F with topology of pointwise convergence is closed, then it is compact.

TODO: reformulate this in terms of a type synonym with the right topology.

source

theorem ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] {s : Set (E' →SL[σ₁₂] F)} (hb : Bornology.IsBounded s) (hc : ∀ (f : E' →SL[σ₁₂] F), ⇑f ∈ closure (DFunLike.coe '' s) → f ∈ s) :

IsClosed (DFunLike.coe '' s)

If a set s of semilinear functions is bounded and is closed in the weak-* topology, then its image under coercion to functions E → F is a closed set. We don't have a name for E →SL[σ] F with weak-* topology in mathlib, so we use an equivalent condition (see isClosed_induced_iff').

TODO: reformulate this in terms of a type synonym with the right topology.

source

theorem ContinuousLinearMap.isCompact_image_coe_of_bounded_of_weak_closed {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] [ProperSpace F] {s : Set (E' →SL[σ₁₂] F)} (hb : Bornology.IsBounded s) (hc : ∀ (f : E' →SL[σ₁₂] F), ⇑f ∈ closure (DFunLike.coe '' s) → f ∈ s) :

IsCompact (DFunLike.coe '' s)

If a set s of semilinear functions is bounded and is closed in the weak-* topology, then its image under coercion to functions E → F is a compact set. We don't have a name for E →SL[σ] F with weak-* topology in mathlib, so we use an equivalent condition (see isClosed_induced_iff').

source

theorem ContinuousLinearMap.is_weak_closed_closedBall {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_6} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_11} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] (f₀ : E' →SL[σ₁₂] F) (r : ℝ) ⦃f : E' →SL[σ₁₂] F⦄ (hf : ⇑f ∈ closure (DFunLike.coe '' Metric.closedBall f₀ r)) :

f ∈ Metric.closedBall f₀ r

A closed ball is closed in the weak-* topology. We don't have a name for E →SL[σ] F with weak-* topology in mathlib, so we use an equivalent condition (see isClosed_induced_iff').

source

theorem ContinuousLinearMap.isClosed_image_coe_closedBall {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f₀ : E →SL[σ₁₂] F) (r : ℝ) :

IsClosed (DFunLike.coe '' Metric.closedBall f₀ r)

The set of functions f : E → F that represent continuous linear maps f : E →SL[σ₁₂] F at distance ≤ r from f₀ : E →SL[σ₁₂] F is closed in the topology of pointwise convergence. This is one of the key steps in the proof of the Banach-Alaoglu theorem.

source

theorem ContinuousLinearMap.isCompact_image_coe_closedBall {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [ProperSpace F] (f₀ : E →SL[σ₁₂] F) (r : ℝ) :

IsCompact (DFunLike.coe '' Metric.closedBall f₀ r)

Banach-Alaoglu theorem. The set of functions f : E → F that represent continuous linear maps f : E →SL[σ₁₂] F at distance ≤ r from f₀ : E →SL[σ₁₂] F is compact in the topology of pointwise convergence. Other versions of this theorem can be found in Analysis.NormedSpace.WeakDual.

source

noncomputable def ContinuousLinearMap.extend {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜 Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [CompleteSpace F] (e : E →L[𝕜] Fₗ) (h_dense : DenseRange ⇑e) (h_e : UniformInducing ⇑e) :

Fₗ →SL[σ₁₂] F

Extension of a continuous linear map f : E →SL[σ₁₂] F, with E a normed space and F a complete normed space, along a uniform and dense embedding e : E →L[𝕜] Fₗ.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem ContinuousLinearMap.extend_eq {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜 Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [CompleteSpace F] (e : E →L[𝕜] Fₗ) (h_dense : DenseRange ⇑e) (h_e : UniformInducing ⇑e) (x : E) :

(ContinuousLinearMap.extend f e h_dense h_e) (e x) = f x

source

theorem ContinuousLinearMap.extend_unique {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜 Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [CompleteSpace F] (e : E →L[𝕜] Fₗ) (h_dense : DenseRange ⇑e) (h_e : UniformInducing ⇑e) (g : Fₗ →SL[σ₁₂] F) (H : ContinuousLinearMap.comp g e = f) :

ContinuousLinearMap.extend f e h_dense h_e = g

source

@[simp]

theorem ContinuousLinearMap.extend_zero {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜 Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} [CompleteSpace F] (e : E →L[𝕜] Fₗ) (h_dense : DenseRange ⇑e) (h_e : UniformInducing ⇑e) :

ContinuousLinearMap.extend 0 e h_dense h_e = 0

source

theorem ContinuousLinearMap.opNorm_extend_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜 Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [CompleteSpace F] (e : E →L[𝕜] Fₗ) (h_dense : DenseRange ⇑e) {N : NNReal} (h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖) [RingHomIsometric σ₁₂] :

‖ContinuousLinearMap.extend f e h_dense ⋯‖ ≤ ↑N * ‖f‖

If a dense embedding e : E →L[𝕜] G expands the norm by a constant factor N⁻¹, then the norm of the extension of f along e is bounded by N * ‖f‖.

source

@[deprecated ContinuousLinearMap.opNorm_extend_le]

theorem ContinuousLinearMap.op_norm_extend_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_6} {Fₗ : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup Fₗ] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜 Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [CompleteSpace F] (e : E →L[𝕜] Fₗ) (h_dense : DenseRange ⇑e) {N : NNReal} (h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖) [RingHomIsometric σ₁₂] :

‖ContinuousLinearMap.extend f e h_dense ⋯‖ ≤ ↑N * ‖f‖

Alias of ContinuousLinearMap.opNorm_extend_le.

If a dense embedding e : E →L[𝕜] G expands the norm by a constant factor N⁻¹, then the norm of the extension of f along e is bounded by N * ‖f‖.

Documentation

Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness

Operators on complete normed spaces #