Helly's lemma

Helly's lemma solves finitely many linear equations in a normed space with almost optimal norm. If φ is an element of the bidual of a normed space E and f₁, …, fₙ are continuous linear functionals on E, then for every ε > 0 there is x : E with ‖x‖ < ‖φ‖ + ε and fᵢ x = φ fᵢ for every i. Equivalently, every finite-dimensional subspace W of the dual admits such an x interpolating φ on all of W. The tolerance cannot be removed in general: for a single functional f and a norm-one φ with φ f = ‖f‖, a solution of norm at most one would be a point of the closed unit ball where f attains its norm.

Classically the lemma is stated without the bidual: prescribed values cᵢ of the functionals fᵢ are attained by vectors of norm less than M + ε for every ε > 0 if and only if ‖∑ aᵢ cᵢ‖ ≤ M ‖∑ aᵢ fᵢ‖ for all scalars aᵢ.

These finite interpolation statements are the basic finite-system tool behind the principle of local reflexivity, which upgrades them to linear maps from finite-dimensional subspaces of the bidual into E. This is unrelated to Helly's intersection theorem for convex sets (Convex.helly_theorem in Mathlib.Analysis.Convex.Radon).

Main results

• StrongDual.exists_norm_lt_and_forall_apply_eq: Helly's lemma for a finite family of functionals and an element of the bidual.
• StrongDual.exists_norm_lt_and_forall_mem_apply_eq: the same for a finite-dimensional subspace of the dual.
• StrongDual.norm_sum_apply_comp_single_le: a coordinatewise bound for functionals on a finite product κ → E, paired with bidual vectors of norm at most one.
• TauCeti.exists_norm_lt_and_forall_apply_eq_iff: Helly's criterion for prescribed values.

References

• H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Lemma 3.3.
• F. Albiac and N. J. Kalton, Topics in Banach Space Theory, §12.2 (the principle of local reflexivity).

theorem StrongDual.exists_norm_lt_and_forall_apply_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (φ : StrongDual 𝕜 (StrongDual 𝕜 E)) {ι : Type u_3} [Finite ι] (f : ι → StrongDual 𝕜 E) {ε : ℝ} (hε : 0 < ε) : ∃ (x : E), ‖x‖ < ‖φ‖ + ε ∧ ∀ (i : ι), (f i) x = φ (f i)

Helly's lemma. For an element φ of the bidual of E, finitely many continuous linear functionals f i on E and ε > 0, some x : E with ‖x‖ < ‖φ‖ + ε satisfies f i x = φ (f i) for every i.

theorem StrongDual.exists_norm_lt_and_forall_mem_apply_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (φ : StrongDual 𝕜 (StrongDual 𝕜 E)) (W : Submodule 𝕜 (StrongDual 𝕜 E)) [FiniteDimensional 𝕜 ↥W] {ε : ℝ} (hε : 0 < ε) : ∃ (x : E), ‖x‖ < ‖φ‖ + ε ∧ ∀ f ∈ W, f x = φ f

Helly's lemma for a finite-dimensional subspace W of the dual: for an element φ of the bidual of E and ε > 0, some x : E with ‖x‖ < ‖φ‖ + ε satisfies f x = φ f for every f ∈ W.

theorem StrongDual.norm_sum_apply_comp_single_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {κ : Type u_3} [Fintype κ] [DecidableEq κ] (f : StrongDual 𝕜 (κ → E)) (hf : ‖f‖ ≤ 1) (z : κ → StrongDual 𝕜 (StrongDual 𝕜 E)) (hz : ∀ (i : κ), ‖z i‖ ≤ 1) : ‖∑ i : κ, (z i) (f ∘SL ContinuousLinearMap.single 𝕜 (fun (x : κ) => E) i)‖ ≤ 1

Helly's lemma, coordinatewise: a functional f of norm at most one on a finite product κ → E pairs bidual vectors z i of norm at most one with its coordinate functionals f ∘ single i to a value of norm at most one.

theorem TauCeti.exists_norm_lt_and_forall_apply_eq_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {ι : Type u_3} [Fintype ι] (f : ι → StrongDual 𝕜 E) (c : ι → 𝕜) {M : ℝ} (hM : 0 ≤ M) : (∀ ε > 0, ∃ (x : E), ‖x‖ < M + ε ∧ ∀ (i : ι), (f i) x = c i) ↔ ∀ (a : ι → 𝕜), ‖∑ i : ι, a i * c i‖ ≤ M * ‖∑ i : ι, a i • f i‖

Helly's criterion. Let f i be finitely many continuous linear functionals on E, let c i be scalars and let 0 ≤ M. For every ε > 0 some x : E with ‖x‖ < M + ε satisfies f i x = c i for every i if and only if ‖∑ i, a i * c i‖ ≤ M * ‖∑ i, a i • f i‖ for all scalars a i.