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 pi_Lp 2
.
Main definitions #
-
euclidean_space 𝕜 n
: defined to bepi_Lp 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). -
orthonormal_basis 𝕜 ι
: defined to be an isometry to Euclidean space from a given finite-dimensional innner product space,E ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι
. -
basis.to_orthonormal_basis
: constructs anorthonormal_basis
for a finite-dimensional Euclidean space from abasis
which isorthonormal
. -
linear_isometry_equiv.of_inner_product_space
: provides an arbitrary isometry to Euclidean space from a given finite-dimensional inner product space, induced by choosing an arbitrary basis. -
complex.isometry_euclidean
: standard isometry fromℂ
toeuclidean_space ℝ (fin 2)
Equations
- pi_Lp.inner_product_space f = {to_normed_group := pi_Lp.normed_group 2 f (λ (i : ι), inner_product_space.to_normed_group 𝕜), to_normed_space := pi_Lp.normed_space 2 f 𝕜 (λ (i : ι), inner_product_space.to_normed_space), to_has_inner := {inner := λ (x y : pi_Lp 2 f), finset.univ.sum (λ (i : ι), has_inner.inner (x i) (y i))}, norm_sq_eq_inner := _, conj_sym := _, add_left := _, smul_left := _}
The standard real/complex Euclidean space, functions on a finite type. For an n
-dimensional
space use euclidean_space 𝕜 (fin n)
.
Equations
- euclidean_space 𝕜 n = pi_Lp 2 (λ (i : n), 𝕜)
Equations
- euclidean_space.inner_product_space = pi_Lp.inner_product_space (λ (i : ι), 𝕜)
A finite, mutually orthogonal family of subspaces of E
, which span E
, induce an isometry
from E
to pi_Lp 2
of the subspaces equipped with the L2
inner product.
Equations
- hV.isometry_L2_of_orthogonal_family hV' = let e₁ : direct_sum ι (λ (i : ι), (λ (i : ι), ↥(V i)) i) ≃ₗ[𝕜] Π (i : ι), (λ (i : ι), ↥(V i)) i := direct_sum.linear_equiv_fun_on_fintype 𝕜 ι (λ (i : ι), ↥(V i)), e₂ : direct_sum ι (λ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := linear_equiv.of_bijective (direct_sum.submodule_coe V) _ _ in (e₂.symm.trans e₁).isometry_of_inner _
The vector given in euclidean space by being 1 : 𝕜
at coordinate i : ι
and 0 : 𝕜
at
all other coordinates.
Equations
- euclidean_space.single i a = pi.single i a
- repr : E ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι
An orthonormal basis on E is an identification of E
with its dimensional-matching
euclidean_space 𝕜 ι
.
Instances for orthonormal_basis
- orthonormal_basis.has_sizeof_inst
- orthonormal_basis.inhabited
- orthonormal_basis.has_coe_to_fun
Equations
b i
is the i
th basis vector.
Equations
- orthonormal_basis.has_coe_to_fun = {coe := λ (b : orthonormal_basis ι 𝕜 E) (i : ι), ⇑(b.repr.symm) (euclidean_space.single i 1)}
The basis ι 𝕜 E
underlying the orthonormal_basis
-
Equations
A basis that is orthonormal is an orthonormal basis.
Equations
- v.to_orthonormal_basis hv = {repr := v.equiv_fun.isometry_of_inner _}
An orthonormal set that spans is an orthonormal basis
Equations
- orthonormal_basis.mk hon hsp = (basis.mk _ hsp).to_orthonormal_basis _
If f : E ≃ₗᵢ[𝕜] E'
is a linear isometry of inner product spaces then an orthonormal basis v
of E
determines a linear isometry e : E' ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι
. This result states that
e
may be obtained either by transporting v
to E'
or by composing with the linear isometry
E ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι
provided by v
.
ℂ
is isometric to ℝ²
with the Euclidean inner product.
Equations
- complex.isometry_euclidean = (complex.basis_one_I.to_orthonormal_basis complex.isometry_euclidean._proof_1).repr
The isometry between ℂ
and a two-dimensional real inner product space given by a basis.
Equations
Given a natural number n
equal to the finrank
of a finite-dimensional inner product space,
there exists an isometry from the space to euclidean_space 𝕜 (fin n)
.
Equations
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
euclidean_space 𝕜 (fin n)
.
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
- L.extend = let d : ℕ := finite_dimensional.finrank 𝕜 ↥Sᗮ, LS : submodule 𝕜 V := L.to_linear_map.range, L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp (let BS : orthonormal_basis (fin d) 𝕜 ↥Sᗮ := (fin_std_orthonormal_basis linear_isometry.extend._proof_6).to_orthonormal_basis linear_isometry.extend._proof_7, BLS : orthonormal_basis (fin d) 𝕜 ↥LSᗮ := (fin_std_orthonormal_basis _).to_orthonormal_basis _ in BS.repr.trans BLS.repr.symm).to_linear_isometry, p1 : V →ₗ[𝕜] ↥S := (orthogonal_projection S).to_linear_map, p2 : V →ₗ[𝕜] ↥Sᗮ := (orthogonal_projection Sᗮ).to_linear_map, M : V →ₗ[𝕜] V := L.to_linear_map.comp p1 + L3.to_linear_map.comp p2 in {to_linear_map := M, norm_map' := _}
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