Approximation properties of normed spaces

The approximation property asks for finite-rank bounded operators approximating the identity uniformly on each norm-compact set. The bounded approximation property imposes a common operator norm bound; the metric approximation property uses bound one. These definitions do not require completeness.

A uniformly bounded net of finite-rank operators converging pointwise to the identity gives the bounded approximation property. The compact-uniform convergence needed here follows from Mathlib's equicontinuity criterion for bounded families of operators and its Ascoli theorem. This criterion applies to finite projections of Schauder bases.

Finite rank is Mathlib's LinearMap.HasFiniteRange, meaning finitely generated range, which over a field is equivalent to finite-dimensional range.

References

• R. E. Megginson, An Introduction to Banach Space Theory, Section 3.4.
• F. Albiac and N. J. Kalton, Topics in Banach Space Theory, Chapter 1.

def TauCeti.HasApproximationProperty (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Prop

The identity can be approximated uniformly on every norm-compact set by bounded operators with finite-dimensional range.

def TauCeti.HasBoundedApproximationPropertyWith (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (C : NNReal) : Prop

The approximation property with the common operator norm bound C.

def TauCeti.HasBoundedApproximationProperty (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Prop

The identity has finite-rank approximations on compact sets with some common finite norm bound. The bound is independent of both the compact set and the error tolerance.

def TauCeti.HasMetricApproximationProperty (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Prop

The identity can be approximated uniformly on compact sets by finite-rank contractions.

theorem TauCeti.hasApproximationProperty_iff {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] : HasApproximationProperty 𝕜 E ↔ ∀ (K : Set E), IsCompact K → ∀ ε > 0, ∃ (T : E →L[𝕜] E), (↑T).HasFiniteRange ∧ ∀ x ∈ K, ‖T x - x‖ < ε

Characterization of the approximation property by compact-set approximations.

theorem TauCeti.hasBoundedApproximationPropertyWith_iff {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {C : NNReal} : HasBoundedApproximationPropertyWith 𝕜 E C ↔ ∀ (K : Set E), IsCompact K → ∀ ε > 0, ∃ (T : E →L[𝕜] E), (↑T).HasFiniteRange ∧ ‖T‖ ≤ ↑C ∧ ∀ x ∈ K, ‖T x - x‖ < ε

Characterization of the approximation property with a prescribed norm bound.

theorem TauCeti.HasBoundedApproximationPropertyWith.mono {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {C D : NNReal} (h : HasBoundedApproximationPropertyWith 𝕜 E C) (hCD : C ≤ D) : HasBoundedApproximationPropertyWith 𝕜 E D

A larger norm bound preserves the bounded approximation property.

theorem TauCeti.HasBoundedApproximationPropertyWith.hasApproximationProperty {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {C : NNReal} (h : HasBoundedApproximationPropertyWith 𝕜 E C) : HasApproximationProperty 𝕜 E

Forgetting a prescribed norm bound gives the approximation property.

theorem TauCeti.HasBoundedApproximationPropertyWith.hasBoundedApproximationProperty {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {C : NNReal} (h : HasBoundedApproximationPropertyWith 𝕜 E C) : HasBoundedApproximationProperty 𝕜 E

A prescribed finite bound witnesses the bounded approximation property.

theorem TauCeti.HasBoundedApproximationProperty.hasApproximationProperty {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (h : HasBoundedApproximationProperty 𝕜 E) : HasApproximationProperty 𝕜 E

The bounded approximation property implies the approximation property.

theorem TauCeti.hasBoundedApproximationProperty_iff {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] : HasBoundedApproximationProperty 𝕜 E ↔ ∃ (C : NNReal), HasBoundedApproximationPropertyWith 𝕜 E C

Characterization of the bounded approximation property by a common finite bound.

theorem TauCeti.hasMetricApproximationProperty_iff {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] : HasMetricApproximationProperty 𝕜 E ↔ HasBoundedApproximationPropertyWith 𝕜 E 1

The metric approximation property is the case of norm bound one.

theorem TauCeti.HasMetricApproximationProperty.hasBoundedApproximationProperty {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (h : HasMetricApproximationProperty 𝕜 E) : HasBoundedApproximationProperty 𝕜 E

The metric approximation property implies the bounded approximation property.

theorem TauCeti.HasBoundedApproximationPropertyWith.of_tendsto {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {ι : Type u_3} {l : Filter ι} [l.NeBot] {C : NNReal} (T : ι → E →L[𝕜] E) (hfinite : ∀ (i : ι), (↑(T i)).HasFiniteRange) (hbound : ∀ (i : ι), ‖T i‖ ≤ ↑C) (hlim : ∀ (x : E), Filter.Tendsto (fun (i : ι) => (T i) x) l (nhds x)) : HasBoundedApproximationPropertyWith 𝕜 E C

A uniformly bounded net of finite-rank operators converging pointwise to the identity gives the bounded approximation property with the same bound.

theorem TauCeti.hasMetricApproximationProperty_of_finiteDimensional {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] : HasMetricApproximationProperty 𝕜 E

Finite-dimensional normed spaces have the metric approximation property.