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} [IsROrC 𝕜] {ι : Type u_8} [Fintype ι] (f : ιType u_9) [(i : ι) → NormedAddCommGroup (f i)] [(i : ι) → InnerProductSpace 𝕜 (f i)] :
Equations
@[simp]
theorem PiLp.inner_apply {𝕜 : Type u_3} [IsROrC 𝕜] {ι : Type u_8} [Fintype ι] {f : ιType u_9} [(i : ι) → NormedAddCommGroup (f i)] [(i : ι) → InnerProductSpace 𝕜 (f i)] (x : PiLp 2 f) (y : PiLp 2 f) :
x, y⟫_𝕜 = Finset.sum Finset.univ fun (i : ι) => x i, y i⟫_𝕜
@[reducible]
def EuclideanSpace (𝕜 : Type u_8) (n : Type u_9) :
Type (max u_9 u_8)

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

Equations
Instances For
    theorem EuclideanSpace.nnnorm_eq {𝕜 : Type u_8} [IsROrC 𝕜] {n : Type u_9} [Fintype n] (x : EuclideanSpace 𝕜 n) :
    x‖₊ = NNReal.sqrt (Finset.sum Finset.univ fun (i : n) => x i‖₊ ^ 2)
    theorem EuclideanSpace.norm_eq {𝕜 : Type u_8} [IsROrC 𝕜] {n : Type u_9} [Fintype n] (x : EuclideanSpace 𝕜 n) :
    x = Real.sqrt (Finset.sum Finset.univ fun (i : n) => x i ^ 2)
    theorem EuclideanSpace.dist_eq {𝕜 : Type u_8} [IsROrC 𝕜] {n : Type u_9} [Fintype n] (x : EuclideanSpace 𝕜 n) (y : EuclideanSpace 𝕜 n) :
    dist x y = Real.sqrt (Finset.sum Finset.univ fun (i : n) => dist (x i) (y i) ^ 2)
    theorem EuclideanSpace.nndist_eq {𝕜 : Type u_8} [IsROrC 𝕜] {n : Type u_9} [Fintype n] (x : EuclideanSpace 𝕜 n) (y : EuclideanSpace 𝕜 n) :
    nndist x y = NNReal.sqrt (Finset.sum Finset.univ fun (i : n) => nndist (x i) (y i) ^ 2)
    theorem EuclideanSpace.edist_eq {𝕜 : Type u_8} [IsROrC 𝕜] {n : Type u_9} [Fintype n] (x : EuclideanSpace 𝕜 n) (y : EuclideanSpace 𝕜 n) :
    edist x y = (Finset.sum Finset.univ fun (i : n) => edist (x i) (y i) ^ 2) ^ (1 / 2)
    theorem EuclideanSpace.ball_zero_eq {n : Type u_8} [Fintype n] (r : ) (hr : 0 r) :
    Metric.ball 0 r = {x : EuclideanSpace n | (Finset.sum Finset.univ fun (i : n) => x i ^ 2) < r ^ 2}
    theorem EuclideanSpace.closedBall_zero_eq {n : Type u_8} [Fintype n] (r : ) (hr : 0 r) :
    Metric.closedBall 0 r = {x : EuclideanSpace n | (Finset.sum Finset.univ fun (i : n) => x i ^ 2) r ^ 2}
    theorem EuclideanSpace.sphere_zero_eq {n : Type u_8} [Fintype n] (r : ) (hr : 0 r) :
    Metric.sphere 0 r = {x : EuclideanSpace n | (Finset.sum Finset.univ fun (i : n) => x i ^ 2) = r ^ 2}
    @[simp]
    theorem finrank_euclideanSpace {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [Fintype ι] :
    theorem finrank_euclideanSpace_fin {𝕜 : Type u_3} [IsROrC 𝕜] {n : } :
    theorem EuclideanSpace.inner_eq_star_dotProduct {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [Fintype ι] (x : EuclideanSpace 𝕜 ι) (y : EuclideanSpace 𝕜 ι) :
    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} [IsROrC 𝕜] [Fintype ι] (x : ι𝕜) (y : ι𝕜) :
    (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} [IsROrC 𝕜] {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 : ι) => Submodule.subtypeₗᵢ (V i)) :
    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} [IsROrC 𝕜] {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 : ι) => Submodule.subtypeₗᵢ (V i)) (w : PiLp 2 fun (i : ι) => (V i)) :
      @[inline, reducible]
      abbrev EuclideanSpace.equiv (ι : Type u_1) (𝕜 : Type u_3) [IsROrC 𝕜] :
      EuclideanSpace 𝕜 ι ≃L[𝕜] ι𝕜

      A shorthand for PiLp.continuousLinearEquiv.

      Equations
      Instances For
        @[simp]
        theorem EuclideanSpace.projₗ_apply {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] (i : ι) :
        ∀ (a : WithLp 2 (ι𝕜)), (EuclideanSpace.projₗ i) a = a i
        def EuclideanSpace.projₗ {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] (i : ι) :
        EuclideanSpace 𝕜 ι →ₗ[𝕜] 𝕜

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

        Equations
        Instances For
          @[simp]
          theorem EuclideanSpace.proj_coe {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] (i : ι) :
          @[simp]
          theorem EuclideanSpace.proj_apply {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] (i : ι) :
          ∀ (a : WithLp 2 (ι𝕜)), (EuclideanSpace.proj i) a = a i
          def EuclideanSpace.proj {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] (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} [IsROrC 𝕜] [DecidableEq ι] (i : ι) (a : 𝕜) :

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

            Equations
            Instances For
              @[simp]
              theorem WithLp.equiv_single {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [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} [IsROrC 𝕜] [DecidableEq ι] (i : ι) (a : 𝕜) :
              (WithLp.equiv 2 ((j : ι) → (fun (x : ι) => 𝕜) j)).symm (Pi.single i a) = EuclideanSpace.single i a
              @[simp]
              theorem EuclideanSpace.single_apply {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [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} [IsROrC 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι) :
              EuclideanSpace.single i a, v⟫_𝕜 = (starRingEnd 𝕜) a * v i
              theorem EuclideanSpace.inner_single_right {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι) :
              v, EuclideanSpace.single i a⟫_𝕜 = a * (starRingEnd ((fun (x : ι) => 𝕜) i)) (v i)
              @[simp]
              theorem EuclideanSpace.norm_single {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) :
              @[simp]
              theorem EuclideanSpace.nnnorm_single {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) :
              @[simp]
              theorem EuclideanSpace.dist_single_same {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) (b : 𝕜) :
              @[simp]
              theorem EuclideanSpace.nndist_single_same {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) (b : 𝕜) :
              @[simp]
              theorem EuclideanSpace.edist_single_same {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [DecidableEq ι] [Fintype ι] (i : ι) (a : 𝕜) (b : 𝕜) :
              theorem EuclideanSpace.orthonormal_single {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [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} [IsROrC 𝕜] [DecidableEq ι] [Fintype ι] {ι' : Type u_8} [Fintype ι'] [DecidableEq ι'] (e : ι' ι) (i' : ι') (v : 𝕜) :
              structure OrthonormalBasis (ι : Type u_1) (𝕜 : Type u_3) [IsROrC 𝕜] (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} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] :
                Function.Injective OrthonormalBasis.repr
                instance OrthonormalBasis.instFunLike {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {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} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (e : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι) :
                { repr := e } = fun (i : ι) => (LinearIsometryEquiv.symm e) (EuclideanSpace.single i 1)
                @[simp]
                theorem OrthonormalBasis.repr_symm_single {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι) :
                @[simp]
                theorem OrthonormalBasis.repr_self {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {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} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (v : E) (i : ι) :
                b.repr v i = b i, v⟫_𝕜
                @[simp]
                theorem OrthonormalBasis.orthonormal {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) :
                Orthonormal 𝕜 b
                def OrthonormalBasis.toBasis {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {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} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) :
                  @[simp]
                  theorem OrthonormalBasis.coe_toBasis_repr {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) :
                  Basis.equivFun (OrthonormalBasis.toBasis b) = b.repr.toLinearEquiv
                  @[simp]
                  theorem OrthonormalBasis.coe_toBasis_repr_apply {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) (i : ι) :
                  ((OrthonormalBasis.toBasis b).repr x) i = b.repr x i
                  theorem OrthonormalBasis.sum_repr {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) :
                  (Finset.sum Finset.univ fun (i : ι) => b.repr x i b i) = x
                  theorem OrthonormalBasis.sum_repr_symm {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (v : EuclideanSpace 𝕜 ι) :
                  (Finset.sum Finset.univ fun (i : ι) => v i b i) = (LinearIsometryEquiv.symm b.repr) v
                  theorem OrthonormalBasis.sum_inner_mul_inner {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) (y : E) :
                  (Finset.sum Finset.univ fun (i : ι) => x, b i⟫_𝕜 * b i, y⟫_𝕜) = x, y⟫_𝕜
                  theorem OrthonormalBasis.orthogonalProjection_eq_sum {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {U : Submodule 𝕜 E} [CompleteSpace U] (b : OrthonormalBasis ι 𝕜 U) (x : E) :
                  (orthogonalProjection U) x = Finset.sum Finset.univ fun (i : ι) => (b i), x⟫_𝕜 b i
                  def OrthonormalBasis.map {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {G : Type u_8} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (b : OrthonormalBasis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G) :

                  Mapping an orthonormal basis along a LinearIsometryEquiv.

                  Equations
                  Instances For
                    @[simp]
                    theorem OrthonormalBasis.map_apply {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {G : Type u_8} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (b : OrthonormalBasis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G) (i : ι) :
                    (OrthonormalBasis.map b L) i = L (b i)
                    @[simp]
                    theorem OrthonormalBasis.toBasis_map {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {G : Type u_8} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] (b : OrthonormalBasis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G) :
                    def Basis.toOrthonormalBasis {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {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
                    Instances For
                      @[simp]
                      theorem Basis.coe_toOrthonormalBasis_repr {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 v) :
                      @[simp]
                      theorem Basis.coe_toOrthonormalBasis_repr_symm {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 v) :
                      @[simp]
                      theorem Basis.toBasis_toOrthonormalBasis {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 v) :
                      @[simp]
                      theorem Basis.coe_toOrthonormalBasis {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 v) :
                      def OrthonormalBasis.mk {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {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} [IsROrC 𝕜] {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} [IsROrC 𝕜] {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
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem OrthonormalBasis.span_apply {ι' : Type u_2} {𝕜 : Type u_3} [IsROrC 𝕜] {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} [IsROrC 𝕜] {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} [IsROrC 𝕜] {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} [IsROrC 𝕜] {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} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (e : ι ι') (i' : ι') :
                              (OrthonormalBasis.reindex b e) i' = b (e.symm i')
                              @[simp]
                              theorem OrthonormalBasis.coe_reindex {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (e : ι ι') :
                              (OrthonormalBasis.reindex b e) = b e.symm
                              @[simp]
                              theorem OrthonormalBasis.repr_reindex {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (e : ι ι') (x : E) (i' : ι') :
                              (OrthonormalBasis.reindex b e).repr x i' = b.repr x (e.symm i')
                              noncomputable def EuclideanSpace.basisFun (ι : Type u_1) (𝕜 : Type u_3) [IsROrC 𝕜] [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) [IsROrC 𝕜] [Fintype ι] [DecidableEq ι] (i : ι) :
                                @[simp]
                                theorem EuclideanSpace.basisFun_repr (ι : Type u_1) (𝕜 : Type u_3) [IsROrC 𝕜] [Fintype ι] (x : EuclideanSpace 𝕜 ι) (i : ι) :
                                (EuclideanSpace.basisFun ι 𝕜).repr x i = x i
                                instance OrthonormalBasis.instInhabited {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] [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

                                    Matrix representation of an orthonormal basis with respect to another #

                                    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} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (a : OrthonormalBasis ι 𝕜 E) (b : OrthonormalBasis ι 𝕜 E) :

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

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

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

                                    Existence of orthonormal basis, etc. #

                                    noncomputable def DirectSum.IsInternal.collectedOrthonormalBasis {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {A : ιSubmodule 𝕜 E} (hV : OrthogonalFamily 𝕜 (fun (i : ι) => (A i)) fun (i : ι) => Submodule.subtypeₗᵢ (A i)) [DecidableEq ι] (hV_sum : DirectSum.IsInternal fun (i : ι) => A i) {α : ιType u_8} [(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
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      theorem DirectSum.IsInternal.collectedOrthonormalBasis_mem {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] {A : ιSubmodule 𝕜 E} [DecidableEq ι] (h : DirectSum.IsInternal A) {α : ιType u_8} [(i : ι) → Fintype (α i)] (hV : OrthogonalFamily 𝕜 (fun (i : ι) => (A i)) fun (i : ι) => Submodule.subtypeₗᵢ (A i)) (v : (i : ι) → OrthonormalBasis (α i) 𝕜 (A i)) (a : (i : ι) × α i) :
                                      theorem Orthonormal.exists_orthonormalBasis_extension {𝕜 : Type u_3} [IsROrC 𝕜] {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} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ι : Type u_8} [Fintype ι] (card_ι : FiniteDimensional.finrank 𝕜 E = Fintype.card ι) {v : ιE} {s : Set ι} (hv : Orthonormal 𝕜 (Set.restrict s v)) :
                                      ∃ (b : OrthonormalBasis ι 𝕜 E), is, b i = v i
                                      theorem exists_orthonormalBasis (𝕜 : Type u_3) [IsROrC 𝕜] (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]

                                      A finite-dimensional InnerProductSpace has an orthonormal basis.

                                      Equations
                                      Instances For
                                        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.

                                        theorem DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv_def {ι : Type u_8} {𝕜 : Type u_9} [IsROrC 𝕜] {E : Type u_10} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : } (hn : FiniteDimensional.finrank 𝕜 E = n) [DecidableEq ι] {V : ιSubmodule 𝕜 E} (hV : DirectSum.IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => (V i)) fun (i : ι) => Submodule.subtypeₗᵢ (V i)) :
                                        @[irreducible]
                                        def DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv {ι : Type u_8} {𝕜 : Type u_9} [IsROrC 𝕜] {E : Type u_10} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : } (hn : FiniteDimensional.finrank 𝕜 E = n) [DecidableEq ι] {V : ιSubmodule 𝕜 E} (hV : DirectSum.IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => (V i)) fun (i : ι) => Submodule.subtypeₗᵢ (V i)) :
                                        (i : ι) × Fin (FiniteDimensional.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
                                        Instances For
                                          @[irreducible]
                                          def DirectSum.IsInternal.subordinateOrthonormalBasis {ι : Type u_8} {𝕜 : Type u_9} [IsROrC 𝕜] {E : Type u_10} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : } (hn : FiniteDimensional.finrank 𝕜 E = n) [DecidableEq ι] {V : ιSubmodule 𝕜 E} (hV : DirectSum.IsInternal V) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => (V i)) fun (i : ι) => Submodule.subtypeₗᵢ (V i)) :

                                          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
                                          Instances For
                                            @[irreducible]
                                            def DirectSum.IsInternal.subordinateOrthonormalBasisIndex {ι : Type u_8} {𝕜 : Type u_9} [IsROrC 𝕜] {E : Type u_10} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : } (hn : FiniteDimensional.finrank 𝕜 E = n) [DecidableEq ι] {V : ιSubmodule 𝕜 E} (hV : DirectSum.IsInternal V) (a : Fin n) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => (V i)) fun (i : ι) => Submodule.subtypeₗᵢ (V i)) :
                                            ι

                                            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_8} {𝕜 : Type u_9} [IsROrC 𝕜] {E : Type u_10} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : } (hn : FiniteDimensional.finrank 𝕜 E = n) [DecidableEq ι] {V : ιSubmodule 𝕜 E} (hV : DirectSum.IsInternal V) (a : Fin n) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => (V i)) fun (i : ι) => Submodule.subtypeₗᵢ (V i)) :
                                              theorem DirectSum.IsInternal.subordinateOrthonormalBasis_subordinate {ι : Type u_1} {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [FiniteDimensional 𝕜 E] {n : } (hn : FiniteDimensional.finrank 𝕜 E = n) [DecidableEq ι] {V : ιSubmodule 𝕜 E} (hV : DirectSum.IsInternal V) (a : Fin n) (hV' : OrthogonalFamily 𝕜 (fun (i : ι) => (V i)) fun (i : ι) => Submodule.subtypeₗᵢ (V i)) :

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

                                              def OrthonormalBasis.fromOrthogonalSpanSingleton {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (n : ) [Fact (FiniteDimensional.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} [IsROrC 𝕜] {V : Type u_8} [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} [IsROrC 𝕜] {V : Type u_8} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] {S : Submodule 𝕜 V} (L : S →ₗᵢ[𝕜] V) (s : S) :
                                                  def Matrix.toEuclideanLin {𝕜 : Type u_3} [IsROrC 𝕜] {m : Type u_8} {n : Type u_9} [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} [IsROrC 𝕜] {m : Type u_8} {n : Type u_9} [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} [IsROrC 𝕜] {m : Type u_8} {n : Type u_9} [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_eq_toLin {𝕜 : Type u_3} [IsROrC 𝕜] {m : Type u_8} {n : Type u_9} [Fintype m] [Fintype n] [DecidableEq n] :
                                                    Matrix.toEuclideanLin = Matrix.toLin (PiLp.basisFun 2 𝕜 n) (PiLp.basisFun 2 𝕜 m)
                                                    theorem inner_matrix_row_row {𝕜 : Type u_3} [IsROrC 𝕜] {m : Type u_8} {n : Type u_9} [Fintype n] (A : Matrix m n 𝕜) (B : Matrix m n 𝕜) (i : m) (j : m) :
                                                    (WithLp.equiv 2 (n𝕜)).symm (A i), (WithLp.equiv 2 (n𝕜)).symm (B j)⟫_𝕜 = (B * Matrix.conjTranspose A) 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} [IsROrC 𝕜] {m : Type u_8} {n : Type u_9} [Fintype m] (A : Matrix m n 𝕜) (B : Matrix m n 𝕜) (i : n) (j : n) :
                                                    (WithLp.equiv 2 (m𝕜)).symm (Matrix.transpose A i), (WithLp.equiv 2 (m𝕜)).symm (Matrix.transpose B j)⟫_𝕜 = (Matrix.conjTranspose A * B) i j

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