<abstract xmlns="http://www.w3.org/1999/xhtml">

<p>This paper formalizes in Mizar [1], [2], that the isometric isomorphisms between spaces formed by an (<italic>n</italic> + 1)-dimensional multilinear map and an <italic>n</italic>-fold composition of linear maps on real normed spaces. This result is used to describe the space of nth-order derivatives of the Frechet derivative as a multilinear space. In Section 1, we discuss the spaces of 1-dimensional multilinear maps and 0-fold compositions as a preparation, and in Section 2, we extend the discussion to the spaces of (<italic>n</italic> + 1)-dimensional multilinear map and an <italic>n</italic>-fold compositions. We referred to [4], [11], [8], [9] in this formalization.</p>
</abstract>

This paper formalizes in Mizar [1], [2], that the isometric isomorphisms between spaces formed by an (n + 1)-dimensional multilinear map and an n-fold composition of linear maps on real normed spaces. This result is used to describe the space of nth-order derivatives of the Frechet derivative as a multilinear space. In Section 1, we discuss the spaces of 1-dimensional multilinear maps and 0-fold compositions as a preparation, and in Section 2, we extend the discussion to the spaces of (n + 1)-dimensional multilinear map and an n-fold compositions. We referred to [4], [11], [8], [9] in this formalization.

Isomorphism between Spaces of Multilinear Maps and Nested Compositions over Real Normed Vector Spaces

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

This paper formalizes in Mizar [1], [2], that the isometric isomorphisms between spaces formed by an (n + 1)-dimensional multilinear map and an n-fold...

Isomorphism between Spaces of Multilinear Maps and Nested Compositions over Real Normed Vector Spaces

Published Online: Dec 21, 2022

Page range: 67 - 77

Accepted: Apr 30, 2022

DOI: https://doi.org/10.2478/forma-2022-0006

Keywords
Banach space, composition function, multilinear function

© 2022 Kazuhisa Nakasho et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Isomorphism between Spaces of Multilinear Maps and Nested Compositions over Real Normed Vector Spaces

Published Online: Dec 21, 2022

Page range: 67 - 77

Accepted: Apr 30, 2022

DOI: https://doi.org/10.2478/forma-2022-0006

KeywordsBanach space, composition function, multilinear function

© 2022 Kazuhisa Nakasho et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Keywords
Banach space, composition function, multilinear function