# `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 be `PiLp 2 (n → 𝕜)` for any `Fintype n`, i.e., the space from functions to `n` to `𝕜` with the `L²` norm. We register several instances on it (notably that it is a finite-dimensional inner product space), and provide a `!ₚ[]` notation (for numeric subscripts like `₂`) for the case when the indexing type is `Fin n`.

- `OrthonormalBasis 𝕜 ι`: defined to be an isometry to Euclidean space from a given finite-dimensional inner product space, `E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι`.

- `Basis.toOrthonormalBasis`: constructs an `OrthonormalBasis` for a finite-dimensional Euclidean space from a `Basis` which is `Orthonormal`.

- `Orthonormal.exists_orthonormalBasis_extension`: provides an existential result of an `OrthonormalBasis` extending a given orthonormal set

- `exists_orthonormalBasis`: provides an orthonormal basis on a finite-dimensional vector space

- `stdOrthonormalBasis`: provides an arbitrarily-chosen `OrthonormalBasis` of a given finite-dimensional inner product space

For consequences in infinite dimension (Hilbert bases, etc.), see the file `Analysis.InnerProductSpace.L2Space`.

source
instance PiLp.innerProductSpace {𝕜 : Type u_3} [RCLike 𝕜] {ι : Type u_7} [Fintype ι] (f : ι → Type u_8) [(i : ι) → NormedAddCommGroup (f i)] [(i : ι) → InnerProductSpace 𝕜 (f i)] :
InnerProductSpace 𝕜 (PiLp 2 f)
Equations

- One or more equations did not get rendered due to their size.

source
theorem PiLp.inner_apply {𝕜 : Type u_3} [RCLike 𝕜] {ι : Type u_7} [Fintype ι] {f : ι → Type u_8} [(i : ι) → NormedAddCommGroup (f i)] [(i : ι) → InnerProductSpace 𝕜 (f i)] (x y : PiLp 2 f) :
inner 𝕜 x y = ∑ i : ι, inner 𝕜 (x.ofLp i) (y.ofLp i)
source
@[reducible, inline]
abbrev EuclideanSpace (𝕜 : Type u_7) (n : Type u_8) :
Type (max u_7 u_8)

The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type, analogous to `![x, y, ...]` notation.

Equations

- EuclideanSpace 𝕜 n = PiLp 2 fun (x : n) => 𝕜

Instances For

source
def PiLp.vecNotation :
Lean.ParserDescr

Notation for vectors in Lp space. `!₂[x, y, ...]` is a shorthand for `WithLp.toLp 2 ![x, y, ...]`, of type `EuclideanSpace _ (Fin _)`.

This also works for other subscripts.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def EuclideanSpace.delabVecNotation :
Lean.PrettyPrinter.Delaborator.Delab

Unexpander for the `!₂[x, y, ...]` notation.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem EuclideanSpace.nnnorm_eq {𝕜 : Type u_7} [RCLike 𝕜] {n : Type u_8} [Fintype n] (x : EuclideanSpace 𝕜 n) :
‖x‖₊ = NNReal.sqrt (∑ i : n, ‖x.ofLp i‖₊ ^ 2)
source
theorem EuclideanSpace.norm_eq {𝕜 : Type u_7} [RCLike 𝕜] {n : Type u_8} [Fintype n] (x : EuclideanSpace 𝕜 n) :
‖x‖ = √(∑ i : n, ‖x.ofLp i‖ ^ 2)
source
theorem EuclideanSpace.norm_sq_eq {𝕜 : Type u_7} [RCLike 𝕜] {n : Type u_8} [Fintype n] (x : EuclideanSpace 𝕜 n) :
‖x‖ ^ 2 = ∑ i : n, ‖x.ofLp i‖ ^ 2
source
theorem EuclideanSpace.dist_eq {𝕜 : Type u_7} [RCLike 𝕜] {n : Type u_8} [Fintype n] (x y : EuclideanSpace 𝕜 n) :
dist x y = √(∑ i : n, dist (x.ofLp i) (y.ofLp i) ^ 2)
source
theorem EuclideanSpace.dist_sq_eq {𝕜 : Type u_7} [RCLike 𝕜] {n : Type u_8} [Fintype n] (x y : EuclideanSpace 𝕜 n) :
dist x y ^ 2 = ∑ i : n, dist (x.ofLp i) (y.ofLp i) ^ 2
source
theorem EuclideanSpace.nndist_eq {𝕜 : Type u_7} [RCLike 𝕜] {n : Type u_8} [Fintype n] (x y : EuclideanSpace 𝕜 n) :
nndist x y = NNReal.sqrt (∑ i : n, nndist (x.ofLp i) (y.ofLp i) ^ 2)
source
theorem EuclideanSpace.edist_eq {𝕜 : Type u_7} [RCLike 𝕜] {n : Type u_8} [Fintype n] (x y : EuclideanSpace 𝕜 n) :
edist x y = (∑ i : n, edist (x.ofLp i) (y.ofLp i) ^ 2) ^ (1 / 2)
source
theorem EuclideanSpace.ball_zero_eq {n : Type u_7} [Fintype n] (r : ℝ) (hr : 0 ≤ r) :
Metric.ball 0 r = {x : EuclideanSpace ℝ n | ∑ i : n, x.ofLp i ^ 2 < r ^ 2}
source
theorem EuclideanSpace.closedBall_zero_eq {n : Type u_7} [Fintype n] (r : ℝ) (hr : 0 ≤ r) :
Metric.closedBall 0 r = {x : EuclideanSpace ℝ n | ∑ i : n, x.ofLp i ^ 2 ≤ r ^ 2}
source
theorem EuclideanSpace.sphere_zero_eq {n : Type u_7} [Fintype n] (r : ℝ) (hr : 0 ≤ r) :
Metric.sphere 0 r = {x : EuclideanSpace ℝ n | ∑ i : n, x.ofLp i ^ 2 = r ^ 2}
source
@[simp]
theorem finrank_euclideanSpace {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [Fintype ι] :
Module.finrank 𝕜 (EuclideanSpace 𝕜 ι) = Fintype.card ι
source
theorem finrank_euclideanSpace_fin {𝕜 : Type u_3} [RCLike 𝕜] {n : ℕ} :
Module.finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n
source
theorem EuclideanSpace.inner_eq_star_dotProduct {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [Fintype ι] (x y : EuclideanSpace 𝕜 ι) :
inner 𝕜 x y = y.ofLp ⬝ᵥ star x.ofLp
source
theorem EuclideanSpace.inner_toLp_toLp {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [Fintype ι] (x y : ι → 𝕜) :
inner 𝕜 (WithLp.toLp 2 x) (WithLp.toLp 2 y) = y ⬝ᵥ star x
source
def DirectSum.IsInternal.isometryL2OfOrthogonalFamily {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) :
E ≃ₗᵢ[𝕜] PiLp 2 fun (i : ι) => ↥(V i)

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

source
@[simp]
theorem DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) (w : PiLp 2 fun (i : ι) => ↥(V i)) :
(hV.isometryL2OfOrthogonalFamily hV').symm w = ∑ i : ι, ↑(w.ofLp i)
source
@[reducible, inline]
abbrev EuclideanSpace.equiv (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] :
EuclideanSpace 𝕜 ι ≃L[𝕜] ι → 𝕜

A shorthand for `PiLp.continuousLinearEquiv`.

Equations

- EuclideanSpace.equiv ι 𝕜 = PiLp.continuousLinearEquiv 2 𝕜 fun (x : ι) => 𝕜

Instances For

source
@[reducible, inline]
abbrev EuclideanSpace.projₗ {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] (i : ι) :
EuclideanSpace 𝕜 ι →ₗ[𝕜] 𝕜

The projection on the `i`-th coordinate of `EuclideanSpace 𝕜 ι`, as a linear map.

Equations

- EuclideanSpace.projₗ i = PiLp.projₗ 2 (fun (x : ι) => 𝕜) i

Instances For

source
@[reducible, inline]
abbrev EuclideanSpace.proj {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] (i : ι) :
StrongDual 𝕜 (EuclideanSpace 𝕜 ι)

The projection on the `i`-th coordinate of `EuclideanSpace 𝕜 ι`, as a continuous linear map.

Equations

- EuclideanSpace.proj i = PiLp.proj 2 (fun (x : ι) => 𝕜) i

Instances For

source
def EuclideanSpace.single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] (i : ι) (a : 𝕜) :
EuclideanSpace 𝕜 ι

The vector given in Euclidean space by being `a : 𝕜` at coordinate `i : ι` and `0 : 𝕜` at all other coordinates.

Equations

- EuclideanSpace.single i a = WithLp.toLp 2 (Pi.single i a)

Instances For

source
@[simp]
theorem EuclideanSpace.ofLp_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] (i : ι) (a : 𝕜) :
(single i a).ofLp = Pi.single i a
source
@[simp]
theorem EuclideanSpace.toLp_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] (i : ι) (a : 𝕜) :
WithLp.toLp 2 (Pi.single i a) = single i a
source
@[simp]
theorem EuclideanSpace.single_apply {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] (i : ι) (a : 𝕜) (j : ι) :
(single i a).ofLp j = if j = i then a else 0
source
@[simp]
theorem EuclideanSpace.single_eq_zero_iff {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] {i : ι} {a : 𝕜} :
single i a = 0 ↔ a = 0
source
theorem EuclideanSpace.inner_single_left {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι) :
inner 𝕜 (single i a) v = (starRingEnd 𝕜) a * v.ofLp i
source
theorem EuclideanSpace.inner_single_right {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι) :
inner 𝕜 v (single i a) = a * (starRingEnd ((fun (x : ι) => 𝕜) i)) (v.ofLp i)
source
@[simp]
theorem EuclideanSpace.norm_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) :
‖single i a‖ = ‖a‖
source
@[simp]
theorem EuclideanSpace.nnnorm_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) :
‖single i a‖₊ = ‖a‖₊
source
@[simp]
theorem EuclideanSpace.dist_single_same {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a b : 𝕜) :
dist (single i a) (single i b) = dist a b
source
@[simp]
theorem EuclideanSpace.nndist_single_same {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a b : 𝕜) :
nndist (single i a) (single i b) = nndist a b
source
@[simp]
theorem EuclideanSpace.edist_single_same {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a b : 𝕜) :
edist (single i a) (single i b) = edist a b
source
theorem EuclideanSpace.orthonormal_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] :
Orthonormal 𝕜 fun (i : ι) => single i 1

`EuclideanSpace.single` forms an orthonormal family.

source
theorem EuclideanSpace.piLpCongrLeft_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] {ι' : Type u_7} [Fintype ι'] [DecidableEq ι'] (e : ι' ≃ ι) (i' : ι') (v : 𝕜) :
(LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) (single i' v) = single (e i') v
source
@[reducible, inline]
abbrev EuclideanSpace.sumEquivProd {𝕜 : Type u_7} [RCLike 𝕜] {ι : Type u_8} {κ : Type u_9} [Fintype ι] [Fintype κ] :
EuclideanSpace 𝕜 (ι ⊕ κ) ≃L[𝕜] EuclideanSpace 𝕜 ι × EuclideanSpace 𝕜 κ

The canonical linear homeomorphism between `EuclideanSpace 𝕜 (ι ⊕ κ)` and `EuclideanSpace 𝕜 ι × EuclideanSpace 𝕜 κ`.

See `PiLp.sumPiLpEquivProdLpPiLp` for the isometry version, where the RHS is equipped with the Euclidean norm rather than the supremum norm.

Equations

- EuclideanSpace.sumEquivProd = (PiLp.sumPiLpEquivProdLpPiLp 2 fun (x : ι ⊕ κ) => 𝕜).toContinuousLinearEquiv.trans (WithLp.prodContinuousLinearEquiv 2 𝕜 (WithLp 2 (ι → 𝕜)) (WithLp 2 (κ → 𝕜)))

Instances For

source
@[reducible, inline]
abbrev EuclideanSpace.finAddEquivProd {𝕜 : Type u_7} [RCLike 𝕜] {n m : ℕ} :
EuclideanSpace 𝕜 (Fin (n + m)) ≃L[𝕜] EuclideanSpace 𝕜 (Fin n) × EuclideanSpace 𝕜 (Fin m)

The canonical linear homeomorphism between `EuclideanSpace 𝕜 (Fin (n + m))` and `EuclideanSpace 𝕜 (Fin n) × EuclideanSpace 𝕜 (Fin m)`.

Equations

- EuclideanSpace.finAddEquivProd = (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 finSumFinEquiv.symm).toContinuousLinearEquiv.trans EuclideanSpace.sumEquivProd

Instances For

source
structure OrthonormalBasis (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] (E : Type u_4) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] :
Type (max (max u_1 u_3) u_4)

An orthonormal basis on E is an identification of `E` with its dimensional-matching `EuclideanSpace 𝕜 ι`.

- ofRepr :: (

- repr : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι

  Linear isometry between `E` and `EuclideanSpace 𝕜 ι` representing the orthonormal basis.

- )

Instances For

source
theorem OrthonormalBasis.repr_injective {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] :
Function.Injective repr
source
instance OrthonormalBasis.instFunLike {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] :
FunLike (OrthonormalBasis ι 𝕜 E) ι E

`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' := ⋯ }

source
@[simp]
theorem OrthonormalBasis.coe_ofRepr {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι) :
⇑{ repr := e } = fun (i : ι) => e.symm (EuclideanSpace.single i 1)
source
@[simp]
theorem OrthonormalBasis.repr_symm_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι) :
b.repr.symm (EuclideanSpace.single i 1) = b i
source
@[simp]
theorem OrthonormalBasis.repr_self {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι) :
b.repr (b i) = EuclideanSpace.single i 1
source
theorem OrthonormalBasis.repr_apply_apply {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (v : E) (i : ι) :
(b.repr v).ofLp i = inner 𝕜 (b i) v
source
@[simp]
theorem OrthonormalBasis.orthonormal {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) :
Orthonormal 𝕜 ⇑b
source
@[simp]
theorem OrthonormalBasis.norm_eq_one {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι) :
‖b i‖ = 1
source
@[simp]
theorem OrthonormalBasis.nnnorm_eq_one {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι) :
‖b i‖₊ = 1
source
@[simp]
theorem OrthonormalBasis.enorm_eq_one {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι) :
‖b i‖ₑ = 1
source
@[simp]
theorem OrthonormalBasis.inner_eq_zero {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) {i j : ι} (hij : i ≠ j) :
inner 𝕜 (b i) (b j) = 0
source
theorem OrthonormalBasis.inner_eq_one {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι) :
inner 𝕜 (b i) (b i) = 1
source
theorem OrthonormalBasis.inner_eq_ite {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (i j : ι) :
inner 𝕜 (b i) (b j) = if i = j then 1 else 0
source
def OrthonormalBasis.toBasis {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) :
Module.Basis ι 𝕜 E

The `Basis ι 𝕜 E` underlying the `OrthonormalBasis`

Equations

- b.toBasis = Module.Basis.ofEquivFun (b.repr.trans (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)))

Instances For

source
@[simp]
theorem OrthonormalBasis.coe_toBasis {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) :
⇑b.toBasis = ⇑b
source
@[simp]
theorem OrthonormalBasis.coe_toBasis_repr {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) :
b.toBasis.equivFun = b.repr.toLinearEquiv ≪≫ₗ WithLp.linearEquiv 2 𝕜 (ι → 𝕜)
source
@[simp]
theorem OrthonormalBasis.coe_toBasis_repr_apply {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) (i : ι) :
(b.toBasis.repr x) i = (b.repr x).ofLp i
source
theorem OrthonormalBasis.sum_repr {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) :
∑ i : ι, (b.repr x).ofLp i • b i = x
source
theorem OrthonormalBasis.sum_repr' {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) :
∑ i : ι, inner 𝕜 (b i) x • b i = x
source
theorem OrthonormalBasis.sum_repr_symm {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (v : EuclideanSpace 𝕜 ι) :
∑ i : ι, v.ofLp i • b i = b.repr.symm v
source
theorem OrthonormalBasis.sum_inner_mul_inner {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x y : E) :
∑ i : ι, inner 𝕜 x (b i) * inner 𝕜 (b i) y = inner 𝕜 x y
source
theorem OrthonormalBasis.sum_sq_norm_inner_right {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) :
∑ i : ι, ‖inner 𝕜 (b i) x‖ ^ 2 = ‖x‖ ^ 2
source
@[deprecated OrthonormalBasis.sum_sq_norm_inner_right (since := "2025-06-23")]
theorem OrthonormalBasis.sum_sq_norm_inner {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) :
∑ i : ι, ‖inner 𝕜 (b i) x‖ ^ 2 = ‖x‖ ^ 2

Alias of `OrthonormalBasis.sum_sq_norm_inner_right`.

source
theorem OrthonormalBasis.sum_sq_norm_inner_left {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) :
∑ i : ι, ‖inner 𝕜 x (b i)‖ ^ 2 = ‖x‖ ^ 2
source
theorem OrthonormalBasis.sum_sq_inner_right {ι : Type u_1} [Fintype ι] {E : Type u_7} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (b : OrthonormalBasis ι ℝ E) (x : E) :
∑ i : ι, inner ℝ (b i) x ^ 2 = ‖x‖ ^ 2
source
theorem OrthonormalBasis.sum_sq_inner_left {ι : Type u_7} {E : Type u_8} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype ι] (b : OrthonormalBasis ι ℝ E) (x : E) :
∑ i : ι, inner ℝ x (b i) ^ 2 = ‖x‖ ^ 2
source
theorem OrthonormalBasis.norm_le_card_mul_iSup_norm_inner {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) :
‖x‖ ≤ √↑(Fintype.card ι) * ⨆ (i : ι), ‖inner 𝕜 (b i) x‖
source
theorem OrthonormalBasis.orthogonalProjection_eq_sum {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {U : Submodule 𝕜 E} [CompleteSpace ↥U] (b : OrthonormalBasis ι 𝕜 ↥U) (x : E) :
U.orthogonalProjection x = ∑ i : ι, inner 𝕜 (↑(b i)) x • b i
source
def OrthonormalBasis.map {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {G : Type u_7} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (b : OrthonormalBasis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G) :
OrthonormalBasis ι 𝕜 G

Mapping an orthonormal basis along a `LinearIsometryEquiv`.

Equations

- b.map L = { repr := L.symm.trans b.repr }

Instances For

source
@[simp]
theorem OrthonormalBasis.map_apply {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {G : Type u_7} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (b : OrthonormalBasis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G) (i : ι) :
(b.map L) i = L (b i)
source
@[simp]
theorem OrthonormalBasis.toBasis_map {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {G : Type u_7} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (b : OrthonormalBasis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G) :
(b.map L).toBasis = b.toBasis.map L.toLinearEquiv
source
def Module.Basis.toOrthonormalBasis {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 ⇑v) :
OrthonormalBasis ι 𝕜 E

A basis that is orthonormal is an orthonormal basis.

Equations

- v.toOrthonormalBasis hv = { repr := (v.equivFun.trans (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm).isometryOfInner ⋯ }

Instances For

source
@[simp]
theorem Module.Basis.coe_toOrthonormalBasis_repr {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 ⇑v) :
⇑(v.toOrthonormalBasis hv).repr = ⇑(v.equivFun ≪≫ₗ (WithLp.linearEquiv 2 𝕜 (ι → 𝕜)).symm)
source
@[simp]
theorem Module.Basis.coe_toOrthonormalBasis_repr_symm {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 ⇑v) :
⇑(v.toOrthonormalBasis hv).repr.symm = ⇑(WithLp.linearEquiv 2 𝕜 (ι → 𝕜) ≪≫ₗ v.equivFun.symm)
source
@[simp]
theorem Module.Basis.toBasis_toOrthonormalBasis {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 ⇑v) :
(v.toOrthonormalBasis hv).toBasis = v
source
@[simp]
theorem Module.Basis.coe_toOrthonormalBasis {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 ⇑v) :
⇑(v.toOrthonormalBasis hv) = ⇑v
source
noncomputable def OrthonormalBasis.singleton (ι : Type u_7) (𝕜 : Type u_8) [Unique ι] [RCLike 𝕜] :
OrthonormalBasis ι 𝕜 𝕜

`OrthonormalBasis.singleton ι 𝕜` is the orthonormal basis sending the unique element of `ι` to `1 : 𝕜`.

Equations

- OrthonormalBasis.singleton ι 𝕜 = (Module.Basis.singleton ι 𝕜).toOrthonormalBasis ⋯

Instances For

source
@[simp]
theorem OrthonormalBasis.singleton_apply {ι : Type u_7} {𝕜 : Type u_8} [Unique ι] [RCLike 𝕜] (i : ι) :
(OrthonormalBasis.singleton ι 𝕜) i = 1
source
@[simp]
theorem OrthonormalBasis.singleton_repr {ι : Type u_7} {𝕜 : Type u_8} [Unique ι] [RCLike 𝕜] (x : 𝕜) (i : ι) :
((OrthonormalBasis.singleton ι 𝕜).repr x).ofLp i = x
source
@[simp]
theorem OrthonormalBasis.coe_singleton {ι : Type u_7} {𝕜 : Type u_8} [Unique ι] [RCLike 𝕜] :
⇑(OrthonormalBasis.singleton ι 𝕜) = 1
source
@[simp]
theorem OrthonormalBasis.toBasis_singleton {ι : Type u_7} {𝕜 : Type u_8} [Unique ι] [RCLike 𝕜] :
(OrthonormalBasis.singleton ι 𝕜).toBasis = Module.Basis.singleton ι 𝕜
source
def Pi.orthonormalBasis {η : Type u_7} [Fintype η] {ι : η → Type u_8} [(i : η) → Fintype (ι i)] {𝕜 : Type u_9} [RCLike 𝕜] {E : η → Type u_10} [(i : η) → NormedAddCommGroup (E i)] [(i : η) → InnerProductSpace 𝕜 (E i)] (B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)) :
OrthonormalBasis ((i : η) × ι i) 𝕜 (PiLp 2 E)

`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_1 : ι x) => 𝕜).symm }

Instances For

source
theorem Pi.orthonormalBasis.toBasis {η : Type u_7} [Fintype η] {ι : η → Type u_8} [(i : η) → Fintype (ι i)] {𝕜 : Type u_9} [RCLike 𝕜] {E : η → Type u_10} [(i : η) → NormedAddCommGroup (E i)] [(i : η) → InnerProductSpace 𝕜 (E i)] (B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)) :
(Pi.orthonormalBasis B).toBasis = (Pi.basis fun (i : η) => (B i).toBasis).map (WithLp.linearEquiv 2 𝕜 ((j : η) → E j)).symm
source
@[simp]
theorem Pi.orthonormalBasis_apply {η : Type u_7} [Fintype η] [DecidableEq η] {ι : η → Type u_8} [(i : η) → Fintype (ι i)] {𝕜 : Type u_9} [RCLike 𝕜] {E : η → Type u_10} [(i : η) → NormedAddCommGroup (E i)] [(i : η) → InnerProductSpace 𝕜 (E i)] (B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)) (j : (i : η) × ι i) :
(Pi.orthonormalBasis B) j = WithLp.toLp 2 (single j.fst ((B j.fst) j.snd))
source
@[simp]
theorem Pi.orthonormalBasis_repr {η : Type u_7} [Fintype η] {ι : η → Type u_8} [(i : η) → Fintype (ι i)] {𝕜 : Type u_9} [RCLike 𝕜] {E : η → Type u_10} [(i : η) → NormedAddCommGroup (E i)] [(i : η) → InnerProductSpace 𝕜 (E i)] (B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)) (x : (i : η) → E i) (j : (i : η) × ι i) :
((Pi.orthonormalBasis B).repr (WithLp.toLp 2 x)).ofLp j = ((B j.fst).repr (x j.fst)).ofLp j.snd
source
def OrthonormalBasis.mk {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hon : Orthonormal 𝕜 v) (hsp : ⊤ ≤ Submodule.span 𝕜 (Set.range v)) :
OrthonormalBasis ι 𝕜 E

A finite orthonormal set that spans is an orthonormal basis

Equations

- OrthonormalBasis.mk hon hsp = (Module.Basis.mk ⋯ hsp).toOrthonormalBasis ⋯

Instances For

source
@[simp]
theorem OrthonormalBasis.coe_mk {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hon : Orthonormal 𝕜 v) (hsp : ⊤ ≤ Submodule.span 𝕜 (Set.range v)) :
⇑(OrthonormalBasis.mk hon hsp) = v
source
def OrthonormalBasis.span {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [DecidableEq E] {v' : ι' → E} (h : Orthonormal 𝕜 v') (s : Finset ι') :
OrthonormalBasis (↥s) 𝕜 ↥(Submodule.span 𝕜 ↑(Finset.image v' s))

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

source
@[simp]
theorem OrthonormalBasis.span_apply {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [DecidableEq E] {v' : ι' → E} (h : Orthonormal 𝕜 v') (s : Finset ι') (i : ↥s) :
↑((OrthonormalBasis.span h s) i) = v' ↑i
source
def OrthonormalBasis.mkOfOrthogonalEqBot {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hon : Orthonormal 𝕜 v) (hsp : (Submodule.span 𝕜 (Set.range v))ᗮ = ⊥) :
OrthonormalBasis ι 𝕜 E

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

source
@[simp]
theorem OrthonormalBasis.coe_of_orthogonal_eq_bot_mk {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {v : ι → E} (hon : Orthonormal 𝕜 v) (hsp : (Submodule.span 𝕜 (Set.range v))ᗮ = ⊥) :
⇑(OrthonormalBasis.mkOfOrthogonalEqBot hon hsp) = v
source
def OrthonormalBasis.reindex {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι') :
OrthonormalBasis ι' 𝕜 E

`b.reindex (e : ι ≃ ι')` is an `OrthonormalBasis` indexed by `ι'`

Equations

- b.reindex e = { repr := b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) }

Instances For

source
theorem OrthonormalBasis.reindex_apply {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι') (i' : ι') :
(b.reindex e) i' = b (e.symm i')
source
@[simp]
theorem OrthonormalBasis.reindex_toBasis {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι') :
(b.reindex e).toBasis = b.toBasis.reindex e
source
@[simp]
theorem OrthonormalBasis.coe_reindex {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι') :
⇑(b.reindex e) = ⇑b ∘ ⇑e.symm
source
@[simp]
theorem OrthonormalBasis.repr_reindex {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι') (x : E) (i' : ι') :
((b.reindex e).repr x).ofLp i' = (b.repr x).ofLp (e.symm i')
source
noncomputable def EuclideanSpace.basisFun (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] [Fintype ι] :
OrthonormalBasis ι 𝕜 (EuclideanSpace 𝕜 ι)

The basis `Pi.basisFun`, bundled as an orthornormal basis of `EuclideanSpace 𝕜 ι`.

Equations

- EuclideanSpace.basisFun ι 𝕜 = { repr := LinearIsometryEquiv.refl 𝕜 (EuclideanSpace 𝕜 ι) }

Instances For

source
@[simp]
theorem EuclideanSpace.basisFun_apply (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] [Fintype ι] [DecidableEq ι] (i : ι) :
(basisFun ι 𝕜) i = single i 1
source
@[simp]
theorem EuclideanSpace.basisFun_repr (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] [Fintype ι] (x : EuclideanSpace 𝕜 ι) (i : ι) :
((basisFun ι 𝕜).repr x).ofLp i = x.ofLp i
source
@[simp]
theorem EuclideanSpace.basisFun_inner (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] [Fintype ι] (x : EuclideanSpace 𝕜 ι) (i : ι) :
inner 𝕜 ((basisFun ι 𝕜) i) x = x.ofLp i
source
@[simp]
theorem EuclideanSpace.inner_basisFun_real (ι : Type u_1) [Fintype ι] (x : EuclideanSpace ℝ ι) (i : ι) :
inner ℝ x ((basisFun ι ℝ) i) = x.ofLp i
source
theorem EuclideanSpace.basisFun_toBasis (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] [Fintype ι] :
(basisFun ι 𝕜).toBasis = PiLp.basisFun 2 𝕜 ι
source
instance OrthonormalBasis.instInhabited {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [Fintype ι] :
Inhabited (OrthonormalBasis ι 𝕜 (EuclideanSpace 𝕜 ι))
Equations

- OrthonormalBasis.instInhabited = { default := EuclideanSpace.basisFun ι 𝕜 }

source
def OrthonormalBasis.equiv {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {E' : Type u_7} [Fintype ι'] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (b : OrthonormalBasis ι 𝕜 E) (b' : OrthonormalBasis ι' 𝕜 E') (e : ι ≃ ι') :
E ≃ₗᵢ[𝕜] E'

The `LinearIsometryEquiv` which maps an orthonormal basis to another. This is a convenience wrapper around `Orthonormal.equiv`.

Equations

- b.equiv b' e = b.repr.trans ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e).trans b'.repr.symm)

Instances For

source
@[simp]
theorem OrthonormalBasis.equiv_symm {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {E' : Type u_7} [Fintype ι'] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (b : OrthonormalBasis ι 𝕜 E) (b' : OrthonormalBasis ι' 𝕜 E') (e : ι ≃ ι') :
(b.equiv b' e).symm = b'.equiv b e.symm
source
@[simp]
theorem OrthonormalBasis.equiv_apply_basis {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {E' : Type u_7} [Fintype ι'] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (b : OrthonormalBasis ι 𝕜 E) (b' : OrthonormalBasis ι' 𝕜 E') (e : ι ≃ ι') (i : ι) :
(b.equiv b' e) (b i) = b' (e i)
source
@[simp]
theorem OrthonormalBasis.equiv_self_rfl {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) :
b.equiv b (Equiv.refl ι) = LinearIsometryEquiv.refl 𝕜 E
source
theorem OrthonormalBasis.equiv_apply {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {E' : Type u_7} [Fintype ι'] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (b : OrthonormalBasis ι 𝕜 E) (b' : OrthonormalBasis ι' 𝕜 E') (e : ι ≃ ι') (x : E) :
(b.equiv b' e) x = ∑ i : ι, (b.repr x).ofLp i • b' (e i)
source
theorem OrthonormalBasis.equiv_apply_euclideanSpace {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : EuclideanSpace 𝕜 ι) :
((EuclideanSpace.basisFun ι 𝕜).equiv b (Equiv.refl ι)) x = ∑ i : ι, x.ofLp i • b i
source
theorem OrthonormalBasis.coe_equiv_euclideanSpace {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) :
⇑((EuclideanSpace.basisFun ι 𝕜).equiv b (Equiv.refl ι)) = fun (x : EuclideanSpace 𝕜 ι) => ∑ i : ι, x.ofLp i • b i
source
def Complex.orthonormalBasisOneI :
OrthonormalBasis (Fin 2) ℝ ℂ

`![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

source
@[simp]
theorem Complex.orthonormalBasisOneI_repr_apply (z : ℂ) :
(orthonormalBasisOneI.repr z).ofLp = ![z.re, z.im]
source
@[simp]
theorem Complex.orthonormalBasisOneI_repr_symm_apply (x : EuclideanSpace ℝ (Fin 2)) :
orthonormalBasisOneI.repr.symm x = ↑(x.ofLp 0) + ↑(x.ofLp 1) * I
source
@[simp]
theorem Complex.toBasis_orthonormalBasisOneI :
orthonormalBasisOneI.toBasis = basisOneI
source
@[simp]
theorem Complex.coe_orthonormalBasisOneI :
⇑orthonormalBasisOneI = ![1, I]
source
def Complex.isometryOfOrthonormal {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (v : OrthonormalBasis (Fin 2) ℝ F) :
ℂ ≃ₗᵢ[ℝ] F

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

source
@[simp]
theorem Complex.map_isometryOfOrthonormal {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {F' : Type u_6} [NormedAddCommGroup F'] [InnerProductSpace ℝ F'] (v : OrthonormalBasis (Fin 2) ℝ F) (f : F ≃ₗᵢ[ℝ] F') :
isometryOfOrthonormal (v.map f) = (isometryOfOrthonormal v).trans f
source
theorem Complex.isometryOfOrthonormal_symm_apply {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (v : OrthonormalBasis (Fin 2) ℝ F) (f : F) :
(isometryOfOrthonormal v).symm f = ↑((v.toBasis.coord 0) f) + ↑((v.toBasis.coord 1) f) * I
source
theorem Complex.isometryOfOrthonormal_apply {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (v : OrthonormalBasis (Fin 2) ℝ F) (z : ℂ) :
(isometryOfOrthonormal v) z = z.re • v 0 + z.im • v 1

### Matrix representation of an orthonormal basis with respect to another #

source
@[simp]
theorem OrthonormalBasis.toMatrix_orthonormalBasis_conjTranspose_mul_self {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] [Fintype ι'] (a : OrthonormalBasis ι' 𝕜 E) (b : OrthonormalBasis ι 𝕜 E) :
(a.toBasis.toMatrix ⇑b).conjTranspose * a.toBasis.toMatrix ⇑b = 1

A version of `OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary` that works for bases with different index types.

source
@[simp]
theorem OrthonormalBasis.toMatrix_orthonormalBasis_self_mul_conjTranspose {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] [Fintype ι'] (a : OrthonormalBasis ι 𝕜 E) (b : OrthonormalBasis ι' 𝕜 E) :
a.toBasis.toMatrix ⇑b * (a.toBasis.toMatrix ⇑b).conjTranspose = 1

A version of `OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary` that works for bases with different index types.

source
theorem OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (a b : OrthonormalBasis ι 𝕜 E) :
a.toBasis.toMatrix ⇑b ∈ Matrix.unitaryGroup ι 𝕜

The change-of-basis matrix between two orthonormal bases `a`, `b` is a unitary matrix.

source
@[simp]
theorem OrthonormalBasis.det_to_matrix_orthonormalBasis {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (a b : OrthonormalBasis ι 𝕜 E) :
‖a.toBasis.det ⇑b‖ = 1

The determinant of the change-of-basis matrix between two orthonormal bases `a`, `b` has unit length.

source
theorem OrthonormalBasis.toMatrix_orthonormalBasis_mem_orthogonal {ι : Type u_1} {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [Fintype ι] [DecidableEq ι] (a b : OrthonormalBasis ι ℝ F) :
a.toBasis.toMatrix ⇑b ∈ Matrix.orthogonalGroup ι ℝ

The change-of-basis matrix between two orthonormal bases `a`, `b` is an orthogonal matrix.

source
theorem OrthonormalBasis.det_to_matrix_orthonormalBasis_real {ι : Type u_1} {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [Fintype ι] [DecidableEq ι] (a b : OrthonormalBasis ι ℝ F) :
a.toBasis.det ⇑b = 1 ∨ a.toBasis.det ⇑b = -1

The determinant of the change-of-basis matrix between two orthonormal bases `a`, `b` is ±1.

### Existence of orthonormal basis, etc. #

source
noncomputable def DirectSum.IsInternal.collectedOrthonormalBasis {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {A : ι → Submodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(A i)) fun (i : ι) => (A i).subtypeₗᵢ) [DecidableEq ι] (hV_sum : IsInternal fun (i : ι) => A i) {α : ι → Type u_7} [(i : ι) → Fintype (α i)] (v_family : (i : ι) → OrthonormalBasis (α i) 𝕜 ↥(A i)) :
OrthonormalBasis ((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

- DirectSum.IsInternal.collectedOrthonormalBasis hV hV_sum v_family = (hV_sum.collectedBasis fun (i : ι) => (v_family i).toBasis).toOrthonormalBasis ⋯

Instances For

source
theorem DirectSum.IsInternal.collectedOrthonormalBasis_mem {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {A : ι → Submodule 𝕜 E} [DecidableEq ι] (h : IsInternal A) {α : ι → Type u_7} [(i : ι) → Fintype (α i)] (hV : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(A i)) fun (i : ι) => (A i).subtypeₗᵢ) (v : (i : ι) → OrthonormalBasis (α i) 𝕜 ↥(A i)) (a : (i : ι) × α i) :
(collectedOrthonormalBasis hV h v) a ∈ A a.fst
source
theorem Orthonormal.exists_orthonormalBasis_extension {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : Set E} [FiniteDimensional 𝕜 E] (hv : Orthonormal 𝕜 Subtype.val) :
∃ (u : Finset E) (b : OrthonormalBasis (↥u) 𝕜 E), v ⊆ ↑u ∧ ⇑b = Subtype.val

In a finite-dimensional `InnerProductSpace`, any orthonormal subset can be extended to an orthonormal basis.

source
theorem Orthonormal.exists_orthonormalBasis_extension_of_card_eq {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ι : Type u_7} [Fintype ι] (card_ι : Module.finrank 𝕜 E = Fintype.card ι) {v : ι → E} {s : Set ι} (hv : Orthonormal 𝕜 (s.restrict v)) :
∃ (b : OrthonormalBasis ι 𝕜 E), ∀ i ∈ s, b i = v i
source
theorem exists_orthonormalBasis (𝕜 : Type u_3) [RCLike 𝕜] (E : Type u_4) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :
∃ (w : Finset E) (b : OrthonormalBasis (↥w) 𝕜 E), ⇑b = Subtype.val

A finite-dimensional inner product space admits an orthonormal basis.

source
@[irreducible]
def stdOrthonormalBasis (𝕜 : Type u_7) [RCLike 𝕜] (E : Type u_8) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :
OrthonormalBasis (Fin (Module.finrank 𝕜 E)) 𝕜 E

A finite-dimensional `InnerProductSpace` has an orthonormal basis.

Equations

- stdOrthonormalBasis 𝕜 E = have b := Classical.choose ⋯; ⋯.mpr (b.reindex (Fintype.equivFinOfCardEq ⋯))

Instances For

source
theorem stdOrthonormalBasis_def (𝕜 : Type u_7) [RCLike 𝕜] (E : Type u_8) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :
stdOrthonormalBasis 𝕜 E = have b := Classical.choose ⋯; ⋯.mpr (b.reindex (Fintype.equivFinOfCardEq ⋯))
source
theorem orthonormalBasis_one_dim {ι : Type u_1} [Fintype ι] (b : OrthonormalBasis ι ℝ ℝ) :
(⇑b = fun (x : ι) => 1) ∨ ⇑b = fun (x : ι) => -1

An orthonormal basis of `ℝ` is made either of the vector `1`, or of the vector `-1`.

source
@[irreducible]
def DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv {ι : Type u_7} {𝕜 : Type u_8} [RCLike 𝕜] {E : Type u_9} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) :
(i : ι) × Fin (Module.finrank 𝕜 ↥(V i)) ≃ Fin n

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

- One or more equations did not get rendered due to their size.

Instances For

source
theorem DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv_def {ι : Type u_7} {𝕜 : Type u_8} [RCLike 𝕜] {E : Type u_9} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) :
sigmaOrthonormalBasisIndexEquiv hn hV hV' = have b := collectedOrthonormalBasis hV' hV fun (i : ι) => stdOrthonormalBasis 𝕜 ↥(V i); Fintype.equivFinOfCardEq ⋯
source
theorem DirectSum.IsInternal.subordinateOrthonormalBasis_def {ι : Type u_7} {𝕜 : Type u_8} [RCLike 𝕜] {E : Type u_9} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) :
subordinateOrthonormalBasis hn hV hV' = (collectedOrthonormalBasis hV' hV fun (i : ι) => stdOrthonormalBasis 𝕜 ↥(V i)).reindex (sigmaOrthonormalBasisIndexEquiv hn hV hV')
source
@[irreducible]
def DirectSum.IsInternal.subordinateOrthonormalBasis {ι : Type u_7} {𝕜 : Type u_8} [RCLike 𝕜] {E : Type u_9} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) :
OrthonormalBasis (Fin n) 𝕜 E

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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[irreducible]
def DirectSum.IsInternal.subordinateOrthonormalBasisIndex {ι : Type u_7} {𝕜 : Type u_8} [RCLike 𝕜] {E : Type u_9} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V) (a : Fin n) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) :
ι

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.

Equations

- DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn hV a hV' = ((DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv hn hV hV').symm a).fst

Instances For

source
theorem DirectSum.IsInternal.subordinateOrthonormalBasisIndex_def {ι : Type u_7} {𝕜 : Type u_8} [RCLike 𝕜] {E : Type u_9} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V) (a : Fin n) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) :
subordinateOrthonormalBasisIndex hn hV a hV' = ((sigmaOrthonormalBasisIndexEquiv hn hV hV').symm a).fst
source
theorem DirectSum.IsInternal.subordinateOrthonormalBasis_subordinate {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : ℕ} (hn : Module.finrank 𝕜 E = n) [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : IsInternal V) (a : Fin n) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => ↥(V i)) fun (i : ι) => (V i).subtypeₗᵢ) :
(subordinateOrthonormalBasis hn hV hV') a ∈ V (subordinateOrthonormalBasisIndex hn hV a hV')

The basis constructed in `DirectSum.IsInternal.subordinateOrthonormalBasis` is subordinate to the `OrthogonalFamily` in question.

source
def OrthonormalBasis.fromOrthogonalSpanSingleton {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (n : ℕ) [Fact (Module.finrank 𝕜 E = n + 1)] {v : E} (hv : v ≠ 0) :
OrthonormalBasis (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 `EuclideanSpace 𝕜 (Fin n)`.

Equations

- OrthonormalBasis.fromOrthogonalSpanSingleton n hv = (stdOrthonormalBasis 𝕜 ↥(Submodule.span 𝕜 {v})ᗮ).reindex (finCongr ⋯)

Instances For

source
noncomputable def LinearIsometry.extend {𝕜 : Type u_3} [RCLike 𝕜] {V : Type u_7} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] {S : Submodule 𝕜 V} (L : ↥S →ₗᵢ[𝕜] V) :
V →ₗᵢ[𝕜] 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

- One or more equations did not get rendered due to their size.

Instances For

source
theorem LinearIsometry.extend_apply {𝕜 : Type u_3} [RCLike 𝕜] {V : Type u_7} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] {S : Submodule 𝕜 V} (L : ↥S →ₗᵢ[𝕜] V) (s : ↥S) :
L.extend ↑s = L s
source
def Matrix.toEuclideanLin {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] :
Matrix m n 𝕜 ≃ₗ[𝕜] EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 m

`Matrix.toLin'` adapted for `EuclideanSpace 𝕜 _`.

Equations

- Matrix.toEuclideanLin = Matrix.toLin'.trans ((WithLp.linearEquiv 2 𝕜 (n → 𝕜)).symm.arrowCongr (WithLp.linearEquiv 2 𝕜 (m → 𝕜)).symm)

Instances For

source
@[simp]
theorem Matrix.toEuclideanLin_toLp {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] (A : Matrix m n 𝕜) (x : n → 𝕜) :
(toEuclideanLin A) (WithLp.toLp 2 x) = WithLp.toLp 2 ((toLin' A) x)
source
@[simp]
theorem Matrix.piLp_ofLp_toEuclideanLin {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] (A : Matrix m n 𝕜) (x : EuclideanSpace 𝕜 n) :
((toEuclideanLin A) x).ofLp = (toLin' A) x.ofLp
source
theorem Matrix.toEuclideanLin_apply {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] (M : Matrix m n 𝕜) (v : EuclideanSpace 𝕜 n) :
(toEuclideanLin M) v = WithLp.toLp 2 (M.mulVec v.ofLp)
source
@[simp]
theorem Matrix.ofLp_toEuclideanLin_apply {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] (M : Matrix m n 𝕜) (v : EuclideanSpace 𝕜 n) :
((toEuclideanLin M) v).ofLp = M.mulVec v.ofLp
source
@[simp]
theorem Matrix.toEuclideanLin_apply_piLp_toLp {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] (M : Matrix m n 𝕜) (v : n → 𝕜) :
(toEuclideanLin M) (WithLp.toLp 2 v) = WithLp.toLp 2 (M.mulVec v)
source
theorem Matrix.toEuclideanLin_eq_toLin {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] [Finite m] :
toEuclideanLin = toLin (PiLp.basisFun 2 𝕜 n) (PiLp.basisFun 2 𝕜 m)
source
theorem Matrix.toEuclideanLin_eq_toLin_orthonormal {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] [Fintype m] :
toEuclideanLin = toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis
source
theorem inner_matrix_row_row {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] (A B : Matrix m n 𝕜) (i j : m) :
inner 𝕜 (WithLp.toLp 2 (A i)) (WithLp.toLp 2 (B j)) = (B * A.conjTranspose) j i

The inner product of a row of `A` and a row of `B` is an entry of `B * Aᴴ`.

source
theorem inner_matrix_col_col {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype m] (A B : Matrix m n 𝕜) (i j : n) :
inner 𝕜 (WithLp.toLp 2 (A.transpose i)) (WithLp.toLp 2 (B.transpose j)) = (A.conjTranspose * B) i j

The inner product of a column of `A` and a column of `B` is an entry of `Aᴴ * B`.

source
theorem toMatrix_innerSL_apply {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] [Fintype m] (b : OrthonormalBasis n 𝕜 E) (b₂ : OrthonormalBasis m 𝕜 𝕜) (x : E) :
(LinearMap.toMatrix b.toBasis b₂.toBasis) ↑((innerSL 𝕜) x) = Matrix.vecMulVec (star ⇑b₂) (star (b.repr x).ofLp)

The matrix representation of `innerSL 𝕜 x` given by an orthonormal basis `b` and `b₂` is equal to `vecMulVec (star b₂) (star (b.repr x))`.