Ssreflect Users Discussion List

[Cyril Cohen <>]

Hi everyone,

I am very short on time right now, and I did not have time to read 
everything you both wrote :(. Sorry about that.
Just my two cents though.

To me, the right approach is indeed to use a `V : lmodType R`, to denote 
the total space, and then use predicates G that are `submodPred` to 
denote subspaces.

Then I think you have two ways to go:

A. You may form any sub-type `W` of elements of the subspace (where the 
predicate defining the subtype is convertible to your `submodPred`), and 
this will be already canonically a `lmodType R` (you can test it with 
`[lmodMixin of W by <:]`).

B. Alternatively, you can break the construction in multiple steps:
1. You first show there exists U s.t. G + U = V, although the + 
operation on submodPred is not yet available to my knowledge.
2. extending linear function on G to full V by prolongating with 0 on a 
complement U of G.
3. showing that to linear function on V you can find another linear 
function g, that coincides with f on G, but which is bounded by p.

Best,
--
Cyril

On 30/01/2019 10:55, Florian Steinberg wrote:
> Hi Assia!
>
> I've recently been formalizing some basic facts about lp-spaces (spaces 
> of summable sequences, not integrable functions), which got me into 
> similar problems. I decided to go with coquelicot and the Rstruct file. 
> Since mathcomp analysis is build on Coquelicot's Hierarchy.v file and 
> Rstruct.v, we should basically be talking about the same stuff... 
> Coquelicot doesn't say a lot about subspaces either (there is work on 
> finite dimensional subspaces of Hilbertspaces by Sylvie and Florian, but 
> lp-spaces infinite dimensional subspaces of a rather big and certainly 
> not Hilbert topological vector space). I think one of the major reasons 
> for the absence of subspaces is that it is difficult to say anything 
> without axioms. (and for coquelicot additionally that the axioms of the 
> reals do not help enough). For instance for spaces of sequences I use 
> functional extensionality to be able to proof that the zero element 
> works and for other parts I have to use proof irrelevance and countable 
> functional choice at least. If I recall correctly, mathcomp-analysis 
> assumes all of these, but neither Coquelicot nor mathcomp themselves do, 
> so this might explain why there is so little material available.
>
> You can find some of the my attempts to make subspaces work for metric 
> spaces on my github account if you are interested (the metric 
> repository, the lp-stuff is in an example file in the incone 
> repository). If you are interested in discussing any of this... I'll be 
> back in Paris from mid February. I'd definatelly be interested in seeing 
> what you are up to with these Banach spaces.
>
> Best,
>
> Florian
>
> On 29/01/2019 17:41, Assia Mahboubi wrote:
> > 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