Uniform approximation by finite partitions of unity

A continuous map F from a compact normal space X to a real normed space is uniformly approximated by the finite convex combinations x ↦ ∑ᶠ k, ρ k x • F k of its own values at finitely many points, with weights given by a partition of unity ρ indexed by those points. This reduces statements about the uniform norm on C(X, E) to statements about finitely many values. It is used, for example, to pass from Grothendieck's inequality for matrices to bounded bilinear forms on spaces of continuous functions.

For scalar-valued families this gives ContinuousMap.exists_partitionOfUnity_norm_sum_smul_sub_le, a uniform approximation of finitely many functions in C(X, 𝕜) by combinations of the partition functions, and PartitionOfUnity.norm_sum_smul_le_one bounds the uniform norm of such combinations with coefficients of norm at most one.

theorem ContinuousMap.exists_partitionOfUnity_dist_finsum_smul_le {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [CompactSpace X] [NormalSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] (F : C(X, E)) {ε : ℝ} (hε : 0 < ε) : ∃ (s : Finset X) (ρ : PartitionOfUnity (↥s) X), ∀ (x : X), dist (∑ᶠ (k : ↥s), (ρ k) x • F ↑k) (F x) ≤ ε

A continuous map on a compact normal space is uniformly within ε > 0 of the convex combinations of its values at the points of a finite set s, weighted by a partition of unity indexed by s.

theorem ContinuousMap.exists_partitionOfUnity_norm_sum_smul_sub_le {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [NormalSpace X] {𝕜 : Type u_3} {ι : Type u_4} [RCLike 𝕜] [Finite ι] (f : ι → C(X, 𝕜)) {δ : ℝ} (hδ : 0 < δ) : ∃ (s : Finset X) (ρ : PartitionOfUnity (↥s) X), ∀ (i : ι), ‖∑ k : ↥s, (f i) ↑k • { toFun := fun (x : X) => ↑((ρ k) x), continuous_toFun := ⋯ } - f i‖ ≤ δ

A finite family in C(X, 𝕜) is uniformly within δ > 0 of the combinations ∑ k, f i k • ρ k of its values at the points of a finite set, for a partition of unity ρ indexed by those points.

theorem PartitionOfUnity.norm_sum_smul_le_one {X : Type u_1} {𝕜 : Type u_2} {κ : Type u_3} [TopologicalSpace X] [CompactSpace X] [RCLike 𝕜] [Fintype κ] (ρ : PartitionOfUnity κ X) {c : κ → 𝕜} (hc : ∀ (k : κ), ‖c k‖ ≤ 1) : ‖∑ k : κ, c k • { toFun := fun (x : X) => ↑((ρ k) x), continuous_toFun := ⋯ }‖ ≤ 1

For a finite partition of unity ρ and scalars c k of norm at most one, the continuous function ∑ k, c k * ρ k has uniform norm at most one.