Approximation property

DefinitionApproximation property#✓fully proved

A normed space has the approximation property if, on every compact set, the identity operator is a uniform limit of finite-rank continuous linear operators.

def HasApproximationProperty (𝕜 E : Type*) [RCLike 𝕜] [NormedAddCommGroup E]
    [NormedSpace 𝕜 E] : Prop :=
  ∀ (K : Set E), IsCompact K → ∀ ε : ℝ, 0 < ε →
    ∃ T : E →L[𝕜] E, FiniteDimensional 𝕜 ↥(LinearMap.range T.toLinearMap) ∧
      ∀ x ∈ K, ‖T x - x‖ < ε

Used by 5

Used byFinite-dimensional spaces have the approximation property · Separable Hilbert spaces have the approximation property · Banach spaces with a Schauder basis have the approximation property · Approximation property passes to complemented subspaces · Approximation property is invariant under linear isomorphism

TheoremFinite-dimensional spaces have the approximation property#✓fully proved

Finite-dimensional spaces have the approximation property: the identity operator is itself finite-rank.

theorem hasApproximationProperty_of_finiteDimensional (E : Type*)
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] :
    HasApproximationProperty 𝕜 E

Uses 1

Statement usesApproximation property

TheoremBanach spaces with a Schauder basis have the approximation property#✓fully proved

A Banach space with a Schauder basis has the approximation property. The partial-sum projections are finite-rank, converge pointwise to the identity, and are uniformly bounded by the Banach–Steinhaus theorem (SchauderBasis.exists_norm_proj_le); pointwise convergence plus uniform boundedness gives uniform convergence on compact sets via a finite ε-net argument.

theorem hasApproximationProperty_of_schauderBasis {E : Type*} [NormedAddCommGroup E]
    [NormedSpace 𝕜 E] [CompleteSpace E] (b : SchauderBasis 𝕜 E) :
    HasApproximationProperty 𝕜 E

Uses 1 · Used by 1

Statement usesApproximation property

Used bySeparable Hilbert spaces have the approximation property

TheoremApproximation property is invariant under linear isomorphism#✓fully proved

The approximation property is preserved under continuous linear equivalence: conjugate a finite-rank approximant by the equivalence.

theorem HasApproximationProperty.of_continuousLinearEquiv {E F : Type*}
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F]
    (h : HasApproximationProperty 𝕜 E) (e : E ≃L[𝕜] F) :
    HasApproximationProperty 𝕜 F

Uses 1

Statement usesApproximation property

TheoremApproximation property passes to complemented subspaces#✓fully proved

The approximation property passes to complemented subspaces: if P is a continuous projection onto the submodule F, restrict a finite-rank approximant on the ambient space via P. The key point is that P fixes every point of F, so P (S x) - x = P (S x - x) for x ∈ F.

theorem HasApproximationProperty.of_complemented {E : Type*} [NormedAddCommGroup E]
    [NormedSpace 𝕜 E] (h : HasApproximationProperty 𝕜 E) {F : Submodule 𝕜 E}
    (P : E →L[𝕜] E) (hPid : ∀ x, P (P x) = P x)
    (hPrange : LinearMap.range P.toLinearMap = F) :
    HasApproximationProperty 𝕜 ↥F

Uses 1

Statement usesApproximation property

TheoremSeparable Hilbert spaces have the approximation property#✓fully proved

A Hilbert space with a Hilbert basis indexed by ℕ has the approximation property, via the associated Schauder basis (HilbertBasis.toSchauderBasis).

theorem hasApproximationProperty_of_hilbertBasis {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace 𝕜 E] [CompleteSpace E] (b : HilbertBasis ℕ 𝕜 E) :
    HasApproximationProperty 𝕜 E

Uses 2

Statement usesApproximation property

Proof usesBanach spaces with a Schauder basis have the approximation property

DefinitionMazur's Problem 153#✓fully proved

The claim of Mazur's Problem 153 from the Scottish Book, in its original form: for every continuous function \(f \colon [0,1]^2 \to \mathbb{R}\) and every real \(\varepsilon > 0\) there are a natural number \(n\), points \(a_1, \dots, a_n, b_1, \dots, b_n \in [0,1]\) and real numbers \(c_1, \dots, c_n\) such that

\[\Bigl| f(x, y) - \sum_{k=1}^n c_k \, f(a_k, y) \, f(x, b_k) \Bigr| \le \varepsilon\]

for all \(x, y \in [0,1]\).

def ScottishBookProblem153Claim : Prop :=
  ∀ (f : C(↥(Set.Icc (0 : ℝ) 1) × ↥(Set.Icc (0 : ℝ) 1), ℝ)) (ε : ℝ), 0 < ε →
    ∃ (n : ℕ) (a b : Fin n → ↥(Set.Icc (0 : ℝ) 1)) (c : Fin n → ℝ),
      ∀ (x y : ↥(Set.Icc (0 : ℝ) 1)),
        -- `dist` here is `|f (x, y) - ∑ k, c k * f (a k, y) * f (x, b k)|` by `Real.dist_eq`.
        dist (f (x, y)) (∑ k, c k * f (a k, y) * f (x, b k)) ≤ ε

Used by 1

Used byNegative answer to Mazur's Problem 153

TheoremNegative answer to Mazur's Problem 153#●ready to prove

There are a continuous function \(f \colon [0,1]^2 \to \mathbb{R}\) and a real number \(\varepsilon > 0\) such that for every natural number \(n\), all points \(a_1, \dots, a_n, b_1, \dots, b_n \in [0,1]\) and all real numbers \(c_1, \dots, c_n\) there are \(x, y \in [0,1]\) with

\[\Bigl| f(x, y) - \sum_{k=1}^n c_k \, f(a_k, y) \, f(x, b_k) \Bigr| > \varepsilon.\]

That is, the approximation scheme of Mazur's Problem 153 fails.

theorem_wanted mazur153_refuted : ¬ ScottishBookProblem153Claim

Sources

• S. Mazur, Problem 153 of the Scottish Book; refuted via P. Enflo's counterexample to the approximation problem in Banach spaces, Acta Math. 130 (1973), 309–317, DOI 10.1007/BF02392270; see the commentary in R. D. Mauldin (ed.), The Scottish Book, 2nd ed. (Birkhäuser, 2015). This is the original bivariate-function form of the problem, distinct from its consequence for the approximation property.

Uses 1

Statement usesMazur's Problem 153

7 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.