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.
This file develops the notion of a finite dimensional Hilbert space over 𝕜 = ℂ, ℝ, referred to as
E. We define an orthonormal_basis 𝕜 ι E as a linear isometric equivalence
between E and euclidean_space 𝕜 ι. Then std_orthonormal_basis 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.to_orthonormal_basis). We show that
orthonormal bases for each summand in a direct sum of spaces can be combined into an orthonormal
basis for the the whole sum in direct_sum.submodule_is_internal.subordinate_orthonormal_basis. In
the last section, various properties of matrices are explored.
Main definitions #
-
euclidean_space 𝕜 n: defined to bepi_Lp 2 (n → 𝕜)for anyfintype n, i.e., the space from functions tonto𝕜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_basisfor a finite-dimensional Euclidean space from abasiswhich isorthonormal. -
orthonormal.exists_orthonormal_basis_extension: provides an existential result of anorthonormal_basisextending a given orthonormal set -
exists_orthonormal_basis: provides an orthonormal basis on a finite dimensional vector space -
std_orthonormal_basis: provides an arbitrarily-chosenorthonormal_basisof a given finite dimensional inner product space
For consequences in infinite dimension (Hilbert bases, etc.), see the file
analysis.inner_product_space.l2_space.
@[protected, instance]
noncomputable
def
pi_Lp.inner_product_space
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{ι : Type u_1}
[fintype ι]
(f : ι → Type u_2)
[Π (i : ι), inner_product_space 𝕜 (f i)] :
inner_product_space 𝕜 (pi_Lp 2 f)
Equations
- pi_Lp.inner_product_space f = {to_normed_add_comm_group := infer_instance (pi_Lp.normed_add_comm_group 2 f), 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 := _}
@[simp]
theorem
pi_Lp.inner_apply
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{ι : Type u_1}
[fintype ι]
{f : ι → Type u_2}
[Π (i : ι), inner_product_space 𝕜 (f i)]
(x y : pi_Lp 2 f) :
has_inner.inner x y = finset.univ.sum (λ (i : ι), has_inner.inner (x i) (y i))
@[nolint, reducible]
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), 𝕜)
theorem
euclidean_space.nnnorm_eq
{𝕜 : Type u_1}
[is_R_or_C 𝕜]
{n : Type u_2}
[fintype n]
(x : euclidean_space 𝕜 n) :
‖x‖₊ = ⇑nnreal.sqrt (finset.univ.sum (λ (i : n), ‖x i‖₊ ^ 2))
theorem
euclidean_space.dist_eq
{𝕜 : Type u_1}
[is_R_or_C 𝕜]
{n : Type u_2}
[fintype n]
(x y : euclidean_space 𝕜 n) :
has_dist.dist x y = real.sqrt (finset.univ.sum (λ (i : n), has_dist.dist (x i) (y i) ^ 2))
theorem
euclidean_space.nndist_eq
{𝕜 : Type u_1}
[is_R_or_C 𝕜]
{n : Type u_2}
[fintype n]
(x y : euclidean_space 𝕜 n) :
has_nndist.nndist x y = ⇑nnreal.sqrt (finset.univ.sum (λ (i : n), has_nndist.nndist (x i) (y i) ^ 2))
theorem
euclidean_space.edist_eq
{𝕜 : Type u_1}
[is_R_or_C 𝕜]
{n : Type u_2}
[fintype n]
(x y : euclidean_space 𝕜 n) :
has_edist.edist x y = finset.univ.sum (λ (i : n), has_edist.edist (x i) (y i) ^ 2) ^ (1 / 2)
@[protected, instance]
def
euclidean_space.finite_dimensional
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
[fintype ι] :
finite_dimensional 𝕜 (euclidean_space 𝕜 ι)
@[protected, instance]
noncomputable
def
euclidean_space.inner_product_space
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
[fintype ι] :
inner_product_space 𝕜 (euclidean_space 𝕜 ι)
Equations
- euclidean_space.inner_product_space = pi_Lp.inner_product_space (λ (i : ι), 𝕜)
@[simp]
theorem
finrank_euclidean_space_fin
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{n : ℕ} :
finite_dimensional.finrank 𝕜 (euclidean_space 𝕜 (fin n)) = n
theorem
euclidean_space.inner_eq_star_dot_product
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
[fintype ι]
(x y : euclidean_space 𝕜 ι) :
has_inner.inner x y = matrix.dot_product (has_star.star (⇑(pi_Lp.equiv 2 (λ (i : ι), 𝕜)) x)) (⇑(pi_Lp.equiv 2 (λ (i : ι), 𝕜)) y)
noncomputable
def
direct_sum.is_internal.isometry_L2_of_orthogonal_family
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
[decidable_eq ι]
{V : ι → submodule 𝕜 E}
(hV : direct_sum.is_internal V)
(hV' : orthogonal_family 𝕜 (λ (i : ι), (V i).subtypeₗᵢ)) :
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.coe_linear_map V) hV in (e₂.symm.trans e₁).isometry_of_inner _
@[simp]
theorem
direct_sum.is_internal.isometry_L2_of_orthogonal_family_symm_apply
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
[decidable_eq ι]
{V : ι → submodule 𝕜 E}
(hV : direct_sum.is_internal V)
(hV' : orthogonal_family 𝕜 (λ (i : ι), (V i).subtypeₗᵢ))
(w : pi_Lp 2 (λ (i : ι), ↥(V i))) :
⇑((hV.isometry_L2_of_orthogonal_family hV').symm) w = finset.univ.sum (λ (i : ι), ↑(w i))
noncomputable
def
euclidean_space.equiv
(ι : Type u_1)
(𝕜 : Type u_3)
[is_R_or_C 𝕜]
[fintype ι] :
euclidean_space 𝕜 ι ≃L[𝕜] ι → 𝕜
pi_Lp.linear_equiv upgraded to a continuous linear map between euclidean_space 𝕜 ι
and ι → 𝕜.
Equations
- euclidean_space.equiv ι 𝕜 = (pi_Lp.linear_equiv 2 𝕜 (λ (i : ι), 𝕜)).to_continuous_linear_equiv
@[simp]
theorem
euclidean_space.equiv_to_linear_equiv_apply
(ι : Type u_1)
(𝕜 : Type u_3)
[is_R_or_C 𝕜]
[fintype ι]
(ᾰ : pi_Lp 2 (λ (i : ι), 𝕜))
(i : ι) :
⇑((euclidean_space.equiv ι 𝕜).to_linear_equiv) ᾰ i = ᾰ i
@[simp]
theorem
euclidean_space.equiv_apply
(ι : Type u_1)
(𝕜 : Type u_3)
[is_R_or_C 𝕜]
[fintype ι]
(ᾰ : pi_Lp 2 (λ (i : ι), 𝕜))
(i : ι) :
⇑(euclidean_space.equiv ι 𝕜) ᾰ i = ᾰ i
@[simp]
theorem
euclidean_space.equiv_symm_apply
(ι : Type u_1)
(𝕜 : Type u_3)
[is_R_or_C 𝕜]
[fintype ι]
(ᾰ : Π (i : ι), (λ (i : ι), 𝕜) i) :
⇑((euclidean_space.equiv ι 𝕜).symm) ᾰ = ⇑((pi_Lp.equiv 2 (λ (i : ι), 𝕜)).symm) ᾰ
@[simp]
theorem
euclidean_space.equiv_to_linear_equiv_symm_apply
(ι : Type u_1)
(𝕜 : Type u_3)
[is_R_or_C 𝕜]
[fintype ι]
(ᾰ : Π (i : ι), (λ (i : ι), 𝕜) i) :
⇑((euclidean_space.equiv ι 𝕜).to_linear_equiv.symm) ᾰ = ⇑((pi_Lp.equiv 2 (λ (i : ι), 𝕜)).symm) ᾰ
noncomputable
def
euclidean_space.projₗ
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
[fintype ι]
(i : ι) :
euclidean_space 𝕜 ι →ₗ[𝕜] 𝕜
The projection on the i-th coordinate of euclidean_space 𝕜 ι, as a linear map.
Equations
- euclidean_space.projₗ i = (linear_map.proj i).comp ↑(pi_Lp.linear_equiv 2 𝕜 (λ (i : ι), 𝕜))
@[simp]
theorem
euclidean_space.projₗ_apply
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
[fintype ι]
(i : ι)
(ᾰ : euclidean_space 𝕜 ι) :
⇑(euclidean_space.projₗ i) ᾰ = ᾰ i
@[simp]
@[simp]
theorem
euclidean_space.proj_apply
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
[fintype ι]
(i : ι)
(ᾰ : euclidean_space 𝕜 ι) :
⇑(euclidean_space.proj i) ᾰ = ᾰ i
noncomputable
def
euclidean_space.proj
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
[fintype ι]
(i : ι) :
euclidean_space 𝕜 ι →L[𝕜] 𝕜
The projection on the i-th coordinate of euclidean_space 𝕜 ι,
as a continuous linear map.
Equations
- euclidean_space.proj i = {to_linear_map := euclidean_space.projₗ i, cont := _}
noncomputable
def
euclidean_space.single
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
[fintype ι]
[decidable_eq ι]
(i : ι)
(a : 𝕜) :
euclidean_space 𝕜 ι
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_Lp.equiv 2 (λ (i : ι), 𝕜)).symm) (pi.single i a)
@[simp]
theorem
pi_Lp.equiv_single
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
[fintype ι]
[decidable_eq ι]
(i : ι)
(a : 𝕜) :
⇑(pi_Lp.equiv 2 (λ (i : ι), 𝕜)) (euclidean_space.single i a) = pi.single i a
@[simp]
theorem
pi_Lp.equiv_symm_single
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
[fintype ι]
[decidable_eq ι]
(i : ι)
(a : 𝕜) :
⇑((pi_Lp.equiv 2 (λ (i : ι), 𝕜)).symm) (pi.single i a) = euclidean_space.single i a
@[simp]
theorem
euclidean_space.single_apply
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
[fintype ι]
[decidable_eq ι]
(i : ι)
(a : 𝕜)
(j : ι) :
euclidean_space.single i a j = ite (j = i) a 0
theorem
euclidean_space.inner_single_left
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
[fintype ι]
[decidable_eq ι]
(i : ι)
(a : 𝕜)
(v : euclidean_space 𝕜 ι) :
has_inner.inner (euclidean_space.single i a) v = ⇑(star_ring_end 𝕜) a * v i
theorem
euclidean_space.inner_single_right
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
[fintype ι]
[decidable_eq ι]
(i : ι)
(a : 𝕜)
(v : euclidean_space 𝕜 ι) :
has_inner.inner v (euclidean_space.single i a) = a * ⇑(star_ring_end ((λ (i : ι), 𝕜) i)) (v i)
theorem
euclidean_space.pi_Lp_congr_left_single
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
[fintype ι]
[decidable_eq ι]
{ι' : Type u_2}
[fintype ι']
[decidable_eq ι']
(e : ι' ≃ ι)
(i' : ι') :
⇑(linear_isometry_equiv.pi_Lp_congr_left 2 𝕜 𝕜 e) (euclidean_space.single i' 1) = euclidean_space.single (⇑e i') 1
structure
orthonormal_basis
(ι : Type u_1)
(𝕜 : Type u_3)
[is_R_or_C 𝕜]
(E : Type u_4)
[inner_product_space 𝕜 E]
[fintype ι] :
Type (max u_1 u_3 u_4)
- 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
@[protected, instance]
noncomputable
def
orthonormal_basis.inhabited
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
[fintype ι] :
inhabited (orthonormal_basis ι 𝕜 (euclidean_space 𝕜 ι))
Equations
@[protected, instance]
noncomputable
def
orthonormal_basis.has_coe_to_fun
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι] :
has_coe_to_fun (orthonormal_basis ι 𝕜 E) (λ (_x : orthonormal_basis ι 𝕜 E), ι → E)
b i is the ith basis vector.
Equations
- orthonormal_basis.has_coe_to_fun = {coe := λ (b : orthonormal_basis ι 𝕜 E) (i : ι), ⇑(b.repr.symm) (euclidean_space.single i 1)}
@[simp]
theorem
orthonormal_basis.coe_of_repr
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
[decidable_eq ι]
(e : E ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι) :
@[protected, simp]
theorem
orthonormal_basis.repr_symm_single
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
[decidable_eq ι]
(b : orthonormal_basis ι 𝕜 E)
(i : ι) :
@[protected, simp]
theorem
orthonormal_basis.repr_self
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
[decidable_eq ι]
(b : orthonormal_basis ι 𝕜 E)
(i : ι) :
⇑(b.repr) (⇑b i) = euclidean_space.single i 1
@[protected]
theorem
orthonormal_basis.repr_apply_apply
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
(b : orthonormal_basis ι 𝕜 E)
(v : E)
(i : ι) :
⇑(b.repr) v i = has_inner.inner (⇑b i) v
@[protected, simp]
theorem
orthonormal_basis.orthonormal
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
(b : orthonormal_basis ι 𝕜 E) :
orthonormal 𝕜 ⇑b
@[protected]
noncomputable
def
orthonormal_basis.to_basis
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
(b : orthonormal_basis ι 𝕜 E) :
basis ι 𝕜 E
The basis ι 𝕜 E underlying the orthonormal_basis
Equations
@[protected, simp]
theorem
orthonormal_basis.coe_to_basis
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
(b : orthonormal_basis ι 𝕜 E) :
@[protected, simp]
theorem
orthonormal_basis.coe_to_basis_repr
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
(b : orthonormal_basis ι 𝕜 E) :
@[protected]
theorem
orthonormal_basis.sum_repr
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
(b : orthonormal_basis ι 𝕜 E)
(x : E) :
@[protected]
theorem
orthonormal_basis.sum_repr_symm
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
(b : orthonormal_basis ι 𝕜 E)
(v : euclidean_space 𝕜 ι) :
@[protected]
theorem
orthonormal_basis.sum_inner_mul_inner
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
(b : orthonormal_basis ι 𝕜 E)
(x y : E) :
finset.univ.sum (λ (i : ι), has_inner.inner x (⇑b i) * has_inner.inner (⇑b i) y) = has_inner.inner x y
@[protected]
theorem
orthonormal_basis.orthogonal_projection_eq_sum
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
{U : submodule 𝕜 E}
[complete_space ↥U]
(b : orthonormal_basis ι 𝕜 ↥U)
(x : E) :
⇑(orthogonal_projection U) x = finset.univ.sum (λ (i : ι), has_inner.inner ↑(⇑b i) x • ⇑b i)
@[protected]
noncomputable
def
orthonormal_basis.map
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
{G : Type u_2}
[inner_product_space 𝕜 G]
(b : orthonormal_basis ι 𝕜 E)
(L : E ≃ₗᵢ[𝕜] G) :
orthonormal_basis ι 𝕜 G
Mapping an orthonormal basis along a linear_isometry_equiv.
@[protected, simp]
theorem
orthonormal_basis.map_apply
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
{G : Type u_2}
[inner_product_space 𝕜 G]
(b : orthonormal_basis ι 𝕜 E)
(L : E ≃ₗᵢ[𝕜] G)
(i : ι) :
@[protected, simp]
theorem
orthonormal_basis.to_basis_map
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
{G : Type u_2}
[inner_product_space 𝕜 G]
(b : orthonormal_basis ι 𝕜 E)
(L : E ≃ₗᵢ[𝕜] G) :
noncomputable
def
basis.to_orthonormal_basis
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
(v : basis ι 𝕜 E)
(hv : orthonormal 𝕜 ⇑v) :
orthonormal_basis ι 𝕜 E
A basis that is orthonormal is an orthonormal basis.
Equations
- v.to_orthonormal_basis hv = {repr := v.equiv_fun.isometry_of_inner _}
@[simp]
theorem
basis.coe_to_orthonormal_basis_repr
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
(v : basis ι 𝕜 E)
(hv : orthonormal 𝕜 ⇑v) :
@[simp]
theorem
basis.coe_to_orthonormal_basis_repr_symm
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
(v : basis ι 𝕜 E)
(hv : orthonormal 𝕜 ⇑v) :
@[simp]
theorem
basis.to_basis_to_orthonormal_basis
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
(v : basis ι 𝕜 E)
(hv : orthonormal 𝕜 ⇑v) :
(v.to_orthonormal_basis hv).to_basis = v
@[simp]
theorem
basis.coe_to_orthonormal_basis
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
(v : basis ι 𝕜 E)
(hv : orthonormal 𝕜 ⇑v) :
⇑(v.to_orthonormal_basis hv) = ⇑v
@[protected]
noncomputable
def
orthonormal_basis.mk
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
{v : ι → E}
(hon : orthonormal 𝕜 v)
(hsp : ⊤ ≤ submodule.span 𝕜 (set.range v)) :
orthonormal_basis ι 𝕜 E
A finite orthonormal set that spans is an orthonormal basis
Equations
- orthonormal_basis.mk hon hsp = (basis.mk _ hsp).to_orthonormal_basis _
@[protected, simp]
theorem
orthonormal_basis.coe_mk
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
{v : ι → E}
(hon : orthonormal 𝕜 v)
(hsp : ⊤ ≤ submodule.span 𝕜 (set.range v)) :
⇑(orthonormal_basis.mk hon hsp) = v
@[protected]
noncomputable
def
orthonormal_basis.span
{ι' : Type u_2}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[decidable_eq E]
{v' : ι' → E}
(h : orthonormal 𝕜 v')
(s : finset ι') :
orthonormal_basis ↥s 𝕜 ↥(submodule.span 𝕜 ↑(finset.image v' s))
Any finite subset of a orthonormal family is an orthonormal_basis for its span.
Equations
- orthonormal_basis.span h s = let e₀' : basis ↥s 𝕜 ↥(submodule.span 𝕜 (set.range (v' ∘ coe))) := basis.span _, e₀ : orthonormal_basis ↥s 𝕜 ↥(submodule.span 𝕜 (set.range (v' ∘ coe))) := orthonormal_basis.mk _ _, φ : ↥(submodule.span 𝕜 ↑(finset.image v' s)) ≃ₗᵢ[𝕜] ↥(submodule.span 𝕜 (set.range (v' ∘ coe))) := linear_isometry_equiv.of_eq (submodule.span 𝕜 ↑(finset.image v' s)) (submodule.span 𝕜 (set.range (v' ∘ coe))) _ in e₀.map φ.symm
@[protected, simp]
theorem
orthonormal_basis.span_apply
{ι' : Type u_2}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[decidable_eq E]
{v' : ι' → E}
(h : orthonormal 𝕜 v')
(s : finset ι')
(i : ↥s) :
↑(⇑(orthonormal_basis.span h s) i) = v' ↑i
@[protected]
noncomputable
def
orthonormal_basis.mk_of_orthogonal_eq_bot
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
{v : ι → E}
(hon : orthonormal 𝕜 v)
(hsp : (submodule.span 𝕜 (set.range v))ᗮ = ⊥) :
orthonormal_basis ι 𝕜 E
A finite orthonormal family of vectors whose span has trivial orthogonal complement is an orthonormal basis.
Equations
- orthonormal_basis.mk_of_orthogonal_eq_bot hon hsp = orthonormal_basis.mk hon _
@[protected, simp]
theorem
orthonormal_basis.coe_of_orthogonal_eq_bot_mk
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
{v : ι → E}
(hon : orthonormal 𝕜 v)
(hsp : (submodule.span 𝕜 (set.range v))ᗮ = ⊥) :
⇑(orthonormal_basis.mk_of_orthogonal_eq_bot hon hsp) = v
noncomputable
def
orthonormal_basis.reindex
{ι : Type u_1}
{ι' : Type u_2}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
[fintype ι']
(b : orthonormal_basis ι 𝕜 E)
(e : ι ≃ ι') :
orthonormal_basis ι' 𝕜 E
b.reindex (e : ι ≃ ι') is an orthonormal_basis indexed by ι'
@[protected, simp]
![1, I] is an orthonormal basis for ℂ considered as a real inner product space.
Equations
- complex.orthonormal_basis_one_I = complex.basis_one_I.to_orthonormal_basis complex.orthonormal_basis_one_I._proof_1
@[simp]
@[simp]
theorem
complex.orthonormal_basis_one_I_repr_symm_apply
(x : euclidean_space ℝ (fin 2)) :
⇑(complex.orthonormal_basis_one_I.repr.symm) x = ↑(x 0) + ↑(x 1) * is_R_or_C.I
@[simp]
noncomputable
def
complex.isometry_of_orthonormal
{F : Type u_6}
[inner_product_space ℝ F]
(v : orthonormal_basis (fin 2) ℝ F) :
The isometry between ℂ and a two-dimensional real inner product space given by a basis.
Equations
@[simp]
theorem
complex.map_isometry_of_orthonormal
{F : Type u_6}
[inner_product_space ℝ F]
{F' : Type u_7}
[inner_product_space ℝ F']
(v : orthonormal_basis (fin 2) ℝ F)
(f : F ≃ₗᵢ[ℝ] F') :
theorem
complex.isometry_of_orthonormal_symm_apply
{F : Type u_6}
[inner_product_space ℝ F]
(v : orthonormal_basis (fin 2) ℝ F)
(f : F) :
theorem
complex.isometry_of_orthonormal_apply
{F : Type u_6}
[inner_product_space ℝ F]
(v : orthonormal_basis (fin 2) ℝ F)
(z : ℂ) :
Matrix representation of an orthonormal basis with respect to another #
theorem
orthonormal_basis.to_matrix_orthonormal_basis_mem_unitary
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
[decidable_eq ι]
(a b : orthonormal_basis ι 𝕜 E) :
a.to_basis.to_matrix ⇑b ∈ matrix.unitary_group ι 𝕜
The change-of-basis matrix between two orthonormal bases a, b is a unitary matrix.
@[simp]
theorem
orthonormal_basis.det_to_matrix_orthonormal_basis
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
[decidable_eq ι]
(a b : orthonormal_basis ι 𝕜 E) :
The determinant of the change-of-basis matrix between two orthonormal bases a, b has
unit length.
theorem
orthonormal_basis.to_matrix_orthonormal_basis_mem_orthogonal
{ι : Type u_1}
{F : Type u_6}
[inner_product_space ℝ F]
[fintype ι]
[decidable_eq ι]
(a b : orthonormal_basis ι ℝ F) :
The change-of-basis matrix between two orthonormal bases a, b is an orthogonal matrix.
theorem
orthonormal_basis.det_to_matrix_orthonormal_basis_real
{ι : Type u_1}
{F : Type u_6}
[inner_product_space ℝ F]
[fintype ι]
[decidable_eq ι]
(a b : orthonormal_basis ι ℝ F) :
The determinant of the change-of-basis matrix between two orthonormal bases a, b is ±1.
Existence of orthonormal basis, etc. #
noncomputable
def
direct_sum.is_internal.collected_orthonormal_basis
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
{A : ι → submodule 𝕜 E}
(hV : orthogonal_family 𝕜 (λ (i : ι), (A i).subtypeₗᵢ))
[decidable_eq ι]
(hV_sum : direct_sum.is_internal (λ (i : ι), A i))
{α : ι → Type u_2}
[Π (i : ι), fintype (α i)]
(v_family : Π (i : ι), orthonormal_basis (α i) 𝕜 ↥(A i)) :
orthonormal_basis (Σ (i : ι), α i) 𝕜 E
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
- direct_sum.is_internal.collected_orthonormal_basis hV hV_sum v_family = (hV_sum.collected_basis (λ (i : ι), (v_family i).to_basis)).to_orthonormal_basis _
theorem
direct_sum.is_internal.collected_orthonormal_basis_mem
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
{A : ι → submodule 𝕜 E}
[decidable_eq ι]
(h : direct_sum.is_internal A)
{α : ι → Type u_2}
[Π (i : ι), fintype (α i)]
(hV : orthogonal_family 𝕜 (λ (i : ι), (A i).subtypeₗᵢ))
(v : Π (i : ι), orthonormal_basis (α i) 𝕜 ↥(A i))
(a : Σ (i : ι), α i) :
⇑(direct_sum.is_internal.collected_orthonormal_basis hV h v) a ∈ A a.fst
theorem
orthonormal.exists_orthonormal_basis_extension
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
{v : set E}
[finite_dimensional 𝕜 E]
(hv : orthonormal 𝕜 coe) :
In a finite-dimensional inner_product_space, any orthonormal subset can be extended to an
orthonormal basis.
theorem
orthonormal.exists_orthonormal_basis_extension_of_card_eq
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[finite_dimensional 𝕜 E]
{ι : Type u_1}
[fintype ι]
(card_ι : finite_dimensional.finrank 𝕜 E = fintype.card ι)
{v : ι → E}
{s : set ι}
(hv : orthonormal 𝕜 (s.restrict v)) :
theorem
exists_orthonormal_basis
(𝕜 : Type u_3)
[is_R_or_C 𝕜]
(E : Type u_4)
[inner_product_space 𝕜 E]
[finite_dimensional 𝕜 E] :
A finite-dimensional inner product space admits an orthonormal basis.
@[irreducible]
noncomputable
def
std_orthonormal_basis
(𝕜 : Type u_3)
[is_R_or_C 𝕜]
(E : Type u_4)
[inner_product_space 𝕜 E]
[finite_dimensional 𝕜 E] :
orthonormal_basis (fin (finite_dimensional.finrank 𝕜 E)) 𝕜 E
A finite-dimensional inner_product_space has an orthonormal basis.
Equations
- std_orthonormal_basis 𝕜 E = let b : orthonormal_basis ↥(classical.some _) 𝕜 E := classical.some _ in _.mpr (b.reindex (fintype.equiv_fin_of_card_eq _))
@[irreducible]
noncomputable
def
direct_sum.is_internal.sigma_orthonormal_basis_index_equiv
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
[finite_dimensional 𝕜 E]
{n : ℕ}
(hn : finite_dimensional.finrank 𝕜 E = n)
[decidable_eq ι]
{V : ι → submodule 𝕜 E}
(hV : direct_sum.is_internal V)
(hV' : orthogonal_family 𝕜 (λ (i : ι), (V i).subtypeₗᵢ)) :
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.
Equations
- direct_sum.is_internal.sigma_orthonormal_basis_index_equiv hn hV hV' = let b : orthonormal_basis (Σ (i : ι), fin (finite_dimensional.finrank 𝕜 ↥(V i))) 𝕜 E := direct_sum.is_internal.collected_orthonormal_basis hV' hV (λ (i : ι), std_orthonormal_basis 𝕜 ↥(V i)) in fintype.equiv_fin_of_card_eq _
@[irreducible]
noncomputable
def
direct_sum.is_internal.subordinate_orthonormal_basis
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
[finite_dimensional 𝕜 E]
{n : ℕ}
(hn : finite_dimensional.finrank 𝕜 E = n)
[decidable_eq ι]
{V : ι → submodule 𝕜 E}
(hV : direct_sum.is_internal V)
(hV' : orthogonal_family 𝕜 (λ (i : ι), (V i).subtypeₗᵢ)) :
orthonormal_basis (fin n) 𝕜 E
An n-dimensional inner_product_space equipped with a decomposition as an internal direct
sum has an orthonormal basis indexed by fin n and subordinate to that direct sum.
Equations
- direct_sum.is_internal.subordinate_orthonormal_basis hn hV hV' = (direct_sum.is_internal.collected_orthonormal_basis hV' hV (λ (i : ι), std_orthonormal_basis 𝕜 ↥(V i))).reindex (direct_sum.is_internal.sigma_orthonormal_basis_index_equiv hn hV hV')
@[irreducible]
noncomputable
def
direct_sum.is_internal.subordinate_orthonormal_basis_index
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
[finite_dimensional 𝕜 E]
{n : ℕ}
(hn : finite_dimensional.finrank 𝕜 E = n)
[decidable_eq ι]
{V : ι → submodule 𝕜 E}
(hV : direct_sum.is_internal V)
(a : fin n)
(hV' : orthogonal_family 𝕜 (λ (i : ι), (V i).subtypeₗᵢ)) :
ι
An n-dimensional inner_product_space 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.
Equations
- direct_sum.is_internal.subordinate_orthonormal_basis_index hn hV a hV' = (⇑((direct_sum.is_internal.sigma_orthonormal_basis_index_equiv hn hV hV').symm) a).fst
theorem
direct_sum.is_internal.subordinate_orthonormal_basis_subordinate
{ι : Type u_1}
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
[fintype ι]
[finite_dimensional 𝕜 E]
{n : ℕ}
(hn : finite_dimensional.finrank 𝕜 E = n)
[decidable_eq ι]
{V : ι → submodule 𝕜 E}
(hV : direct_sum.is_internal V)
(a : fin n)
(hV' : orthogonal_family 𝕜 (λ (i : ι), (V i).subtypeₗᵢ)) :
⇑(direct_sum.is_internal.subordinate_orthonormal_basis hn hV hV') a ∈ V (direct_sum.is_internal.subordinate_orthonormal_basis_index hn hV a hV')
The basis constructed in orthogonal_family.subordinate_orthonormal_basis is subordinate to
the orthogonal_family in question.
noncomputable
def
orthonormal_basis.from_orthogonal_span_singleton
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{E : Type u_4}
[inner_product_space 𝕜 E]
(n : ℕ)
[fact (finite_dimensional.finrank 𝕜 E = n + 1)]
{v : E}
(hv : v ≠ 0) :
orthonormal_basis (fin n) 𝕜 ↥(submodule.span 𝕜 {v})ᗮ
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).
Equations
- orthonormal_basis.from_orthogonal_span_singleton n hv = (std_orthonormal_basis 𝕜 ↥(submodule.span 𝕜 {v})ᗮ).reindex (fin_congr _)
noncomputable
def
linear_isometry.extend
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{V : Type u_8}
[inner_product_space 𝕜 V]
[finite_dimensional 𝕜 V]
{S : submodule 𝕜 V}
(L : ↥S →ₗᵢ[𝕜] V) :
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 := linear_map.range L.to_linear_map, L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp ((std_orthonormal_basis 𝕜 ↥Sᗮ).repr.trans ((std_orthonormal_basis 𝕜 ↥LSᗮ).reindex (fin_congr _)).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' := _}
theorem
inner_matrix_row_row
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{n m : ℕ}
(A B : matrix (fin n) (fin m) 𝕜)
(i j : fin n) :
has_inner.inner (A i) (B j) = B.mul A.conj_transpose j i
The inner product of a row of A and a row of B is an entry of B ⬝ Aᴴ.
theorem
inner_matrix_col_col
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{n m : ℕ}
(A B : matrix (fin n) (fin m) 𝕜)
(i j : fin m) :
has_inner.inner (A.transpose i) (B.transpose j) = A.conj_transpose.mul B i j
The inner product of a column of A and a column of B is an entry of Aᴴ ⬝ B