IsHilbertSum.mkInternal
theorem IsHilbertSum.mkInternal :
โ {ฮน : Type u_1} {๐ : Type u_2} [inst : RCLike ๐] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
[inst_2 : InnerProductSpace ๐ E] [cplt : CompleteSpace E] (F : ฮน โ Submodule ๐ E)
[inst_3 : โ (i : ฮน), CompleteSpace โฅ(F i)],
(OrthogonalFamily ๐ (fun i => โฅ(F i)) fun i => (F i).subtypeโแตข) โ
โค โค (โจ i, F i).topologicalClosure โ IsHilbertSum ๐ (fun i => โฅ(F i)) fun i => (F i).subtypeโแตข
This theorem, `IsHilbertSum.mkInternal`, states that for any type `ฮน`, any type `๐` that behaves like a ring, and any type `E` which is a normed additive commutative group and an inner product space over `๐`, if `E` is a complete space and for every `i` of type `ฮน`, the subspace `F i` of `E` is a complete space, then if the family of these subspaces `F i` is orthogonal and the topological closure of the suprema (i.e., least upper bounds) of the subspaces `F i` contains the entire space `E`, then this configuration constitutes a Hilbert space sum. In other words, if we have a set of orthogonal subspaces that collectively cover the entire space after taking their topological closure, then these subspaces form a Hilbert space sum.
More concisely: If `E` is a complete normed additive commutative group and inner product space over a ring `๐`, and if every subspace `F i` of `E` is a complete orthogonal subspace with closure containing `E`, then `E` is the Hilbert space sum of the `F i`.
|
IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single
theorem IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single :
โ {ฮน : Type u_1} {๐ : Type u_2} [inst : RCLike ๐] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
[inst_2 : InnerProductSpace ๐ E] [cplt : CompleteSpace E] {G : ฮน โ Type u_4}
[inst_3 : (i : ฮน) โ NormedAddCommGroup (G i)] [inst_4 : (i : ฮน) โ InnerProductSpace ๐ (G i)]
{V : (i : ฮน) โ G i โโแตข[๐] E} (hV : IsHilbertSum ๐ G V) (Wโ : ฮ โ (i : ฮน), G i),
โ(Wโ.sum fun a b => hV.linearIsometryEquiv ((V a) b)) = โWโ
The theorem `IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single` states that for any type `ฮน`, field `๐` which is a Real and Complex number, a Hilbert sum `E` of `G : ฮน โ Type*` and `lp G 2`, and given that `E` is a normed add commutative group, `E` is an inner product space over `๐`, `E` is a complete space, every `G i` is a normed add commutative group, every `G i` is an inner product space over `๐`, and for every `i : ฮน`, `G i โโแตข[๐] E` is a linear isometry, if `V` forms a Hilbert sum, then any finitely-supported vector `Wโ` in `lp G 2` is the image of the associated finite sum of elements of `E`. In other words, the application of the canonical isometric isomorphism to the summation of the elements of a finitely-supported vector in `lp G 2` is the same as applying the vector itself.
More concisely: Given a Hilbert sum `E` of normed add commutative groups `G : ฮน โ Type*` that are also inner product spaces over a Real or Complex field `๐`, and are complete with linear isometric inclusions `G i โโแตข[๐] E`, any finitely-supported vector `Wโ` in the square-lattice of `E` is the image of the corresponding finite sum of elements in `E` under the canonical isometric isomorphism.
|
IsHilbertSum.hasSum_linearIsometryEquiv_symm
theorem IsHilbertSum.hasSum_linearIsometryEquiv_symm :
โ {ฮน : Type u_1} {๐ : Type u_2} [inst : RCLike ๐] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
[inst_2 : InnerProductSpace ๐ E] [cplt : CompleteSpace E] {G : ฮน โ Type u_4}
[inst_3 : (i : ฮน) โ NormedAddCommGroup (G i)] [inst_4 : (i : ฮน) โ InnerProductSpace ๐ (G i)]
{V : (i : ฮน) โ G i โโแตข[๐] E} (hV : IsHilbertSum ๐ G V) (w : โฅ(lp G 2)),
HasSum (fun i => (V i) (โw i)) (hV.linearIsometryEquiv.symm w)
The theorem `IsHilbertSum.hasSum_linearIsometryEquiv_symm` states that for any type `ฮน`, scalar type `๐` which is a ring complete with respect to an absolute value, Hilbert space `E` over the scalars `๐`, and for each `ฮน`, a normed addive commutative group `G i` with an inner product space over the scalars `๐`, and a linear isometric map `V` from `G i` to `E`, if `V` forms a Hilbert sum and `w` is a vector in the `lp`-space with `p = 2`, then the infinite sum of the associated elements in `E`, given by `(V i) (โw i)` for each `i`, converges to the image of `w` under the inverse of the linear isometric equivalence associated with `V`. In layman's terms, the theorem connects the concepts of lp-spaces, Hilbert spaces, and infinite sums (or series), and asserts a certain convergent behavior of the series in the context of these structures.
More concisely: For any type `ฮน`, scalar type `๐` completely equipped with an absolute value, Hilbert space `E` over `๐`, normed additive commutative groups `G i` over `๐` with inner products, linear isometric maps `V i : G i โ E`, and `lp[2]`-vector `w` in the product space, if `V` forms a Hilbert sum and `w` converges in `lp[2]`, then `(V i (โwi))` converges to `Vโปยน(โi โ ฮน wi)` in `E`.
|
IsHilbertSum.mk
theorem IsHilbertSum.mk :
โ {ฮน : Type u_1} {๐ : Type u_2} [inst : RCLike ๐] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
[inst_2 : InnerProductSpace ๐ E] [cplt : CompleteSpace E] {G : ฮน โ Type u_4}
[inst_3 : (i : ฮน) โ NormedAddCommGroup (G i)] [inst_4 : (i : ฮน) โ InnerProductSpace ๐ (G i)]
{V : (i : ฮน) โ G i โโแตข[๐] E} [inst_5 : โ (i : ฮน), CompleteSpace (G i)],
OrthogonalFamily ๐ G V โ โค โค (โจ i, LinearMap.range (V i).toLinearMap).topologicalClosure โ IsHilbertSum ๐ G V
The theorem `IsHilbertSum.mk` states that, given an orthogonal family `V` (a family of linear isometric maps from `G i` to `E` indexed by `ฮน`) such that the supremum of the ranges of each `V i` is dense in `E` (formally stated as `โค โค (โจ i, LinearMap.range (V i).toLinearMap).topologicalClosure`), then the pair `(E, V)` forms a Hilbert sum of `G`. This is under the assumption that `๐` is a ring-like structure, `E` and each `G i` are normed additive commutative groups and inner product spaces, and both `E` and each `G i` form complete spaces.
More concisely: Given a family `V` of orthogonal linear isometric maps from normed additive commutative groups `G_i` to a complete normed inner product space `E`, with dense supremum ranges, `V` forms a Hilbert sum of `G_i` in `E`.
|
Orthonormal.isHilbertSum
theorem Orthonormal.isHilbertSum :
โ {ฮน : Type u_1} {๐ : Type u_2} [inst : RCLike ๐] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
[inst_2 : InnerProductSpace ๐ E] [cplt : CompleteSpace E] {v : ฮน โ E} (hv : Orthonormal ๐ v),
โค โค (Submodule.span ๐ (Set.range v)).topologicalClosure โ
IsHilbertSum ๐ (fun x => ๐) fun i => LinearIsometry.toSpanSingleton ๐ E โฏ
This theorem states that for any orthonormal family of vectors `v : ฮน โ E` in an inner product space `E` over a field `๐`, if `E` is a complete space and the span of the range of `v` is dense in `E`, then `E` can be represented as a Hilbert sum over `๐` with respect to the family of linear isometries that map a scalar `k` to `k` times the corresponding vector `v i`. In other words, `E` is isometric to a direct sum of copies of `๐`, each spanned by a vector from the orthonormal family `v`.
More concisely: If `v : ฮน โ E` is an orthonormal family of vectors in the complete inner product space `E` over field `๐` such that the span of `v` is dense in `E`, then `E` is isometric to the Hilbert sum of copies of `๐` with respect to `v`.
|
IsHilbertSum.linearIsometryEquiv_symm_apply
theorem IsHilbertSum.linearIsometryEquiv_symm_apply :
โ {ฮน : Type u_1} {๐ : Type u_2} [inst : RCLike ๐] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
[inst_2 : InnerProductSpace ๐ E] [cplt : CompleteSpace E] {G : ฮน โ Type u_4}
[inst_3 : (i : ฮน) โ NormedAddCommGroup (G i)] [inst_4 : (i : ฮน) โ InnerProductSpace ๐ (G i)]
{V : (i : ฮน) โ G i โโแตข[๐] E} (hV : IsHilbertSum ๐ G V) (w : โฅ(lp G 2)),
hV.linearIsometryEquiv.symm w = โ' (i : ฮน), (V i) (โw i)
The theorem `IsHilbertSum.linearIsometryEquiv_symm_apply` states that for any type `ฮน`, a field `๐` that is a real or complex number, a normed additive commutative group `E`, and a complete inner product space over `E`, if `G` is a function from `ฮน` to a type `u_4` that forms a normed additive commutative group and an inner product space, and `V` is a linear isometric mapping from `G i` to `E` that forms a Hilbert sum, then for any vector `w` in the `lp` space of `G` with `p=2`, the inverse of the linear isometric equivalence of `V` applied to `w` equals the infinite sum of the elements in `E` associated with `w` via `V`. In simpler terms, it says that a vector in the `lp` space can be represented as an infinite sum of associated elements in the Hilbert sum space `E` under the linear isometric mapping `V`.
More concisely: For a Hilbert sum `E` of a complete inner product space over a normed additive commutative group `G`, a linear isometric mapping `V` from `G` to `E`, and any vector `w` in the `lp[2]` space of `G`, the inverse of the equivalence of `w` under `V` is equal to the infinite sum of the images of the components of `w` under `V`.
|
IsHilbertSum.linearIsometryEquiv_symm_apply_single
theorem IsHilbertSum.linearIsometryEquiv_symm_apply_single :
โ {ฮน : Type u_1} {๐ : Type u_2} [inst : RCLike ๐] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
[inst_2 : InnerProductSpace ๐ E] [cplt : CompleteSpace E] {G : ฮน โ Type u_4}
[inst_3 : (i : ฮน) โ NormedAddCommGroup (G i)] [inst_4 : (i : ฮน) โ InnerProductSpace ๐ (G i)]
{V : (i : ฮน) โ G i โโแตข[๐] E} (hV : IsHilbertSum ๐ G V) {i : ฮน} (x : G i),
hV.linearIsometryEquiv.symm (lp.single 2 i x) = (V i) x
This theorem states that in the context of a Hilbert sum `E` of a family of types `G : ฮน โ Type*`, under a canonical isometric isomorphism between `E` and `lp G 2`, an "elementary basis vector" in `lp G 2` supported at an index `i : ฮน` corresponds to the image of the associated element in `E`. Specifically, for any `i : ฮน` and `x : G i`, applying the inverse of the linear isometry equivalence to the lp-single (a function that returns a sequence with `x` at the `i`'th position and zeros elsewhere) of 2, `i` and `x`, we get the linear isometric map `V i` applied to `x`. The theorem is valid in the realm of a type of scalar `๐` that behaves like real numbers, a normed additive commutative group `E`, an inner product space over `E` and `๐`, a complete space `E`, and nested within each index `i : ฮน`, a normed additive commutative group `(G i)` and an inner product space over `(G i)` and `๐`.
More concisely: In the context of a Hilbert sum of types `G : ฮน โ Type*` over a real numbers-like scalar `๐`, an elementary basis vector in `lp G 2` corresponds to the image of the associated element in `E` under the inverse of the linear isometric isomorphism between `E` and `lp G 2`.
|
IsHilbertSum.surjective_isometry
theorem IsHilbertSum.surjective_isometry :
โ {ฮน : Type u_1} {๐ : Type u_2} [inst : RCLike ๐] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
[inst_2 : InnerProductSpace ๐ E] [cplt : CompleteSpace E] {G : ฮน โ Type u_4}
[inst_3 : (i : ฮน) โ NormedAddCommGroup (G i)] [inst_4 : (i : ฮน) โ InnerProductSpace ๐ (G i)]
{V : (i : ฮน) โ G i โโแตข[๐] E} (self : IsHilbertSum ๐ G V), Function.Surjective โโฏ.linearIsometry
The theorem states that for any type `ฮน`, any type `๐` that behaves like the real or complex numbers, any type `E` that is a normed additive commutative group and an inner product space over `๐`, and any type `G` that is a function from `ฮน` to a type that is a normed additive commutative group and an inner product space over `๐`, the isometry from the Hilbert space `lp G 2` to `E` induced by the orthogonal family `V` is surjective. This means that for every element in `E`, there exists an element in `lp G 2` such that applying the isometry to this element results in the element in `E`. The completeness of the space `E` is also a necessary condition.
More concisely: Given a type `ฮน`, a type `๐` of complex or real numbers, a normed additive commutative group and inner product space `E` over `๐`, and a function `G : ฮน -> normed_add_comm_group E`, the isometry from the Hilbert space `lp G 2` to `E` induced by an orthogonal family `V` is surjective if and only if `E` is complete.
|
lp.summable_inner
theorem lp.summable_inner :
โ {ฮน : Type u_1} {๐ : Type u_2} [inst : RCLike ๐] {G : ฮน โ Type u_4} [inst_1 : (i : ฮน) โ NormedAddCommGroup (G i)]
[inst_2 : (i : ฮน) โ InnerProductSpace ๐ (G i)] (f g : โฅ(lp G 2)), Summable fun i => โชโf i, โg iโซ_๐
This theorem, `lp.summable_inner`, states that for any types `ฮน` and `๐`, where `๐` behaves like a ring-completed line (`RCLike ๐`), and for any function `G` mapping `ฮน` to a type which forms a normed additive commutative group and an inner product space over `๐`, given two elements `f` and `g` of the L^2 space (`lp G 2`), the inner product of the corresponding elements of `f` and `g` (i.e., `โชโf i, โg iโซ_๐`) is summable. In other words, the inner product series converges to a sum.
More concisely: Given a type `ฮน`, a RCLike ring `๐`, and a function `G` mapping `ฮน` to a normed additive commutative group and inner product space over `๐`, for any `f` and `g` in the L^2 space `lp G 2`, the sum of their inner products `โชโf i, โg iโซ_๐` over `ฮน` converges.
|
IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single
theorem IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single :
โ {ฮน : Type u_1} {๐ : Type u_2} [inst : RCLike ๐] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
[inst_2 : InnerProductSpace ๐ E] [cplt : CompleteSpace E] {G : ฮน โ Type u_4}
[inst_3 : (i : ฮน) โ NormedAddCommGroup (G i)] [inst_4 : (i : ฮน) โ InnerProductSpace ๐ (G i)]
{V : (i : ฮน) โ G i โโแตข[๐] E} (hV : IsHilbertSum ๐ G V) (Wโ : ฮ โ (i : ฮน), G i),
hV.linearIsometryEquiv.symm (Wโ.sum (lp.single 2)) = Wโ.sum fun i => โ(V i)
The theorem `IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single` states that for an arbitrary index set `ฮน`, a field `๐` that is a subfield of the complex numbers, a Hilbert space `E` over `๐`, and a family of Hilbert spaces `G i` indexed by `ฮน` also over `๐`, if we have a family of linear isometric embeddings `V i` from `G i` into `E` such that the sum of the images of `V i` is a Hilbert space, then the inverse of the canonical isometric isomorphism between the Hilbert sum of `G i` and the space of `๐`-valued sequences `lp G 2` under this sum map, applied to the sum of the `lp.single 2` applied to a vector `Wโ` in the direct sum of `G i`, is equal to the sum of `V i` applied to the components of `Wโ`. In simpler terms, a finitely-supported vector in the sequence space is the image of the associated finite sum of elements of the Hilbert spaces under the isometric isomorphisms.
More concisely: Given a Hilbert space `E` over a subfield `๐` of the complex numbers, a family `(G\_i)_{i โ ฮน}` of Hilbert spaces over `๐`, and isometric embeddings `V\_i : G\_i โ E`, if the sum of the images of `V\_i` forms a Hilbert space and `Wโ` is a finitely-supported sequence in `E = โ G\_i`, then `(โฅV\_i (lp.single 2 (Wโ ! i))โฅ\_E)^2 = โ (i โ ฮน) โฅV\_i (lp.single 2 (Wโ ! i))โฅยฒโ\_G\_i`, where `lp` refers to the `lp[2]` vector space.
|
IsHilbertSum.OrthogonalFamily
theorem IsHilbertSum.OrthogonalFamily :
โ {ฮน : Type u_1} {๐ : Type u_2} [inst : RCLike ๐] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
[inst_2 : InnerProductSpace ๐ E] [cplt : CompleteSpace E] {G : ฮน โ Type u_4}
[inst_3 : (i : ฮน) โ NormedAddCommGroup (G i)] [inst_4 : (i : ฮน) โ InnerProductSpace ๐ (G i)]
{V : (i : ฮน) โ G i โโแตข[๐] E}, IsHilbertSum ๐ G V โ OrthogonalFamily ๐ G V
This theorem states that for any types `ฮน`, `๐`, `E`, and `G` where `๐` is a ring-like structure, `E` is a normed additive commutative group as well as an inner product space, and `G` is an indexed family of normed additive commutative groups and inner product spaces, if `V` is a mapping that takes each element of `G` into `E` and forms a Hilbert sum, then `V` constitutes an orthogonal family. Here, the Hilbert sum represents an infinite sum in a Hilbert space (a complete inner product space), and an orthogonal family is a collection of vectors where each pair of different vectors is orthogonal (their inner product is zero). The completeness of `E` is also a crucial condition, ensuring that limits exist for all Cauchy sequences in `E`.
More concisely: Given types `ฮน`, `๐`, `E` (a commutative ring-like structure, a complete inner product space, and a Hilbert space), and `G` an indexed family of normed additive commutative groups and inner product spaces, if `V : G โ E` forms a Hilbert sum, then `V` is an orthogonal family.
|
OrthogonalFamily.range_linearIsometry
theorem OrthogonalFamily.range_linearIsometry :
โ {ฮน : Type u_1} {๐ : Type u_2} [inst : RCLike ๐] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
[inst_2 : InnerProductSpace ๐ E] [cplt : CompleteSpace E] {G : ฮน โ Type u_4}
[inst_3 : (i : ฮน) โ NormedAddCommGroup (G i)] [inst_4 : (i : ฮน) โ InnerProductSpace ๐ (G i)]
{V : (i : ฮน) โ G i โโแตข[๐] E} (hV : OrthogonalFamily ๐ G V) [inst_5 : โ (i : ฮน), CompleteSpace (G i)],
LinearMap.range hV.linearIsometry.toLinearMap = (โจ i, LinearMap.range (V i).toLinearMap).topologicalClosure
The theorem `OrthogonalFamily.range_linearIsometry` states that for any type `ฮน`, scalar field type `๐`, normed additive commutative group `E` having an inner product space over `๐` and is a complete space, types `G : ฮน โ Type u_4` forming normed additive commutative groups and inner product spaces over `๐`, and a family of linear isometries `V` from `G i` to `E` for each `i : ฮน` that is mutually orthogonal, the range of the canonical linear isometry on the 2-norm space (`lp 2`) of this family `hV` is equal to the topological closure of the sup (least upper bound) of the ranges of each `V i`. In other words, this theorem states that the range of the canonical linear isometry from the `lp 2` of a mutually orthogonal family of subspaces into the space `E` is the closure of the span of the subspaces.
More concisely: The range of the canonical linear isometry from the 2-normed space of a mutually orthogonal family of subspaces in a complete, inner product space is the topological closure of the span of their ranges.
|