Documentation

Mathlib.Analysis.InnerProductSpace.PiL2

inner product space structure on finite products of inner product spaces #

The 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 #

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

instance PiLp.innerProductSpace {𝕜 : Type u_3} [RCLike 𝕜] {ι : Type u_7} [Fintype ι] (f : ιType u_8) [(i : ι) → NormedAddCommGroup (f i)] [(i : ι) → InnerProductSpace 𝕜 (f i)] :
Equations
@[simp]
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 i) (y i)
@[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
Instances For

    Notation for vectors in Lp space. !₂[x, y, ...] is a shorthand for (WithLp.equiv 2 _ _).symm ![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

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem EuclideanSpace.nnnorm_eq {𝕜 : Type u_7} [RCLike 𝕜] {n : Type u_8} [Fintype n] (x : EuclideanSpace 𝕜 n) :
        x‖₊ = NNReal.sqrt (∑ i : n, x i‖₊ ^ 2)
        theorem EuclideanSpace.norm_eq {𝕜 : Type u_7} [RCLike 𝕜] {n : Type u_8} [Fintype n] (x : EuclideanSpace 𝕜 n) :
        x = (∑ i : n, x i ^ 2)
        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 i) (y i) ^ 2)
        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 i) (y i) ^ 2)
        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 i) (y i) ^ 2) ^ (1 / 2)
        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 i ^ 2 < r ^ 2}
        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 i ^ 2 r ^ 2}
        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 i ^ 2 = r ^ 2}
        @[simp]
        theorem finrank_euclideanSpace {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [Fintype ι] :
        theorem finrank_euclideanSpace_fin {𝕜 : Type u_3} [RCLike 𝕜] {n : } :
        theorem EuclideanSpace.inner_eq_star_dotProduct {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [Fintype ι] (x y : EuclideanSpace 𝕜 ι) :
        inner x y = Matrix.dotProduct (star ((WithLp.equiv 2 (ι𝕜)) x)) ((WithLp.equiv 2 (ι𝕜)) y)
        theorem EuclideanSpace.inner_piLp_equiv_symm {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [Fintype ι] (x y : ι𝕜) :
        inner ((WithLp.equiv 2 (ι𝕜)).symm x) ((WithLp.equiv 2 (ι𝕜)).symm y) = Matrix.dotProduct (star x) y
        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 : DirectSum.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
          @[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 : DirectSum.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 i)
          @[reducible, inline]
          abbrev EuclideanSpace.equiv (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] :
          EuclideanSpace 𝕜 ι ≃L[𝕜] ι𝕜

          A shorthand for PiLp.continuousLinearEquiv.

          Equations
          Instances For
            @[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
            Instances For
              @[reducible, inline]
              abbrev EuclideanSpace.proj {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] (i : ι) :
              EuclideanSpace 𝕜 ι →L[𝕜] 𝕜

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

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

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

                Equations
                Instances For
                  @[simp]
                  theorem WithLp.equiv_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] (i : ι) (a : 𝕜) :
                  (WithLp.equiv 2 ((i : ι) → (fun (x : ι) => 𝕜) i)) (EuclideanSpace.single i a) = Pi.single i a
                  @[simp]
                  theorem WithLp.equiv_symm_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] (i : ι) (a : 𝕜) :
                  (WithLp.equiv 2 (ι𝕜)).symm (Pi.single i a) = EuclideanSpace.single i a
                  @[simp]
                  theorem EuclideanSpace.single_apply {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] (i : ι) (a : 𝕜) (j : ι) :
                  EuclideanSpace.single i a j = if j = i then a else 0
                  theorem EuclideanSpace.inner_single_left {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι) :
                  theorem EuclideanSpace.inner_single_right {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι) :
                  inner v (EuclideanSpace.single i a) = a * (starRingEnd ((fun (x : ι) => 𝕜) i)) (v i)
                  @[simp]
                  theorem EuclideanSpace.norm_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) :
                  @[simp]
                  theorem EuclideanSpace.nnnorm_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) :
                  @[simp]
                  theorem EuclideanSpace.dist_single_same {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a b : 𝕜) :
                  @[simp]
                  theorem EuclideanSpace.nndist_single_same {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a b : 𝕜) :
                  @[simp]
                  theorem EuclideanSpace.edist_single_same {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a b : 𝕜) :
                  theorem EuclideanSpace.orthonormal_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] :
                  Orthonormal 𝕜 fun (i : ι) => EuclideanSpace.single i 1

                  EuclideanSpace.single forms an orthonormal family.

                  theorem EuclideanSpace.piLpCongrLeft_single {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] [Fintype ι] {ι' : Type u_7} [Fintype ι'] [DecidableEq ι'] (e : ι' ι) (i' : ι') (v : 𝕜) :
                  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 𝕜 ι.

                  Instances For
                    theorem OrthonormalBasis.repr_injective {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] :
                    Function.Injective OrthonormalBasis.repr
                    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 ith basis vector.

                    Equations
                    @[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)
                    @[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
                    @[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
                    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 i = inner (b i) v
                    @[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
                    def OrthonormalBasis.toBasis {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) :
                    Basis ι 𝕜 E

                    The Basis ι 𝕜 E underlying the OrthonormalBasis

                    Equations
                    Instances For
                      @[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
                      @[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
                      @[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 i
                      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 i b i = x
                      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
                      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 i b i = b.repr.symm v
                      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
                      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) :
                      (orthogonalProjection U) x = i : ι, inner (↑(b i)) x b i
                      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) :

                      Mapping an orthonormal basis along a LinearIsometryEquiv.

                      Equations
                      • b.map L = { repr := L.symm.trans b.repr }
                      Instances For
                        @[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)
                        @[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
                        def Basis.toOrthonormalBasis {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 v) :

                        A basis that is orthonormal is an orthonormal basis.

                        Equations
                        • v.toOrthonormalBasis hv = { repr := v.equivFun.isometryOfInner }
                        Instances For
                          @[simp]
                          theorem 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
                          @[simp]
                          theorem 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 = v.equivFun.symm
                          @[simp]
                          theorem 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
                          @[simp]
                          theorem 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
                          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
                          Instances For
                            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
                            @[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.equiv 2 ((j : η) → E j)).symm (Pi.single j.fst ((B j.fst) j.snd))
                            @[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 x j = (B j.fst).repr (x j.fst) j.snd
                            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)) :

                            A finite orthonormal set that spans is an orthonormal basis

                            Equations
                            Instances For
                              @[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
                              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 { x : ι' // x s } 𝕜 (Submodule.span 𝕜 (Finset.image v' s))

                              Any finite subset of an orthonormal family is an OrthonormalBasis for its span.

                              Equations
                              Instances For
                                @[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 : { x : ι' // x s }) :
                                ((OrthonormalBasis.span h s) i) = v' i
                                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)) = ) :

                                A finite orthonormal family of vectors whose span has trivial orthogonal complement is an orthonormal basis.

                                Equations
                                Instances For
                                  @[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)) = ) :
                                  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
                                  Instances For
                                    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')
                                    @[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
                                    @[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
                                    @[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 i' = b.repr x (e.symm i')
                                    noncomputable def EuclideanSpace.basisFun (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] [Fintype ι] :

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

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem EuclideanSpace.basisFun_apply (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] [Fintype ι] [DecidableEq ι] (i : ι) :
                                      @[simp]
                                      theorem EuclideanSpace.basisFun_repr (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] [Fintype ι] (x : EuclideanSpace 𝕜 ι) (i : ι) :
                                      (EuclideanSpace.basisFun ι 𝕜).repr x i = x i
                                      theorem EuclideanSpace.basisFun_toBasis (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] [Fintype ι] :
                                      (EuclideanSpace.basisFun ι 𝕜).toBasis = PiLp.basisFun 2 𝕜 ι
                                      instance OrthonormalBasis.instInhabited {ι : Type u_1} {𝕜 : Type u_3} [RCLike 𝕜] [Fintype ι] :
                                      Equations

                                      ![1, I] is an orthonormal basis for considered as a real inner product space.

                                      Equations
                                      Instances For

                                        The isometry between and a two-dimensional real inner product space given by a basis.

                                        Equations
                                        Instances For
                                          theorem Complex.isometryOfOrthonormal_symm_apply {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace F] (v : OrthonormalBasis (Fin 2) F) (f : F) :
                                          (Complex.isometryOfOrthonormal v).symm f = ((v.toBasis.coord 0) f) + ((v.toBasis.coord 1) f) * Complex.I

                                          Matrix representation of an orthonormal basis with respect to another #

                                          @[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.

                                          @[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.

                                          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.

                                          @[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.

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

                                          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. #

                                          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 : DirectSum.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
                                          Instances For
                                            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 : DirectSum.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) :
                                            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 { x : E // x u } 𝕜 E), v u b = Subtype.val

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

                                            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), is, b i = v i
                                            theorem exists_orthonormalBasis (𝕜 : Type u_3) [RCLike 𝕜] (E : Type u_4) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :
                                            ∃ (w : Finset E) (b : OrthonormalBasis { x : E // x w } 𝕜 E), b = Subtype.val

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

                                            @[irreducible]
                                            def stdOrthonormalBasis (𝕜 : Type u_7) [RCLike 𝕜] (E : Type u_8) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :

                                            A finite-dimensional InnerProductSpace has an orthonormal basis.

                                            Equations
                                            Instances For
                                              theorem stdOrthonormalBasis_def (𝕜 : Type u_7) [RCLike 𝕜] (E : Type u_8) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :
                                              stdOrthonormalBasis 𝕜 E = let b := Classical.choose ; .mpr (b.reindex (Fintype.equivFinOfCardEq ))
                                              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.

                                              @[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 : DirectSum.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
                                                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 : DirectSum.IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => (V i)) fun (i : ι) => (V i).subtypeₗᵢ) :
                                                @[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 : DirectSum.IsInternal V) (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.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  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 : DirectSum.IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => (V i)) fun (i : ι) => (V i).subtypeₗᵢ) :
                                                  @[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 : DirectSum.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
                                                  Instances For
                                                    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 : DirectSum.IsInternal V) (a : Fin n) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => (V i)) fun (i : ι) => (V i).subtypeₗᵢ) :
                                                    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 : DirectSum.IsInternal V) (a : Fin n) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => (V i)) fun (i : ι) => (V i).subtypeₗᵢ) :

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

                                                    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
                                                    Instances For
                                                      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
                                                        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
                                                        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
                                                        Instances For
                                                          @[simp]
                                                          theorem Matrix.toEuclideanLin_piLp_equiv_symm {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] (A : Matrix m n 𝕜) (x : n𝕜) :
                                                          (Matrix.toEuclideanLin A) ((WithLp.equiv 2 ((i : n) → (fun (x : n) => 𝕜) i)).symm x) = (WithLp.equiv 2 (m𝕜)).symm ((Matrix.toLin' A) x)
                                                          @[simp]
                                                          theorem Matrix.piLp_equiv_toEuclideanLin {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] (A : Matrix m n 𝕜) (x : EuclideanSpace 𝕜 n) :
                                                          (WithLp.equiv 2 ((i : m) → (fun (x : m) => 𝕜) i)) ((Matrix.toEuclideanLin A) x) = (Matrix.toLin' A) ((WithLp.equiv 2 (n𝕜)) x)
                                                          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) :
                                                          (Matrix.toEuclideanLin M) v = (WithLp.equiv 2 (m𝕜)).symm (M.mulVec ((WithLp.equiv 2 (n𝕜)) v))
                                                          @[simp]
                                                          theorem Matrix.piLp_equiv_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) :
                                                          (WithLp.equiv 2 (m𝕜)) ((Matrix.toEuclideanLin M) v) = M.mulVec ((WithLp.equiv 2 (n𝕜)) v)
                                                          @[simp]
                                                          theorem Matrix.toEuclideanLin_apply_piLp_equiv_symm {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] (M : Matrix m n 𝕜) (v : n𝕜) :
                                                          (Matrix.toEuclideanLin M) ((WithLp.equiv 2 (n𝕜)).symm v) = (WithLp.equiv 2 (m𝕜)).symm (M.mulVec v)
                                                          theorem Matrix.toEuclideanLin_eq_toLin {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] [Finite m] :
                                                          Matrix.toEuclideanLin = Matrix.toLin (PiLp.basisFun 2 𝕜 n) (PiLp.basisFun 2 𝕜 m)
                                                          theorem Matrix.toEuclideanLin_eq_toLin_orthonormal {𝕜 : Type u_3} [RCLike 𝕜] {m : Type u_7} {n : Type u_8} [Fintype n] [DecidableEq n] [Fintype m] :
                                                          Matrix.toEuclideanLin = Matrix.toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis
                                                          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.equiv 2 (n𝕜)).symm (A i)) ((WithLp.equiv 2 (n𝕜)).symm (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ᴴ.

                                                          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.equiv 2 (m𝕜)).symm (A.transpose i)) ((WithLp.equiv 2 (m𝕜)).symm (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.