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).

noncomputable def ContinuousLinearMap.ofMemClosureImageCoeBounded {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6} [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 = (linearMapOfMemClosureRangeCoe f ⋯).mkContinuousOfExistsBound ⋯

@[simp]

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

noncomputable def ContinuousLinearMap.ofTendstoOfBoundedRange {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] {α : Type u_7} {l : Filter α} [l.NeBot] (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 ⋯

@[simp]

theorem ContinuousLinearMap.ofTendstoOfBoundedRange_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6} [SeminormedAddCommGroup E'] [NormedSpace 𝕜 E'] [RingHomIsometric σ₁₂] {α : Type u_7} {l : Filter α} [l.NeBot] (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)) : ⇑(ofTendstoOfBoundedRange f g hf hg) = f

theorem ContinuousLinearMap.tendsto_of_tendsto_pointwise_of_cauchySeq {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6} [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.

theorem ContinuousLinearMap.isCompact_closure_image_coe_of_bounded {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6} [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.

theorem ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6} [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.

theorem ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6} [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.

theorem ContinuousLinearMap.isCompact_image_coe_of_bounded_of_weak_closed {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6} [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').

theorem ContinuousLinearMap.is_weak_closed_closedBall {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6} [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').

theorem ContinuousLinearMap.isClosed_image_coe_closedBall {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [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.

theorem ContinuousLinearMap.isCompact_image_coe_closedBall {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [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.Normed.Module.WeakDual.