On 4/3/2019 6:57 AM, Lawrence Paulson wrote:
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.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.
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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
