immler at in.tum.de
Wed Apr 3 16:53:27 CEST 2019
On 4/3/2019 6:57 AM, Lawrence Paulson wrote:
> I have adopted the theory Poly_Mapping, which is part of the AFP entry Polynomials, as the basis for a theory of finite abelian groups, which plays a huge role in the homology development. (It concerns "almost everywhere zero functions”.) I am gradually installing the components of this development in various places, and think that Poly_Mapping could go into Library, as it depends only on other Library entries. I hope nobody objects to this. Then I guess the duplicate in the AFP should be deleted.
> I also managed to accomplish the following:
> instantiation "poly_mapping" :: (type, real_normed_vector) real_normed_vector
> But I never found a use for it and I’m not sure what to do with it.
I always thought this would be useful to define (bounded) multilinear
maps and use them to define higher derivatives.
Somewhat like nth_derivative in
but without the restriction that the derivative is taken in the same
direction h for every order.
It could also useful for an alternative take on finite dimensional analysis.
Instead of fixing the dimension in the type (like with the
euclidean_space type class or the real^('n::finite) types), with
poly_mapping, one can fix the Basis/dimension with an explicit assumption.
Having the dimension in the term language makes everything more
flexible, while still keeping most of advantages of using type classes
(for all the properties below real_normed_vector).
Given that there are several potential applications, I guess you could
add it as a separate theory (Poly_Mapping_Normed_Vector_Space?) to
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev