[isabelle-dev] Poly_Mapping

[Fabian Immler]

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 
https://www.isa-afp.org/browser_info/current/AFP/Smooth_Manifolds/Smooth.html 
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 
HOL-Analysis?

Fabian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190403/851c88e1/attachment-0001.bin>