Ssreflect Users Discussion List

[Assia Mahboubi <>]

Hello,

  Marie Kerjean (cc'd) is working on a formalization of the Hahn-Banach
theorem in functional analysis.

This theorem takes place in real vector spaces of arbitrary (typically
non-finite) dimension, and requires a variant of Zorn, at least the
existence of an ultra-filter for any filter.

Since linear algebra in Mathematical Components is geared towards finite
dimension, Marie is using lmodType in combination with the experimental
(classical) analysis library.

But the formalized theory of lmodTypes available in Mathematical
Components lacks the theory of subspaces needed here.

We would be glad to hear comments/suggestions/feedback on the best
possible way to address this.

More precisely, the theorem we are interested in here is the so-called
analytical form of Hahn Banach:

Let V be a real vector space, and p a convex function V -> R.
Let G be a subspace of V and f a linear form on G such that:
 for any x in G, f x <= p x.
Then, there is a linear extension g of f on V such that g is still
bounded by p, i.e.:
  for any x in V, g x <= p x.

The proof goes by showing that f can be gradually linearly extended from
G to V, using a choice argument to ensure that the extension reaches V:
- take v in V \ G, and extend f to define it on G + vR (it is possible
because f is bounded by the convex p).
- define the relation <= on pairs (M, g) of a subspace and a linear form
on this set. It is a partial order, and Zorn's lemma provides a maximal
extension (M, g) of (G, f). (M, g) being maximal, M is necessarily V.

It is not entirely clear that subspaces are needed here: in fact we only
need to consider applications that are linear only on a subset (which is
in fact a subspace) of the larger V. Which is somehow a similar topic.

Any suggestion of a related formalization problem?

Many thanks in advance for your input.

Best wishes,

assia and Marie