L²
inner product space structure on finite products of inner product spaces #
The L²
norm on a finite product of inner product spaces is compatible with an inner product
$$ \langle x, y\rangle = \sum \langle x_i, y_i \rangle. $$
This is recorded in this file as an inner product space instance on PiLp 2
.
This file develops the notion of a finite dimensional Hilbert space over 𝕜 = ℂ, ℝ
, referred to as
E
. We define an OrthonormalBasis 𝕜 ι E
as a linear isometric equivalence
between E
and EuclideanSpace 𝕜 ι
. Then stdOrthonormalBasis
shows that such an equivalence
always exists if E
is finite dimensional. We provide language for converting between a basis
that is orthonormal and an orthonormal basis (e.g. Basis.toOrthonormalBasis
). We show that
orthonormal bases for each summand in a direct sum of spaces can be combined into an orthonormal
basis for the whole sum in DirectSum.IsInternal.subordinateOrthonormalBasis
. In
the last section, various properties of matrices are explored.
Main definitions #
EuclideanSpace 𝕜 n
: defined to bePiLp 2 (n → 𝕜)
for anyFintype n
, i.e., the space from functions ton
to𝕜
with theL²
norm. We register several instances on it (notably that it is a finite-dimensional inner product space).OrthonormalBasis 𝕜 ι
: defined to be an isometry to Euclidean space from a given finite-dimensional inner product space,E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
.Basis.toOrthonormalBasis
: constructs anOrthonormalBasis
for a finite-dimensional Euclidean space from aBasis
which isOrthonormal
.Orthonormal.exists_orthonormalBasis_extension
: provides an existential result of anOrthonormalBasis
extending a given orthonormal setexists_orthonormalBasis
: provides an orthonormal basis on a finite dimensional vector spacestdOrthonormalBasis
: provides an arbitrarily-chosenOrthonormalBasis
of a given finite dimensional inner product space
For consequences in infinite dimension (Hilbert bases, etc.), see the file
Analysis.InnerProductSpace.L2Space
.
Equations
- PiLp.innerProductSpace f = InnerProductSpace.mk ⋯ ⋯ ⋯ ⋯
The standard real/complex Euclidean space, functions on a finite type. For an n
-dimensional
space use EuclideanSpace 𝕜 (Fin n)
.
Equations
- EuclideanSpace 𝕜 n = PiLp 2 fun (x : n) => 𝕜
Instances For
A finite, mutually orthogonal family of subspaces of E
, which span E
, induce an isometry
from E
to PiLp 2
of the subspaces equipped with the L2
inner product.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A shorthand for PiLp.continuousLinearEquiv
.
Equations
- EuclideanSpace.equiv ι 𝕜 = PiLp.continuousLinearEquiv 2 𝕜 fun (x : ι) => 𝕜
Instances For
The projection on the i
-th coordinate of EuclideanSpace 𝕜 ι
, as a linear map.
Equations
- EuclideanSpace.projₗ i = LinearMap.proj i ∘ₗ ↑(WithLp.linearEquiv 2 𝕜 (ι → 𝕜))
Instances For
The projection on the i
-th coordinate of EuclideanSpace 𝕜 ι
,
as a continuous linear map.
Equations
- EuclideanSpace.proj i = { toLinearMap := EuclideanSpace.projₗ i, cont := ⋯ }
Instances For
The vector given in euclidean space by being a : 𝕜
at coordinate i : ι
and 0 : 𝕜
at
all other coordinates.
Equations
- EuclideanSpace.single i a = (WithLp.equiv 2 ((i : ι) → (fun (x : ι) => 𝕜) i)).symm (Pi.single i a)
Instances For
EuclideanSpace.single
forms an orthonormal family.
An orthonormal basis on E is an identification of E
with its dimensional-matching
EuclideanSpace 𝕜 ι
.
- ofRepr :: (
- repr : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
Linear isometry between
E
andEuclideanSpace 𝕜 ι
representing the orthonormal basis. - )
Instances For
b i
is the i
th basis vector.
Equations
- OrthonormalBasis.instFunLike = { coe := fun (b : OrthonormalBasis ι 𝕜 E) (i : ι) => b.repr.symm (EuclideanSpace.single i 1), coe_injective' := ⋯ }
The Basis ι 𝕜 E
underlying the OrthonormalBasis
Equations
- b.toBasis = Basis.ofEquivFun b.repr.toLinearEquiv
Instances For
Mapping an orthonormal basis along a LinearIsometryEquiv
.
Equations
- b.map L = { repr := L.symm.trans b.repr }
Instances For
A basis that is orthonormal is an orthonormal basis.
Equations
- v.toOrthonormalBasis hv = { repr := v.equivFun.isometryOfInner ⋯ }
Instances For
Pi.orthonormalBasis (B : ∀ i, OrthonormalBasis (ι i) 𝕜 (E i))
is the
Σ i, ι i
-indexed orthonormal basis on Π i, E i
given by B i
on each component.
Equations
- Pi.orthonormalBasis B = { repr := (LinearIsometryEquiv.piLpCongrRight 2 fun (i : η) => (B i).repr).trans (LinearIsometryEquiv.piLpCurry 𝕜 2 fun (x : η) (x : ι x) => 𝕜).symm }
Instances For
A finite orthonormal set that spans is an orthonormal basis
Equations
- OrthonormalBasis.mk hon hsp = (Basis.mk ⋯ hsp).toOrthonormalBasis ⋯
Instances For
Any finite subset of an orthonormal family is an OrthonormalBasis
for its span.
Equations
- OrthonormalBasis.span h s = (OrthonormalBasis.mk ⋯ ⋯).map (LinearIsometryEquiv.ofEq (Submodule.span 𝕜 ↑(Finset.image v' s)) (Submodule.span 𝕜 (Set.range (v' ∘ Subtype.val))) ⋯).symm
Instances For
A finite orthonormal family of vectors whose span has trivial orthogonal complement is an orthonormal basis.
Equations
- OrthonormalBasis.mkOfOrthogonalEqBot hon hsp = OrthonormalBasis.mk hon ⋯
Instances For
b.reindex (e : ι ≃ ι')
is an OrthonormalBasis
indexed by ι'
Equations
- b.reindex e = { repr := b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) }
Instances For
The basis Pi.basisFun
, bundled as an orthornormal basis of EuclideanSpace 𝕜 ι
.
Equations
- EuclideanSpace.basisFun ι 𝕜 = { repr := LinearIsometryEquiv.refl 𝕜 (EuclideanSpace 𝕜 ι) }
Instances For
Equations
- OrthonormalBasis.instInhabited = { default := EuclideanSpace.basisFun ι 𝕜 }
![1, I]
is an orthonormal basis for ℂ
considered as a real inner product space.
Equations
- Complex.orthonormalBasisOneI = Complex.basisOneI.toOrthonormalBasis Complex.orthonormalBasisOneI.proof_1
Instances For
The isometry between ℂ
and a two-dimensional real inner product space given by a basis.
Equations
- Complex.isometryOfOrthonormal v = Complex.orthonormalBasisOneI.repr.trans v.repr.symm
Instances For
Matrix representation of an orthonormal basis with respect to another #
A version of OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary
that works for bases with
different index types.
A version of OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary
that works for bases with
different index types.
The change-of-basis matrix between two orthonormal bases a
, b
is a unitary matrix.
The determinant of the change-of-basis matrix between two orthonormal bases a
, b
has
unit length.
The change-of-basis matrix between two orthonormal bases a
, b
is an orthogonal matrix.
The determinant of the change-of-basis matrix between two orthonormal bases a
, b
is ±1.
Existence of orthonormal basis, etc. #
Given an internal direct sum decomposition of a module M
, and an orthonormal basis for each
of the components of the direct sum, the disjoint union of these orthonormal bases is an
orthonormal basis for M
.
Equations
- DirectSum.IsInternal.collectedOrthonormalBasis hV hV_sum v_family = (hV_sum.collectedBasis fun (i : ι) => (v_family i).toBasis).toOrthonormalBasis ⋯
Instances For
In a finite-dimensional InnerProductSpace
, any orthonormal subset can be extended to an
orthonormal basis.
A finite-dimensional inner product space admits an orthonormal basis.
A finite-dimensional InnerProductSpace
has an orthonormal basis.
Equations
Instances For
An orthonormal basis of ℝ
is made either of the vector 1
, or of the vector -1
.
Exhibit a bijection between Fin n
and the index set of a certain basis of an n
-dimensional
inner product space E
. This should not be accessed directly, but only via the subsequent API.
Instances For
An n
-dimensional InnerProductSpace
equipped with a decomposition as an internal direct
sum has an orthonormal basis indexed by Fin n
and subordinate to that direct sum.
Instances For
An n
-dimensional InnerProductSpace
equipped with a decomposition as an internal direct
sum has an orthonormal basis indexed by Fin n
and subordinate to that direct sum. This function
provides the mapping by which it is subordinate.
Instances For
The basis constructed in DirectSum.IsInternal.subordinateOrthonormalBasis
is subordinate to
the OrthogonalFamily
in question.
Given a natural number n
one less than the finrank
of a finite-dimensional inner product
space, there exists an isometry from the orthogonal complement of a nonzero singleton to
EuclideanSpace 𝕜 (Fin n)
.
Equations
- OrthonormalBasis.fromOrthogonalSpanSingleton n hv = (stdOrthonormalBasis 𝕜 ↥(Submodule.span 𝕜 {v})ᗮ).reindex (finCongr ⋯)
Instances For
Let S
be a subspace of a finite-dimensional complex inner product space V
. A linear
isometry mapping S
into V
can be extended to a full isometry of V
.
TODO: The case when S
is a finite-dimensional subspace of an infinite-dimensional V
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Matrix.toLin'
adapted for EuclideanSpace 𝕜 _
.
Equations
- Matrix.toEuclideanLin = Matrix.toLin'.trans ((WithLp.linearEquiv 2 𝕜 (n → 𝕜)).symm.arrowCongr (WithLp.linearEquiv 2 𝕜 (m → 𝕜)).symm)
Instances For
The inner product of a row of A
and a row of B
is an entry of B * Aᴴ
.
The inner product of a column of A
and a column of B
is an entry of Aᴴ * B
.