Physlib.SpaceAndTime.Space.Slice
Slices of space
i. Overview
In this module we will define the equivalence between `Space d.succ` and `ℝ × Space d` which extracts the `i`th coordinate on `Space d.succ`.
ii. Key results
- `slice` : The continuous linear equivalence between `Space d.succ` and `ℝ × Space d` extracting the `i`th coordinate.
iii. Table of contents
- A. Slicing spaces - A.1. Basic applications of the slicing map - A.2. Slice as a measurable embedding - A.3. The norm of the slice map - A.4. Derivative of the slice map - A.5. Basis in terms of slices
iv. References
- https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/API.20around.20.60Space.20.28d1.20.2B.20d2.29.60.20to.20.60Space.20d1.20x.20Space.20d2.60/with/556754634
A. Slicing spaces
A.1. Basic applications of the slicing map
A.2. Slice as a measurable embedding
A.3. The norm of the slice map
A.4. Derivative of the slice map
A.5. Basis in terms of slices
15 declarations
Continuous linear equivalence via the -th coordinate slice
For a natural number and an index , the map is a continuous linear equivalence (a topological vector space isomorphism) between and . Given an element , the map extracts the -th coordinate as the first component of the product and projects the remaining coordinates onto . Specifically, it is defined by , where and is the function that skips the index .
The inverse of corresponds to inserting the -th coordinate
For any natural number , an index , a scalar , and a vector , the inverse of the continuous linear equivalence applied to the pair is the vector in obtained by inserting at the -th coordinate and filling the remaining coordinates with the components of .
The -th coordinate of is
For any natural number , index , real number , and vector , the -th coordinate of the vector obtained by applying the inverse of the slicing map to the pair is equal to . Here, is the inverse of the continuous linear equivalence that extracts the -th coordinate.
Components of at non- indices are
For any natural number , index , scalar , and vector , let be the vector in obtained by inserting at the -th coordinate and filling the remaining positions with . For any , the component of at the index is equal to the -th component of , where maps to the corresponding index in .
The inverse slicing map is a measurable embedding
For any natural number and index , the inverse of the slicing map is a measurable embedding. The slicing map is the continuous linear equivalence that identifies with by extracting the -th coordinate; its inverse reconstructs a vector in by inserting a real value at the -th position and filling the remaining coordinates with the components of a vector in .
For any natural number , index , real number , and vector , the Euclidean norm of the vector in obtained by applying the inverse of the slicing map to the pair is given by: where is the isomorphism that inserts as the -th coordinate and uses the components of for the remaining coordinates.
For any natural number , index , real number , and vector , the absolute value of is less than or equal to the Euclidean norm of the vector in produced by applying the inverse slicing map to the pair : where is the isomorphism that constructs a vector by inserting as the -th coordinate and using the components of for the remaining dimensions.
For any natural number , index , real number , and vector , the Euclidean norm of is less than or equal to the Euclidean norm of the vector in obtained by applying the inverse slicing map to the pair : where is the isomorphism that inserts as the -th coordinate and uses the components of for the remaining coordinates.
The Fréchet derivative of is
For any natural number , index , and point , the Fréchet derivative of the inverse slice map at the point is equal to the linear map itself.
The Fréchet derivative of is
For any natural number , index , and fixed vector , consider the function defined by , where is the inverse of the continuous linear equivalence that extracts the -th coordinate. For any , the Fréchet derivative of at the point applied to the direction is given by:
The Fréchet derivative of with respect to the right component applied to is
For any natural number , index , fixed real number , and points , the Fréchet derivative of the map defined by at the point applied to the vector is equal to , where is the inverse of the -th coordinate slice map.
Fréchet derivative of with respect to the spatial component applied to
For any natural number , index , and fixed real number , let be a function that is differentiable at for some point . The Fréchet derivative of the composition at the point applied to a vector is equal to the Fréchet derivative of at the point applied to the vector , where denotes the inverse of the -th coordinate slice map.
The Fréchet derivative of is
For any natural number , index , real numbers , vector , and function , suppose is differentiable at the point , where is the inverse of the continuous linear equivalence that extracts the -th coordinate. The Fréchet derivative of the composition at the point applied to the increment is given by:
For any natural number and index , let be the -th vector of the standard orthonormal basis of . This basis vector is equal to the image of the pair under the inverse of the slicing map , where is the zero element of .
For any natural number , index , and index , let denote the standard orthonormal basis of and denote the standard orthonormal basis of . The basis vector is equal to the image of the pair under the inverse of the slicing map . Here, is the index in obtained by skipping the index .
