LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.InnerProductSpace.Projection

`orthogonalProjection_orthogonalProjection_of_le` theorem orthogonalProjection_orthogonalProjection_of_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection U] [inst_4 : HasOrthogonalProjection V], U ≤ V → ∀ (x : E), (orthogonalProjection U) ↑((orthogonalProjection V) x) = (orthogonalProjection U) x The theorem `orthogonalProjection_orthogonalProjection_of_le` states that for any real or complex scalar field `𝕜`, a normed add commutative group `E`, and an inner product space over `E` and `𝕜`, if `U` and `V` are submodules of `E` with `U` being a subspace of `V`, then projecting a vector `x` from `E` first onto `V` and then onto `U` is equivalent to directly projecting `x` onto `U`. This is to say, the two-step projection does not alter the end result compared to a direct projection onto `U`. More concisely: For any inner product space `(E, ⟨ situation, situation ⟩)` over a scalar field `𝕜` and subspaces `U` of `V` of `E`, the orthogonal projection of a vector `x` in `E` onto `U` is equal to the orthogonal projection of `x` first onto `V` and then onto `U`.
`eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero` theorem eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] {u v : E}, v ∈ K → (∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0) → orthogonalProjectionFn K u = v The theorem `eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero` asserts that for any types `𝕜` and `E`, where `𝕜` is a ring-like structure (as defined by `RCLike`), `E` is a normed add commutative group and `E` is an inner product space over `𝕜`. If we have a submodule `K` of `E` which has an orthogonal projection and two elements `u` and `v` in `E`, then if `v` lies in `K` and for all `w` in `K`, the inner product of `u - v` and `w` is zero, then the orthogonal projection of `u` onto `K` is `v`. In simpler terms, it states that the orthogonal projection of a vector onto a subspace is the unique point in the subspace that is orthogonal to the original vector. This theorem is mainly used for setting up the bundled version of the orthogonal projection and should not be used once the bundled version is established. More concisely: If `u` is an element of a normed add commutative group `E` over a ring-like structure `𝕜`, `K` is a submodule of `E` with an orthogonal projection, `v` is an element of `K` such that `u - v` is orthogonal to every `w` in `K`, then `v` is the orthogonal projection of `u` onto `K`.
`Submodule.sup_orthogonal_inf_of_completeSpace` theorem Submodule.sup_orthogonal_inf_of_completeSpace : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K₁ K₂ : Submodule 𝕜 E}, K₁ ≤ K₂ → ∀ [inst_3 : HasOrthogonalProjection K₁], K₁ ⊔ K₁.orthogonal ⊓ K₂ = K₂ This theorem states that for any two submodules `K₁` and `K₂` in an inner product space over a ring `𝕜` with a normed commutative additive group structure, if `K₁` is contained in `K₂` and `K₁` is complete, then the linear span of `K₁` and the intersection of `K₁'s` orthogonal complement and `K₂` is equal to `K₂`. In other words, every element in `K₂` can be expressed as a combination of elements from `K₁` and elements from the intersection of `K₁'s` orthogonal complement with `K₂`. More concisely: If `K₁` is a complete submodule of `K₂`, the linear span of `K₁` and the orthogonal complement of `K₁` in `K₂` is equal to `K₂`.
`inner_orthogonalProjection_left_eq_right` theorem inner_orthogonalProjection_left_eq_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [inst_3 : HasOrthogonalProjection K] (u v : E), ⟪↑((orthogonalProjection K) u), v⟫_𝕜 = ⟪u, ↑((orthogonalProjection K) v)⟫_𝕜 The theorem `inner_orthogonalProjection_left_eq_right` states that for any type `𝕜` with Real and Complex number-like behaviors, any type `E` that forms a normed additive commutative group, any inner product space formed over these types `𝕜` and `E`, any submodule `K` of `E` over `𝕜`, and any two elements `u` and `v` of `E`, the inner product of the orthogonal projection of `u` onto `K` with `v` is equal to the inner product of `u` with the orthogonal projection of `v` onto `K`. This is essentially stating that the orthogonal projection operation is self-adjoint. More concisely: For any inner product space over a Real or Complex number-like type `𝕜` with normed additive commutative group `E`, and any submodule `K` of `E`, the orthogonal projection of `u` onto `K` and the orthogonal projection of `v` onto `K` satisfy `〈u.project K, v.project K〉 = 〈u, v.project K〉`, where `〈.,.〉` denotes the inner product.
`orthogonalProjection_minimal` theorem orthogonalProjection_minimal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection U] (y : E), ‖y - ↑((orthogonalProjection U) y)‖ = ⨅ x, ‖y - ↑x‖ The theorem `orthogonalProjection_minimal` states that for any real or complex number type `𝕜`, any normed add commutative group `E`, and any inner product space over `𝕜` and `E`, given a submodule `U` of `E` and any element `y` of `E`, the orthogonality of the projection of `y` onto `U` is such that it minimizes the norm (or distance) of `y - x` for any `x` in `U`. In mathematical terms, this can be written as `‖y - ↑((orthogonalProjection U) y)‖ = ⨅ x, ‖y - ↑x‖`, where `⨅ x` denotes the infimum over all `x` in `U`. More concisely: The orthogonal projection of an element onto a submodule minimizes its distance to any element in the submodule with respect to the given inner product norm.
`orthogonalProjection_add_orthogonalProjection_orthogonal` theorem orthogonalProjection_add_orthogonalProjection_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [inst_3 : HasOrthogonalProjection K] (w : E), ↑((orthogonalProjection K) w) + ↑((orthogonalProjection K.orthogonal) w) = w This theorem states that for a given type `𝕜`, an inner product space `E` over `𝕜`, and a complete submodule `K` of `E`, if the orthogonal projection to `K` is well-defined, any vector `w` in `E` can be written as the sum of its orthogonal projections onto `K` and onto the orthogonal complement of `K`. In other words, each vector in the inner product space is the sum of two orthogonal components: one that lies in the submodule `K` and another that lies in the orthogonal complement of the submodule. More concisely: For any inner product space `(E, <., .>`) over a field `𝕜`, a complete submodule `K ≤ E`, and any `w ∈ E`, if the orthogonal projection `P_K : E → K` exists, then `w = P_K w + P_{K⊥} w`, where `P_{K⊥} : E → K⊥` is the orthogonal projection onto the orthogonal complement of `K`.
`reflection_symm` theorem reflection_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K], (reflection K).symm = reflection K This theorem asserts that the reflection operation in a scalar field 𝕜 and a normed add commutative group E, which also forms an inner product space, is its own inverse. This means that if we reflect a point or vector in a given submodule K (which has an orthogonal projection) of E and then reflect it again, we get back the original point or vector. Essentially, performing the reflection operation twice is the same as doing nothing. More concisely: The reflection operation with respect to a submodule K in a normed add commutative group E, which is also an inner product space over a scalar field, is idempotent, i.e., performing two reflections equals the identity transformation.
`Submodule.orthogonal_orthogonal` theorem Submodule.orthogonal_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [inst_3 : HasOrthogonalProjection K], K.orthogonal.orthogonal = K This theorem states that for a given submodule `K` of an inner product space over a field `𝕜`, if `K` admits an orthogonal projection, then the orthogonal complement of the orthogonal complement of `K` is `K` itself. In other words, applying the operation of finding the orthogonal complement twice on `K` brings us back to `K`. More concisely: If a submodule `K` of an inner product space over a field admits an orthogonal projection, then the orthogonal complement of `K` equals `K`.
`norm_sq_eq_add_norm_sq_projection` theorem norm_sq_eq_add_norm_sq_projection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (x : E) (S : Submodule 𝕜 E) [inst_3 : HasOrthogonalProjection S], ‖x‖ ^ 2 = ‖(orthogonalProjection S) x‖ ^ 2 + ‖(orthogonalProjection S.orthogonal) x‖ ^ 2 This theorem is a form of the Pythagorean theorem in the context of an orthogonal projection. It states that for a given vector `x` and a subspace `S` of an inner product space over a type `𝕜`, if `S` has an orthogonal projection, then the square of the norm of `x` equals the sum of the squares of the norms of the orthogonal projections of `x` onto `S` and the orthogonal complement of `S`. This is analogous to the classic Pythagorean theorem in Euclidean geometry, where the square of the length of the hypotenuse of a right triangle equals the sum of the squares of the lengths of the other two sides. More concisely: For a vector `x` in an inner product space over `𝕜` and a subspace `S` with an orthogonal projection, the square of the norm of `x` equals the sum of the squares of the norms of the orthogonal projections of `x` onto `S` and the orthogonal complement of `S`.
`orthogonalProjection_singleton` theorem orthogonalProjection_singleton : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {v : E} (w : E), ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = (⟪v, w⟫_𝕜 / ↑(‖v‖ ^ 2)) • v The theorem `orthogonalProjection_singleton` provides a formula for the orthogonal projection of a vector onto a single vector. Given a type `𝕜` (which we will assume to be a real or complex number type), a normed additive commutative group `E` (which is the space our vectors are in) and an inner product space over `𝕜` and `E`, for any two vectors `v` and `w` in `E`, the orthogonal projection of `w` onto the submodule spanned by `{v}` is equal to the scalar product of `v` and `w`, divided by the squared norm of `v`, all scaled by `v`. Here, `⟪v, w⟫_𝕜` represents the inner product of `v` and `w`, `‖v‖` denotes the norm of `v`, and the function `orthogonalProjection` is used to denote orthogonal projection onto a given submodule. More concisely: The orthogonal projection of a vector `w` onto the subspace spanned by a single vector `v` is equal to the scalar product of `v` and `w`, divided by the squared norm of `v`.
`OrthogonalFamily.projection_directSum_coeAddHom` theorem OrthogonalFamily.projection_directSum_coeAddHom : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} [inst_3 : DecidableEq ι] {V : ι → Submodule 𝕜 E}, (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) → ∀ (x : DirectSum ι fun i => ↥(V i)) (i : ι) [inst_4 : CompleteSpace ↥(V i)], (orthogonalProjection (V i)) ((DirectSum.coeAddMonoidHom V) x) = x i This theorem states that given a family of submodules `V` of a normed additive commutative group `E` over field `𝕜` that are orthogonal, the orthogonal projection onto a subspace `V i` of the direct sum of the family (converted to `E` via the canonical embedding) is equal to the coefficient of the direct sum at `i`. Specifically, for any element `x` of the direct sum and any index `i`, if the subspace `V i` is complete, then the orthogonal projection of `x` onto `V i` (after converting `x` to `E`) is exactly the `i`-th component of `x`. This theorem essentially provides a way to recover the components of a direct sum from its orthogonal projection onto the corresponding subspaces. More concisely: Given a family of orthogonal, complete subspaces of a normed additive commutative group over a field, the orthogonal projection onto each subspace equals the corresponding component in the direct sum.
`Dense.eq_of_sub_mem_orthogonal` theorem Dense.eq_of_sub_mem_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} {x y : E}, Dense ↑K → x - y ∈ K.orthogonal → x = y The theorem `Dense.eq_of_sub_mem_orthogonal` states that for any real or complex scalar type `𝕜` and any normed additive commutative group `E` that is also an inner product space over `𝕜`, if a submodule `K` of `E` is dense in the topological space sense, and the difference `x - y` belongs to the orthogonal complement of `K`, then `x` equals `y`. In simpler terms, this theorem shows that if we have two vectors `x` and `y` in a dense submodule, and their difference falls in the orthogonal complement of the submodule, then the two vectors must be identical. More concisely: If a dense submodule of a normed additive commutative group and inner product space over the real or complex scalar type contains the difference of two vectors, then these vectors are equal.
`LinearIsometryEquiv.reflections_generate_dim_aux` theorem LinearIsometryEquiv.reflections_generate_dim_aux : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] [inst_2 : FiniteDimensional ℝ F] {n : ℕ} (φ : F ≃ₗᵢ[ℝ] F), FiniteDimensional.finrank ℝ ↥(LinearMap.ker (ContinuousLinearMap.id ℝ F - ↑{ toLinearEquiv := φ.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })).orthogonal ≤ n → ∃ l, l.length ≤ n ∧ φ = (List.map (fun v => reflection (Submodule.span ℝ {v}).orthogonal) l).prod This theorem states that for a given element `φ` of the orthogonal group of a finite dimensional normed add-commutative group `F` with an inner product space over the real numbers, `φ` can be expressed as a product of reflections. More specifically, the number of reflections needed is at most equal to the dimension of the orthogonal complement of the fixed subspace of `φ`. That is, if the difference between the identity map and `φ` has a kernel with rank less than or equal to `n`, then there exists a list of vectors `l` with a length less than or equal to `n` such that `φ` is the product of the reflections across the orthogonal complements of the spans of the vectors in `l`. More concisely: For any orthogonal transformation `φ` of a finite dimensional inner product space over the real numbers, the number of reflections needed to express `φ` as a product is at most equal to the dimension of the orthogonal complement of `φ`'s fixed subspace.
`reflection_apply` theorem reflection_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] (p : E), (reflection K) p = 2 • ↑((orthogonalProjection K) p) - p The theorem `reflection_apply` states that for any type `𝕜`, any normed add commutative group `E`, and any inner product space over `𝕜` and `E`, given a submodule `K` of `E` over `𝕜` and any point `p` in `E`, the result of reflecting `p` over `K` equals to twice the orthogonal projection of `p` onto `K` minus `p` itself. This is written mathematically in LaTeX as: for all `p` in `E`, `(reflection K) p = 2 * ((orthogonalProjection K) p) - p`. More concisely: The reflection of a point `p` in a submodule `K` of an inner product space equals twice the orthogonal projection of `p` onto `K` minus `p`.
`reflection_mem_subspace_orthogonal_precomplement_eq_neg` theorem reflection_mem_subspace_orthogonal_precomplement_eq_neg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] {v : E}, v ∈ K → (reflection K.orthogonal) v = -v This theorem states that for any element `v` in a given subspace `K` of an inner product space over a field `𝕜`, the reflection of `v` in the orthogonal complement of `K` is equal to the negation of `v`. This holds true under the assumption that `K` has an orthogonal projection. The involved structures include a ring-like structure `𝕜`, a normed add commutative group `E`, and an inner product space over `𝕜` and `E`. More concisely: For any subspace `K` of an inner product space over a field `𝕜` with orthogonal projection, the reflection of an element `v` in `K`'s orthogonal complement is equal to the negation of `v`.
`orthogonalProjection_bot` theorem orthogonalProjection_bot : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E], orthogonalProjection ⊥ = 0 This theorem states that the orthogonal projection onto the trivial submodule is the zero map. In the context of a given scalar field `𝕜` and a normed add commutative group `E`, where `E` is an inner product space over `𝕜`, the orthogonal projection onto the trivial (or zero) submodule always results in the zero map. This means that any vector projected orthogonally onto the subspace consisting only of the zero vector will be mapped to the zero vector. More concisely: The orthogonal projection of any vector onto the trivial subspace of an inner product space is the zero vector.
`Submodule.topologicalClosure_eq_top_iff` theorem Submodule.topologicalClosure_eq_top_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : CompleteSpace E], K.topologicalClosure = ⊤ ↔ K.orthogonal = ⊥ The theorem `Submodule.topologicalClosure_eq_top_iff` states that, for any type 𝕜 and any normed additively commutative group E with an inner product space over 𝕜, if E is a complete space, then the topological closure of a submodule K of E equals the entire space if and only if the orthogonal complement of K is the zero submodule. In simpler terms, it means that a set in a complete inner product space spans the whole space if and only if its orthogonal complement is trivial. More concisely: In a complete inner product space, a submodule spans the whole space if and only if its orthogonal complement is the zero submodule.
`LinearIsometryEquiv.reflections_generate` theorem LinearIsometryEquiv.reflections_generate : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] [inst_2 : FiniteDimensional ℝ F], Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v}).orthogonal) = ⊤ This theorem states that for any normed additive commutative group `F` equipped with an inner product space structure over the real numbers `ℝ` and for which `F` is also a finite-dimensional vector space over `ℝ`, the orthogonal group of `F` is generated by reflections. Here, a reflection is defined on the orthogonal complement of the one-dimensional subspace spanned by each vector `v` in `F`. In other words, the closure of the set of all such reflections forms the entire orthogonal group of `F`, denoted by `⊤`. More concisely: For any finite-dimensional, normed additive commutative group `F` over the real numbers `ℝ` with an inner product space structure, the orthogonal group `⊤` is generated by reflections on the orthogonal complements of one-dimensional subspaces.
`OrthogonalFamily.isInternal_iff` theorem OrthogonalFamily.isInternal_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} [inst_3 : DecidableEq ι] [inst_4 : FiniteDimensional 𝕜 E] {V : ι → Submodule 𝕜 E}, (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) → (DirectSum.IsInternal V ↔ (iSup V).orthogonal = ⊥) The theorem `OrthogonalFamily.isInternal_iff` states that for any given type `𝕜`, type `E`, type `ι`, and a family of subspaces `V : ι → Submodule 𝕜 E` in an inner product space over the type `E` with inner product defined over `𝕜`, where `𝕜` behaves like a division ring and `E` is a normed commutative additive group, and also `E` is finite dimensional over `𝕜`, with a decidable equality over `ι`, if the family `V` is orthogonal (denoted by `OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ`), then the family `V` forms an internal direct sum decomposition of `E` (denoted by `DirectSum.IsInternal V`) if and only if the orthogonal complement of the supremum of the subspaces `V` is trivial (denoted by `(iSup V).orthogonal = ⊥`). More concisely: For an orthogonal family of subspaces in a finite-dimensional inner product space over a division ring with decidable equality, the family forms an internal direct sum decomposition if and only if the orthogonal complement of their supremum is the trivial subspace.
`reflection_mem_subspace_orthogonalComplement_eq_neg` theorem reflection_mem_subspace_orthogonalComplement_eq_neg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] {v : E}, v ∈ K.orthogonal → (reflection K) v = -v This theorem states that for any field 𝕜, and for any normed additively commutative group E that is also an inner product space over 𝕜, given a submodule K of E (which also has an orthogonal projection), if a vector v is in the orthogonal complement of K, then the reflection of v in K is equal to the negation of v. In other words, if a vector is orthogonal to a subspace, its reflection in that subspace is just its negative. More concisely: For any normed additively commutative group E over a field 𝕜 that is also an inner product space, the reflection of a vector orthogonal to a submodule K of E is equal to its negative within K.
`eq_orthogonalProjection_of_mem_orthogonal'` theorem eq_orthogonalProjection_of_mem_orthogonal' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] {u v z : E}, v ∈ K → z ∈ K.orthogonal → u = v + z → ↑((orthogonalProjection K) u) = v The theorem `eq_orthogonalProjection_of_mem_orthogonal'` states that for any types `𝕜` and `E`, where `𝕜` is a type that behaves like real or complex numbers (`RCLike 𝕜`), `E` is a normed additive commutative group (`NormedAddCommGroup E`), and `E` has an inner product structure (`InnerProductSpace 𝕜 E`), if we have a submodule `K` of `E` for which an orthogonal projection is defined (`HasOrthogonalProjection K`), and if we have any three elements `u`, `v`, and `z` from `E` such that `v` belongs to `K`, `z` is orthogonal to `K` (`z ∈ K.orthogonal`), and `u` is the sum of `v` and `z` (`u = v + z`), then the orthogonal projection of `u` onto `K` is equal to `v`. This theorem is a key result in the theory of orthogonal projection onto subspaces in inner product spaces. More concisely: If `K` is a submodule of a normed additive commutative group `E` with an inner product structure and has an orthogonal projection, then for any `u = v + z` in `E` with `v` in `K` and `z` orthogonal to `K`, the orthogonal projection of `u` onto `K` equals `v`.
`finrank_orthogonal_span_singleton` theorem finrank_orthogonal_span_singleton : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {n : ℕ} [_i : Fact (FiniteDimensional.finrank 𝕜 E = n + 1)] {v : E}, v ≠ 0 → FiniteDimensional.finrank 𝕜 ↥(Submodule.span 𝕜 {v}).orthogonal = n The theorem `finrank_orthogonal_span_singleton` states that for any inner product space `E` over a field `𝕜` of finite dimension `n+1`, if we take any nonzero vector `v` from the space `E`, the dimension of the orthogonal complement of the span of the vector `v` would be `n`. In other words, in a finite-dimensional inner product space, the dimension of the space orthogonal to the space spanned by a nonzero vector is one less than the total dimension of the space. More concisely: In a finite-dimensional inner product space, the dimension of the orthogonal complement of a nonzero vector's span is equal to the difference between the total dimension and one.
`orthogonalProjection_inner_eq_zero` theorem orthogonalProjection_inner_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] (v w : E), w ∈ K → ⟪v - ↑((orthogonalProjection K) v), w⟫_𝕜 = 0 The theorem named `orthogonalProjection_inner_eq_zero` characterizes the orthogonal projection onto a complete subspace. Specifically, it states that for any type 𝕜, any normed additive commutative group E, and any inner product space over 𝕜 and E, if we have a submodule K of E and K has an orthogonal projection, then for any two vectors (v and w) in E, if w is in K, the inner product of the difference between v and the orthogonal projection of v onto K with w equals zero. This is essentially the property that defines orthogonal projections: the difference between a vector and its projection onto a subspace is orthogonal to every vector in the subspace. More concisely: If a subspace K of a normed additive commutative group E over a field 𝕜 has an orthogonal projection, then for all vectors v, w in E with w in K, the inner product of v − P(v) and w equals zero, where P(v) is the orthogonal projection of v onto K.
`eq_orthogonalProjection_of_mem_of_inner_eq_zero` theorem eq_orthogonalProjection_of_mem_of_inner_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] {u v : E}, v ∈ K → (∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0) → ↑((orthogonalProjection K) u) = v The theorem `eq_orthogonalProjection_of_mem_of_inner_eq_zero` states that for any type `𝕜`, a normed additive commutative group `E` with a structure of an inner product space over `𝕜`, and a submodule `K` of `E` with a valid orthogonal projection, if a vector `v` from `E` belongs to `K` and for every vector `w` in `K`, the inner product of `u - v` and `w` equals 0, then `v` is the orthogonal projection of `u` onto `K`. In simpler terms, it states that the orthogonal projection of a vector onto a subspace is the unique point in the subspace that maintains orthogonality (i.e., the inner product equals zero) with all other vectors in the subspace. More concisely: If a vector `v` in a normed additive commutative group `E` with an inner product is in a submodule `K` and is orthogonal to every vector `w` in `K`, then `v` is the orthogonal projection of any vector `u` in `E` onto `K`.
`maximal_orthonormal_iff_basis_of_finiteDimensional` theorem maximal_orthonormal_iff_basis_of_finiteDimensional : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {v : Set E} [inst_3 : FiniteDimensional 𝕜 E], Orthonormal 𝕜 Subtype.val → ((∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ ∃ b, ⇑b = Subtype.val) The theorem `maximal_orthonormal_iff_basis_of_finiteDimensional` states that in a finite-dimensional inner product space, an orthonormal set is maximal if and only if it forms a basis. In the context of this theorem, a set is 'maximal' if it cannot be properly contained within any other set that also satisfies the property of being orthonormal. Specifically, for a set of vectors `v` in an inner product space `E` over a field `𝕜`, the set `v` is maximal and orthonormal if and only if there exists a basis `b` such that the function `⇑b` is equal to the `Subtype.val` function, which extracts the underlying element from the subtype representing `v`. More concisely: In a finite-dimensional inner product space, an orthonormal set is maximal if and only if it is a basis.
`Submodule.isCompl_orthogonal_of_completeSpace` theorem Submodule.isCompl_orthogonal_of_completeSpace : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K], IsCompl K K.orthogonal This theorem states that for any field `𝕜` and any normed add-commutative group `E` that forms an inner product space over `𝕜`, if a submodule `K` of `E` admits an orthogonal projection, then `K` and the orthogonal complement of `K` (denoted `Kᗮ`) are complements of each other. In the context of vector spaces, two subspaces being complements means that every vector in the space can be uniquely written as the sum of a vector in one subspace and a vector in the other subspace. More concisely: If a submodule `K` of a normed add-commutative group `E` over a field `𝕜`, which forms an inner product space, has an orthogonal projection, then `K` and its orthogonal complement `Kᗮ` are complementary subspaces.
`orthogonalProjection_unit_singleton` theorem orthogonalProjection_unit_singleton : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {v : E}, ‖v‖ = 1 → ∀ (w : E), ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = ⟪v, w⟫_𝕜 • v This theorem states that for any field 𝕜, equipped with a real-like structure (rclike 𝕜), and any normed additively commutative group E that forms an inner product space over 𝕜, given a vector v in E with norm equal to 1, the orthogonal projection of any vector w in E onto the span of {v} (which is the smallest subspace of E containing {v}) is equal to the inner product of v and w scaled by vector v. Intuitively, this describes the process of projecting a vector onto the line defined by a unit vector. More concisely: For any normed inner product space E over a real-like field 𝕜, the orthogonal projection of a vector w onto the line through the unit vector v is equal to the inner product of v and w, scaled by v.
`Submodule.finrank_add_inf_finrank_orthogonal` theorem Submodule.finrank_add_inf_finrank_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K₁ K₂ : Submodule 𝕜 E} [inst_3 : FiniteDimensional 𝕜 ↥K₂], K₁ ≤ K₂ → FiniteDimensional.finrank 𝕜 ↥K₁ + FiniteDimensional.finrank 𝕜 ↥(K₁.orthogonal ⊓ K₂) = FiniteDimensional.finrank 𝕜 ↥K₂ This theorem states that for a given finite-dimensional subspace `K₂` and a subspace `K₁` contained in it, the sum of the dimensions of `K₁` and the intersection of its orthogonal subspace with `K₂` equals the dimension of `K₂`. Here, `𝕜` is the field over which the spaces are defined, `E` is the vector space, `K₁` and `K₂` are subspaces of `E`, `K₁.orthogonal` is the orthogonal subspace of `K₁`, and `FiniteDimensional.finrank 𝕜 ↥K₁` represents the dimension of the subspace `K₁`. This is a result in the field of linear algebra, specifically dealing with the relationship between a subspace, its orthogonal complement, and their dimensions. More concisely: The theorem states that the dimension of a finite-dimensional subspace `K₁` and the intersection of `K₁` with its orthogonal complement in a larger finite-dimensional subspace `K₂` sum up to the dimension of `K₂`.
`orthogonalProjection_orthogonalComplement_singleton_eq_zero` theorem orthogonalProjection_orthogonalComplement_singleton_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (v : E), (orthogonalProjection (Submodule.span 𝕜 {v}).orthogonal) v = 0 This theorem states that for any vector `v` in an inner product space `E` over a field `𝕜`, the orthogonal projection of `v` onto the orthogonal complement of the span of `v` is zero. In other words, the projection of a vector on the space orthogonal to it is always the zero vector. This is an expected result, as a vector has no component along a direction that is orthogonal to it. More concisely: For any vector `v` in an inner product space `E`, the orthogonal projection of `v` onto the orthogonal complement of `v`'s span is the zero vector.
`Submodule.finrank_add_finrank_orthogonal` theorem Submodule.finrank_add_finrank_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : FiniteDimensional 𝕜 E] (K : Submodule 𝕜 E), FiniteDimensional.finrank 𝕜 ↥K + FiniteDimensional.finrank 𝕜 ↥K.orthogonal = FiniteDimensional.finrank 𝕜 E This theorem states that for a given finite-dimensional space `E` and a subspace `K` of `E`, the sum of the dimensions of `K` and its orthogonal complement `Kᗮ` is equal to the dimension of `E`. Here, `𝕜` is the field over which the spaces are defined, `NormedAddCommGroup E` asserts that `E` is a normed additive commutative group, `InnerProductSpace 𝕜 E` means that `E` is an inner product space over `𝕜`, and `FiniteDimensional 𝕜 E` indicates that `E` is a finite-dimensional space over `𝕜`. The dimensions are computed using the function `FiniteDimensional.finrank 𝕜 X`, where `X` is the space or subspace in question. More concisely: For any finite-dimensional inner product space `E` and subspace `K` over a field `𝕜`, the dimensions of `K` and its orthogonal complement satisfy `FiniteDimensional.finrank 𝕜 K + FiniteDimensional.finrank 𝕜 (Kᗮ) = FiniteDimensional.dim 𝕜 E`.
`exists_norm_eq_iInf_of_complete_subspace` theorem exists_norm_eq_iInf_of_complete_subspace : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E), IsComplete ↑K → ∀ (u : E), ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖ The theorem `exists_norm_eq_iInf_of_complete_subspace` states that for every point `u` in a given inner product space, and for a given non-empty complete subspace `K`, there exists a unique point `v` in `K` such that the norm of the difference between `u` and `v` is equal to the infimum of the norms of `u` minus every other point in the subspace `K`. This point `v` minimizes the distance between `u` and `K`, and is typically referred to as the orthogonal projection of `u` onto `K`. More concisely: For every point `u` in an inner product space and complete subspace `K`, there exists a unique point `v` in `K` such that the norm of `u - v` equals the infimum of the norms of `u - x` for all `x` in `K`.
`norm_eq_iInf_iff_real_inner_le_zero` theorem norm_eq_iInf_iff_real_inner_le_zero : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {K : Set F}, Convex ℝ K → ∀ {u v : F}, v ∈ K → (‖u - v‖ = ⨅ w, ‖u - ↑w‖ ↔ ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0) This theorem states that for a given convex set K in a real inner product space, and for any two elements u and v from that space, where v is an element of K, the norm (or length) of the difference between u and v is equal to the infimum (greatest lower bound) of the norms of the differences between u and any element w, if and only if the inner product of the difference between u and v with the difference between w and v is less than or equal to zero for all w in K. In other words, it characterizes the conditions under which a point v in the convex set K is the closest point in K to another point u in the space. More concisely: Given a convex set K in a real inner product space and u, v in the space with v in K, u-v has the smallest norm among all u-w for w in K if and only if (u-v).(w-v) ≤ 0 for all w in K.
`Submodule.finrank_add_finrank_orthogonal'` theorem Submodule.finrank_add_finrank_orthogonal' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : FiniteDimensional 𝕜 E] {K : Submodule 𝕜 E} {n : ℕ}, FiniteDimensional.finrank 𝕜 ↥K + n = FiniteDimensional.finrank 𝕜 E → FiniteDimensional.finrank 𝕜 ↥K.orthogonal = n This theorem states that for a given finite-dimensional space `E` and a subspace `K` of `E` over a division ring `𝕜`, if the sum of the dimensions of `K` and some natural number `n` equals the dimension of `E`, then the dimension of the orthogonal complement of `K` in `E` is equal to `n`. In other words, it encapsulates the idea that the dimensions of a subspace and its orthogonal complement in a finite-dimensional space add up to the dimension of the entire space. More concisely: If the dimensions of a subspace and its orthogonal complement in a finite-dimensional space over a division ring sum to the space's dimension, then they are complementary and have the specified dimensions.
`maximal_orthonormal_iff_orthogonalComplement_eq_bot` theorem maximal_orthonormal_iff_orthogonalComplement_eq_bot : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {v : Set E}, Orthonormal 𝕜 Subtype.val → ((∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ (Submodule.span 𝕜 v).orthogonal = ⊥) The theorem `maximal_orthonormal_iff_orthogonalComplement_eq_bot` states that for any field `𝕜` and any Normed Additive Commutative Group `E` that also has an inner product structure, given a set `v` of elements in `E`, if the elements, when treated as vectors, form an orthonormal set, then the set `v` is maximal or cannot be enlarged while preserving the orthonormal property if and only if the orthogonal complement of the span of `v` (which is the set of vectors in `E` orthogonal to every vector in the span of `v`) is the zero vector or trivial subspace. In other words, a set of vectors is a maximal orthonormal set if and only if there are no vectors orthogonal to all vectors in the set (except for the zero vector). More concisely: A set of vectors in a normed additive commutative group with an inner product structure is maximal orthonormal if and only if the orthogonal complement of their span is the zero vector.
`reflection_eq_self_iff` theorem reflection_eq_self_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] (x : E), (reflection K) x = x ↔ x ∈ K This theorem states that for any point `x` in an inner product space `E` over a field `𝕜`, the reflection of `x` in a subspace `K` of `E` is equal to `x` if and only if `x` is an element of the subspace `K`. Here, `𝕜` is a field that behaves like real or complex numbers, `NormedAddCommGroup E` implies the inner product space `E` is a normed additive commutative group, and `HasOrthogonalProjection K` means that the subspace `K` has an orthogonal projection. The inner product space, subspace, and the point are all parameters to the theorem. The reflection operation is defined in the context of the inner product space and the specified subspace. More concisely: For an inner product space E over field 𝕜 with subspace K having an orthogonal projection, the reflection of a point x in K is equal to x if and only if x is an element of K.
`orthogonalProjection_tendsto_self` theorem orthogonalProjection_tendsto_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {ι : Type u_4} [inst_4 : SemilatticeSup ι] (U : ι → Submodule 𝕜 E) [inst_5 : ∀ (t : ι), CompleteSpace ↥(U t)], Monotone U → ∀ (x : E), ⊤ ≤ (⨆ t, U t).topologicalClosure → Filter.Tendsto (fun t => ↑((orthogonalProjection (U t)) x)) Filter.atTop (nhds x) The theorem `orthogonalProjection_tendsto_self` states that given a monotone family `U` of complete submodules of a normed add commutative group `E`, under a field `𝕜` endowed with an inner product, where `U` has a dense span supremum and for every `t`, the type `U t` is a complete space. If we take any element `x` from `E` such that this element `x` is an element of the topological closure of the least upper bound of `U`, then the orthogonal projection of `x` on `U t` tends to `x` as `t` tends to infinity. In simpler terms, the orthogonal projections of a point onto a growing sequence of subspaces eventually converges to the point when the supremum of the subspaces densely spans the entire space. More concisely: Given a monotone family of complete subspaces of a normed add commutative group with dense span supremum, the orthogonal projection of any element in the topological closure of the supremum onto each subspace converges to that element as the subspace grows.
`orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero` theorem orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] {v : E}, v ∈ K.orthogonal → (orthogonalProjection K) v = 0 The theorem `orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero` states that for an arbitrary type `𝕜`, type `E`, where `𝕜` forms a RingLike structure, `E` forms a NormedAddCommGroup, and `E` with `𝕜` forms an InnerProductSpace; for any submodule `K` of `E` over `𝕜`, if we have an orthogonal projection onto `K`, then for any element `v` of `E`, if `v` belongs to the orthogonal complement of `K` (denoted as `K.orthogonal`), the orthogonal projection of `v` onto `K` is zero. In mathematical terms, if a vector is orthogonal to a subspace, its orthogonal projection onto that subspace is the zero vector. More concisely: For any submodule `K` of a normed additive commutative group `E` over a ring `𝕜` in an inner product space, the orthogonal projection of any vector `v` in the orthogonal complement of `K` onto `K` is the zero vector.
`OrthogonalFamily.isInternal_iff_of_isComplete` theorem OrthogonalFamily.isInternal_iff_of_isComplete : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} [inst_3 : DecidableEq ι] {V : ι → Submodule 𝕜 E}, (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) → IsComplete ↑(iSup V) → (DirectSum.IsInternal V ↔ (iSup V).orthogonal = ⊥) This theorem states that, given a field `𝕜`, a normed additive commutative group `E`, an inner product space structure on `E` over `𝕜`, and an index set `ι`, for any family `V` of submodules of `E` indexed by `ι` (where equality of indices is decidable), if this family is orthogonal (i.e., each pair of different submodules are orthogonal in the sense of inner product spaces), then the family `V` provides an internal direct sum decomposition of `E` if and only if the orthogonal complement of the span of the family `V` is trivial. The completeness of the span of the family `V` is a prerequisite for the theorem. More concisely: A family of subspaces of a normed additive commutative group with an inner product space structure over a field forms an internal direct sum if and only if it is orthogonal and the orthogonal complement of their span is trivial, given decidable index equality and completeness of the span.
`orthogonalProjection_isSymmetric` theorem orthogonalProjection_isSymmetric : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [inst_3 : HasOrthogonalProjection K], (K.subtypeL.comp (orthogonalProjection K)).IsSymmetric The theorem states that the orthogonal projection is symmetric. Specifically, for any type `𝕜` with a ring-complement-like structure, any type `E` that forms a normed additive commutative group, and any inner product space over `𝕜` and `E`, if we have a submodule `K` of `E` over `𝕜` that has an orthogonal projection, then the composition of `K.subtypeL` (which is a continuous linear map from `K` to `E`) and the orthogonal projection from `E` to `K` is symmetric. In mathematical terms, if we denote the orthogonal projection by `P_K`, then the map `P_K ∘ i_K` is symmetric, where `i_K` is the inclusion map of `K` into `E`. More concisely: For any inner product space over a ring-complemented normed additive commutative group and any submodule with an orthogonal projection, the orthogonal projection and its restriction to the submodule form a commuting pair.
`norm_eq_iInf_iff_inner_eq_zero` theorem norm_eq_iInf_iff_inner_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) {u v : E}, v ∈ K → (‖u - v‖ = ⨅ w, ‖u - ↑w‖ ↔ ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0) This theorem characterizes the points in a subspace that minimize their distance to a given point in an inner product space. Specifically, given a point `u` in an inner product space, a nonempty subspace `K`, and a point `v` in `K`, the distance `‖u - v‖` is minimized over all points in `K` if and only if for all `w` in `K`, the inner product `⟪u - v, w⟫` is zero. This essentially means that `u - v` is orthogonal to every vector in the subspace `K`. More concisely: In an inner product space, a point in a subspace minimizes the distance to a given point if and only if it is orthogonal to every vector in the subspace with respect to that point.
`OrthogonalFamily.sum_projection_of_mem_iSup` theorem OrthogonalFamily.sum_projection_of_mem_iSup : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {ι : Type u_4} [inst_3 : Fintype ι] {V : ι → Submodule 𝕜 E} [inst_4 : ∀ (i : ι), CompleteSpace ↥(V i)], (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) → ∀ x ∈ iSup V, (Finset.univ.sum fun i => ↑((orthogonalProjection (V i)) x)) = x The theorem `OrthogonalFamily.sum_projection_of_mem_iSup` states that for any real or complex number type `𝕜`, any type `E` that is a normed add commutative group and an inner product space over `𝕜`, any type `ι` that has a finite number of distinct values, and any function `V` from `ι` to submodules of `E` over `𝕜`, such that each co-domain of `V` is a complete space and the family of linear isometries from co-domains of `V` to `E` is orthogonal, then for any element `x` that lies in the supremum of the range of `V`, `x` can be expressed as the sum of the orthogonal projections of `x` onto each submodule in `V`, where the sum is taken over all elements of `ι`. In other words, if `x` lies within an orthogonal family `V`, it can be expressed as a sum of projections onto each element of the family. More concisely: Given a finite family `V` of orthogonal complete subspaces of a normed add commutative group and inner product space `E` over a field `𝕜`, any element `x` in the closure of their union can be represented as the orthogonal sum of the projections of `x` onto each subspace in `V`.
`orthogonalProjectionFn_inner_eq_zero` theorem orthogonalProjectionFn_inner_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] (v w : E), w ∈ K → ⟪v - orthogonalProjectionFn K v, w⟫_𝕜 = 0 The theorem `orthogonalProjectionFn_inner_eq_zero` characterizes the unbundled orthogonal projection in an inner product space. Specifically, for any types `𝕜` under a Ring-Commutative-Like structure and `E` under a Normed Additive Commutative Group structure, and for `𝕜` as an Inner Product Space over `E`, given any submodule `K` of `E` that supports orthogonal projection, the theorem states that for any vectors `v` and `w` in `E`, if `w` is an element of `K`, then the inner product of the difference between `v` and the orthogonal projection of `v` onto `K` with `w` equals zero. In essence, this theorem captures the orthogonality condition inherent in orthogonal projections. More concisely: For any inner product space `(𝕜, E)` over a ring `𝕜`, and submodule `K` of `E` supporting orthogonal projection, if `w` is in `K`, then the inner product of `v - 𝔄_K v` with `w` equals zero for all `v` in `E`, where `𝔄_K v` denotes the orthogonal projection of `v` onto `K`.
`Submodule.IsOrtho.orthogonalProjection_comp_subtypeL` theorem Submodule.IsOrtho.orthogonalProjection_comp_subtypeL : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection U], U.IsOrtho V → (orthogonalProjection U).comp V.subtypeL = 0 The theorem `Submodule.IsOrtho.orthogonalProjection_comp_subtypeL` states that for any types `𝕜` and `E` where `𝕜` is a ring-like structure, `E` is a normed additive commutative group, and `E` is an inner product space over `𝕜`, given two submodules `U` and `V` of `E`, if `U` is orthogonal to `V`, then the composition of the orthogonal projection onto `U` and the embedding of `V` into `E` (denoted by `V.subtypeL`) is the zero linear map. In other words, if `U` and `V` are orthogonal subspaces, projecting from `V` into `U` gives the zero map. More concisely: If submodules $U$ and $V$ of a normed additive commutative group $E$ over a ring-like structure ${\mathbb{R}}$ are orthogonal, then the composition of the orthogonal projection onto $U$ and the embedding of $V$ into $E$ is the zero linear map.
`orthogonalProjection_mem_subspace_eq_self` theorem orthogonalProjection_mem_subspace_eq_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] (v : ↥K), (orthogonalProjection K) ↑v = v This theorem states that for any type `𝕜` and `E` where `𝕜` behaves like a ring and `E` is a normed commutative group with an inner product space over `𝕜`, given a submodule `K` of `E` that has an orthogonal projection, the orthogonal projection of any element `v` of `K` onto `K` is just `v` itself. In other words, the orthogonal projection function leaves the elements of `K` unchanged. More concisely: Let `𝕜` be a ring, `E` a normed commutative `𝕜`-module with an inner product, and `K` a submodule of `E` with an orthogonal projection. Then for all `v` in `K`, `P_K(v) = v`, where `P_K` denotes the orthogonal projection onto `K`.
`orthogonalProjection_norm_le` theorem orthogonalProjection_norm_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [inst_3 : HasOrthogonalProjection K], ‖orthogonalProjection K‖ ≤ 1 The theorem `orthogonalProjection_norm_le` states that for any type `𝕜` which behaves like a real or complex number, type `E` which is a normed additive commutative group, and inner product space over `𝕜` and `E`, and for any submodule `K` of `E` that has an orthogonal projection, the norm of the orthogonal projection onto `K` is less than or equal to 1. More concisely: For any normed additive commutative group `E` over a real or complex number field `𝕜`, with an inner product and a submodule `K` having an orthogonal projection, the norm of this projection is bounded by 1.
`eq_orthogonalProjection_of_mem_orthogonal` theorem eq_orthogonalProjection_of_mem_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] {u v : E}, v ∈ K → u - v ∈ K.orthogonal → ↑((orthogonalProjection K) u) = v This theorem states that for any two vectors `u` and `v` in a normed additive commutative group `E` over a ring `𝕜` with an inner product space structure, if `v` lies in a submodule `K` of `E` and the difference `u - v` is orthogonal to `K` (lies in the orthogonal complement of `K`), then `v` is in fact the orthogonal projection of `u` onto `K`. This provides a characterization of the orthogonal projection in terms of orthogonality properties. More concisely: If a vector `v` in a normed additive commutative group `E` over a ring `𝕜` with an inner product space structure lies in a submodule `K` and is orthogonal to the difference of any vector `u` in `E` and `v`, then `v` is the orthogonal projection of `u` onto `K`.
`eq_orthogonalProjection_of_eq_submodule` theorem eq_orthogonalProjection_of_eq_submodule : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] {K' : Submodule 𝕜 E} [inst_4 : HasOrthogonalProjection K'], K = K' → ∀ (u : E), ↑((orthogonalProjection K) u) = ↑((orthogonalProjection K') u) The theorem `eq_orthogonalProjection_of_eq_submodule` states that for any real or complex scalars `𝕜`, normed add commutative group `E`, and inner product space over `𝕜` and `E`, given two submodules `K` and `K'` of `E` that both have orthogonal projections, if `K` and `K'` are equal, then for any element `u` in `E`, the orthogonal projections of `u` onto `K` and `K'` are the same when they are coerced back to points in `E`. In other words, equivalent subspaces share the same orthogonal projections. More concisely: If two equal subspaces `K` and `K'` of a normed add commutative group `E` over real or complex scalars, both with orthogonal projections, have identical orthogonal projections for any element `u` in `E`.
`Submodule.sup_orthogonal_of_completeSpace` theorem Submodule.sup_orthogonal_of_completeSpace : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K], K ⊔ K.orthogonal = ⊤ This theorem states that for any complete space `K` within an inner product space over a ring-like structure `𝕜`, the span of `K` and its orthogonal complement `Kᗮ` equals the whole space. In other words, every point in the space can be expressed as the sum of a point in `K` and a point in `Kᗮ`. More concisely: For any complete subspace `K` of an inner product space over a ring-like structure `𝕜`, the span of `K` and its orthogonal complement `Kᗮ` equals the entire space.
`reflection_map_apply` theorem reflection_map_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_4} {E' : Type u_5} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup E'] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (K : Submodule 𝕜 E) [inst_5 : HasOrthogonalProjection K] (x : E'), (reflection (Submodule.map (↑f.toLinearEquiv) K)) x = f ((reflection K) (f.symm x)) This theorem is about the reflection of a point in the image of a subspace under a linear isometry. Given a field `𝕜`, normed additive commutative groups `E` and `E'`, both equipped with an inner product space structure over `𝕜`, a linear isometric equivalence `f` from `E` to `E'`, a submodule `K` of `E`, and a point `x` in `E'`, the theorem states that the reflection of `x` in the `Submodule.map` of `K` under `f` is equal to the image under `f` of the reflection of the preimage of `x` under `f` in `K`. More concisely: Given a linear isometric equivalence between normed inner product spaces, the reflection of an image point in the subspace image under the map is equal to the image of the reflection of the preimage in the original subspace.
`reflection_inv` theorem reflection_inv : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K], (reflection K)⁻¹ = reflection K This theorem states that the reflection operation is its own inverse in the context of inner product spaces. Given any type `𝕜` (the field over which the space is defined), any type `E` (the inner product space itself), any submodule `K` of `E`, and assuming that `𝕜` is a ring with characteristic not equal to 2, and `E` is a normed add commutative group with an inner product, the inverse of the reflection operation on `K` is simply the reflection operation on `K` itself. This essentially means that performing the reflection operation twice will lead back to the original state. More concisely: In the context of inner product spaces over a ring with characteristic not equal to 2, the reflection operation on a submodule is its own inverse.
`exists_norm_eq_iInf_of_complete_convex` theorem exists_norm_eq_iInf_of_complete_convex : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {K : Set F}, K.Nonempty → IsComplete K → Convex ℝ K → ∀ (u : F), ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖ The theorem `exists_norm_eq_iInf_of_complete_convex` states that given a point `u` in a real inner product space, and a nonempty, complete, convex subset `K` of the same space, there exists a unique point `v` in `K` that minimizes the Euclidean distance `‖u - v‖` between `u` and `v`. Here, `‖u - v‖` denotes the norm (or magnitude) of the vector difference between `u` and `v`, and `⨅ w, ‖u - ↑w‖` represents the infimum (greatest lower bound) of the distances `‖u - w‖` for all `w` in `K`. The completeness of `K` ensures that any Cauchy sequence in `K` has a limit in `K`, and the convexity of `K` ensures that, for any two points in `K`, all points on the line segment that joins them are also in `K`. More concisely: Given a real inner product space, a nonempty, complete, convex subset, and any point in the space, there exists a unique point in the subset that minimizes the Euclidean distance to that point.
`LinearIsometryEquiv.reflections_generate_dim` theorem LinearIsometryEquiv.reflections_generate_dim : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] [inst_2 : FiniteDimensional ℝ F] (φ : F ≃ₗᵢ[ℝ] F), ∃ l, l.length ≤ FiniteDimensional.finrank ℝ F ∧ φ = (List.map (fun v => reflection (Submodule.span ℝ {v}).orthogonal) l).prod This theorem is a special case of the Cartan–Dieudonné theorem and it states that for any given normed additive commutative group `F` that has an inner product space over the real numbers ℝ and is a finite-dimensional vector space over ℝ, any linear isometry (orthogonal transformation) `φ` from `F` to `F` can be expressed as the product of at most as many reflections as the dimension of `F`. In particular, there exists a list of vectors `l` such that the length of `l` is less than or equal to the rank (dimension) of `F`, and `φ` is equal to the product of reflections across the orthogonal complement of the span of each vector in `l`. More concisely: Any finite-dimensional, normed, additive commutative group with an inner product over the real numbers that is isometrically mapped by an orthogonal transformation can be expressed as a product of at most that many reflections, where the number of reflections equals the dimension of the group.
`orthogonalProjectionFn_mem` theorem orthogonalProjectionFn_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] (v : E), orthogonalProjectionFn K v ∈ K The theorem `orthogonalProjectionFn_mem` states that for any type `𝕜` endowed with the structure of a ring with conjugation, any type `E` that is a normed additive commutative group and an inner product space over `𝕜`, and any submodule `K` of `E` that has an orthogonal projection, the orthogonal projection of any vector `v` from `E` (as computed by the function `orthogonalProjectionFn`) is an element of the submodule `K`. This theorem is a setup for the bundled version of the orthogonal projection and should not be used once the bundled version is defined. More concisely: For any normed additive commutative group and inner product space `E` over a ring with conjugation `𝕜`, and any submodule `K` of `E` with an orthogonal projection, the orthogonal projection of any vector `v` from `E` is an element of `K`.
`reflection_orthogonalComplement_singleton_eq_neg` theorem reflection_orthogonalComplement_singleton_eq_neg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (v : E), (reflection (Submodule.span 𝕜 {v}).orthogonal) v = -v The theorem `reflection_orthogonalComplement_singleton_eq_neg` states that for any vector `v` in an inner product space `E` over a field `𝕜`, the reflection of `v` in the orthogonal complement of the subspace generated by `v` is equal to `-v`. Here, the subspace generated by `v` is the smallest subspace of `E` that contains `v`, and its orthogonal complement is the set of all vectors in `E` that are orthogonal to every vector in the subspace. The reflection operation sends a vector to its mirror image in a subspace. More concisely: For any inner product space vector `v` over field `𝕜`, the reflection of `v` in the orthogonal complement of the subspace generated by `v` equals `-v`.
`Submodule.exists_add_mem_mem_orthogonal` theorem Submodule.exists_add_mem_mem_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [inst_3 : HasOrthogonalProjection K] (v : E), ∃ y ∈ K, ∃ z ∈ K.orthogonal, v = y + z This theorem states that if `K` is a complete submodule of a normed add commutative group `E` over a ring `𝕜` with a well-defined inner product, and `v` is an element of `E`, then there exist elements `y` and `z` in `K` and `K`'s orthogonal complement respectively, such that `v` is the sum of `y` and `z`. In other words, any vector in the inner product space can be decomposed into a component that lies in a given complete subspace and one that is orthogonal to it. More concisely: Given a complete submodule `K` of a normed add commutative group `E` over a ring `𝕜` with a well-defined inner product, any `v` in `E` can be written as the sum of an element in `K` and an element in `K`'s orthogonal complement.
`Submodule.finrank_add_inf_finrank_orthogonal'` theorem Submodule.finrank_add_inf_finrank_orthogonal' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K₁ K₂ : Submodule 𝕜 E} [inst_3 : FiniteDimensional 𝕜 ↥K₂], K₁ ≤ K₂ → ∀ {n : ℕ}, FiniteDimensional.finrank 𝕜 ↥K₁ + n = FiniteDimensional.finrank 𝕜 ↥K₂ → FiniteDimensional.finrank 𝕜 ↥(K₁.orthogonal ⊓ K₂) = n The theorem `Submodule.finrank_add_inf_finrank_orthogonal'` states that for a given finite-dimensional subspace `K₂` of a normed additive commutative group `E` over a division ring `𝕜`, if there exists a subspace `K₁` that is contained within `K₂`, then the sum of the dimensions (defined as their ranks) of `K₁` and the intersection of `K₁`'s orthogonal subspace with `K₂` equals the dimension of `K₂`. In other words, if we denote the dimension of a subspace `A` as `dim(A)`, the theorem can be expressed as: if `K₁` is a subspace of `K₂`, then for a given natural number `n`, if `dim(K₁) + n = dim(K₂)`, it follows that `dim(K₁.orthogonal ∩ K₂) = n`. More concisely: If `K₁` is a subspace of `K₂` in a finite-dimensional normed additive commutative group `E` over a division ring `𝕜`, then the sum of their dimensions equals the dimension of their intersection if and only if the dimension of `K₁` is the difference between the dimension of `K₂` and the dimension of `K₁`'s orthogonal complement in `K₂`.
`Submodule.orthogonal_orthogonal_eq_closure` theorem Submodule.orthogonal_orthogonal_eq_closure : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [inst_3 : CompleteSpace E], K.orthogonal.orthogonal = K.topologicalClosure This theorem states that in a Hilbert space, the orthogonal complement of the orthogonal complement of a given subspace `K` is equal to the topological closure of `K`. However, this is valid only under the assumption that the space is complete. For example, consider the space of sequences of real numbers that converge to zero (`ℕ →₀ ℝ`), with an inner product space structure inherited from `PiLp 2 (fun _ : ℕ ↦ ℝ)`. In this case, if we take `K` as the subspace of sequences whose elements sum to zero, the orthogonal complement of `K` is the zero subspace, and the orthogonal complement of this zero subspace is the whole space, not the topological closure of `K`. More concisely: In a complete Hilbert space, the orthogonal complement of the orthogonal complement of a subspace equals the topological closure of that subspace.
`orthogonalProjection_comp_subtypeL_eq_zero_iff` theorem orthogonalProjection_comp_subtypeL_eq_zero_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection U], (orthogonalProjection U).comp V.subtypeL = 0 ↔ U.IsOrtho V The theorem `orthogonalProjection_comp_subtypeL_eq_zero_iff` states that for any two submodules `U` and `V` of an inner product space over a type `𝕜`, the composition of the orthogonal projection onto `U` and the inclusion of `V` into the larger space is the zero map if and only if `U` and `V` are orthogonal. In mathematical terms, this means that the projection of `V` into `U` gives the zero vector for all vectors in `V` if and only if every vector in `U` is orthogonal to every vector in `V`. More concisely: The orthogonal projection of submodule `V` onto `U` is the zero map if and only if every vector in `U` is orthogonal to every vector in `V`.
`reflection_involutive` theorem reflection_involutive : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [inst_3 : HasOrthogonalProjection K], Function.Involutive ⇑(reflection K) The theorem `reflection_involutive` states that the reflection operation is involutive for any vector space with an inner product. More specifically, for any scalar type `𝕜`, any type `E` forming a normed commutative additive group, any submodule `K` of `E`, and any inner product space formed by `𝕜` and `E`, if `K` has an orthogonal projection, then the reflection operation on `K` is involutive. In mathematical terms, applying the reflection operation twice in this context brings us back to the original element, i.e., for all `x`, `reflection(reflection(x)) = x`. More concisely: If `K` is a submodule of an inner product space `(𝕜, E)` with an orthogonal projection, then the reflection operation on `K` is involutive, i.e., `reflection(reflection(x)) = x` for all `x` in `K`.
`reflection_reflection` theorem reflection_reflection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [inst_3 : HasOrthogonalProjection K] (p : E), (reflection K) ((reflection K) p) = p This theorem states that reflecting a point in a subspace of an inner product space twice results in the original point. More specifically, for any field `𝕜`, type `E` that forms a normed add commutative group and an inner product space, and a submodule `K` of `E` with orthogonal projection, the reflection of a point `p` in `K` followed by another reflection in the same `K` brings us back to `p`. More concisely: For any point `p` in an inner product space `E` with submodule `K` and orthogonal projection, reflecting `p` in `K` twice returns the original point `p`.
`orthogonalProjection_eq_self_iff` theorem orthogonalProjection_eq_self_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] {v : E}, ↑((orthogonalProjection K) v) = v ↔ v ∈ K This theorem states that for any point `v` in an inner product space `E` over a ring `𝕜`, the orthogonal projection of `v` onto a complete subspace `K` of `E` is equal to `v` itself if and only if `v` is an element of the subspace `K`. This theorem allows us to check whether a point lies in a given subspace by comparing the point with its orthogonal projection onto the subspace. It is a fundamental property in the theory of orthogonal projections in inner product spaces. More concisely: The orthogonal projection of a point `v` in an inner product space `E` onto a complete subspace `K` is equal to `v` if and only if `v` is in `K`.
`reflection_trans_reflection` theorem reflection_trans_reflection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [inst_3 : HasOrthogonalProjection K], (reflection K).trans (reflection K) = LinearIsometryEquiv.refl 𝕜 E The theorem `reflection_trans_reflection` states that the operation of reflection in a given inner product space is involutive. Given an inner product space `E` over a field `𝕜` and a submodule `K` of `E` with an orthogonal projection, applying the reflection operation twice (i.e., reflecting twice across `K`) yields the identity map, which leaves all points in the space unchanged. This essentially means that reflecting a point twice gets you back to where you started. More concisely: The reflection operation with respect to an orthogonal projection in an inner product space is self-inverse.
`reflection_map` theorem reflection_map : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_4} {E' : Type u_5} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup E'] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (K : Submodule 𝕜 E) [inst_5 : HasOrthogonalProjection K], reflection (Submodule.map (↑f.toLinearEquiv) K) = f.symm.trans ((reflection K).trans f) This theorem, `reflection_map`, states that for any normed-add-commutative-group (a mathematical structure that satisfies the properties of a normed space and an add-commutative group) E and E' that also have an inner product space structure over some ring-like structure 𝕜, and a linear isometry f from E to E', the reflection in the image of a submodule K of E under the map induced by f is equal to the composition of the reflection in K and the map f. This is achieved by first reflecting in K, then transforming using f, and finally applying the inverse of f. The result holds when K has an orthogonal projection. More concisely: For any normed-add-commutative-group E, E' with inner product space structures over a ring-like structure 𝕜, and a linear isometry f from E to E' between their norms, if K is a submodule of E with an orthogonal projection, then the reflection of a point in K using f is equal to the composition of reflecting in K, applying f, and taking the inverse of f.
`sub_orthogonalProjection_mem_orthogonal` theorem sub_orthogonalProjection_mem_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] (v : E), v - ↑((orthogonalProjection K) v) ∈ K.orthogonal This theorem states that for any vector `v` in an inner product space `E` over a field `𝕜`, the difference between `v` and its orthogonal projection onto a submodule `K` of `E` is an element of the orthogonal complement of `K`. Here the orthogonal complement of `K` is the set of all vectors in `E` that are orthogonal to every vector in `K`. In more mathematical terms, if we denote the orthogonal projection of `v` onto `K` as `proj_K(v)`, the theorem can be written as `v - proj_K(v) ∈ Kᗮ`, where `Kᗮ` denotes the orthogonal complement of `K`. More concisely: The difference between a vector `v` and its orthogonal projection onto a submodule `K` of an inner product space is an element of the orthogonal complement of `K`. In symbols: `v - proj_K(v) ∈ K⊥`.
`Submodule.triorthogonal_eq_orthogonal` theorem Submodule.triorthogonal_eq_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : CompleteSpace E], K.orthogonal.orthogonal.orthogonal = K.orthogonal This theorem states that for any submodule `K` of a normed add commutative group `E` over a ring-like structure `𝕜`, with `E` being a complete space, the orthogonal complement of the orthogonal complement of the orthogonal complement of `K` is equal to the orthogonal complement of `K`. In other words, if you find the orthogonal complement three times, you end up where you started. This is based in the realm of inner product space theory, where orthogonal complements are a key concept. More concisely: For any submodule `K` of a complete, normed, add commutative group `E` over a ring-like structure `𝕜`, the orthogonal complement of `K` equals the orthogonal complement of its orthogonal complement.
`id_eq_sum_orthogonalProjection_self_orthogonalComplement` theorem id_eq_sum_orthogonalProjection_self_orthogonalComplement : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [inst_3 : HasOrthogonalProjection K], ContinuousLinearMap.id 𝕜 E = K.subtypeL.comp (orthogonalProjection K) + K.orthogonal.subtypeL.comp (orthogonalProjection K.orthogonal) This theorem states that in a complete space `E`, over a ring `𝕜` with a real or complex structure, the identity map on `E` can be expressed as the sum of the projection maps onto a complete subspace `K` and its orthogonal complement. Specifically, the identity map is equal to the composition of the inclusion map from `K` to `E` and the orthogonal projection onto `K`, plus the composition of the inclusion map from the orthogonal complement of `K` to `E` and the orthogonal projection onto the orthogonal complement of `K`. More concisely: In a complete space over a real or complex ring, the identity map is equal to the sum of the orthogonal projections onto a complete subspace and its orthogonal complement.
`orthogonalProjection_mem_subspace_orthogonal_precomplement_eq_zero` theorem orthogonalProjection_mem_subspace_orthogonal_precomplement_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K.orthogonal] {v : E}, v ∈ K → (orthogonalProjection K.orthogonal) v = 0 The theorem `orthogonalProjection_mem_subspace_orthogonal_precomplement_eq_zero` states that for any scalar field `𝕜`, any normed commutative group `E`, and any inner product space over `E` and `𝕜`, given a submodule `K` of `E` that has an orthogonal projection and an element `v` of `E` that belongs to `K`, the orthogonal projection of `v` onto the orthogonal complement of `K` is zero. In simpler terms, if you take a vector from a subspace and project it orthogonally onto the subspace's orthogonal complement, you get the zero vector. More concisely: For any inner product space over a scalar field and normed commutative group, if a submodule has an orthogonal projection and an element belongs to it, then the orthogonal projection of that element onto the orthogonal complement is the zero vector.
`orthogonalProjection_tendsto_closure_iSup` theorem orthogonalProjection_tendsto_closure_iSup : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {ι : Type u_4} [inst_4 : SemilatticeSup ι] (U : ι → Submodule 𝕜 E) [inst_5 : ∀ (i : ι), CompleteSpace ↥(U i)], Monotone U → ∀ (x : E), Filter.Tendsto (fun i => ↑((orthogonalProjection (U i)) x)) Filter.atTop (nhds ↑((orthogonalProjection (⨆ i, U i).topologicalClosure) x)) This theorem states that given a sequence of complete subspaces `U i` of a normed add commutative group `E` over a ring `𝕜`, where the sequence is monotone (each `U i` is less than or equal to `U i+1`), and a fixed vector `x` in `E`, the orthogonal projection of `x` onto each `U i` tends to the orthogonal projection of `x` onto the topological closure of the supremum of the `U i` as `i` tends towards infinity. In other words, as we consider larger and larger subspaces `U i`, the projection of `x` onto these subspaces gets closer and closer to the projection of `x` onto the closed subspace that contains all of the `U i`. More concisely: Given a monotone increasing sequence of complete subspaces of a normed add commutative group, and a fixed vector, the orthogonal projection of the vector onto each subspace converges to the orthogonal projection onto the closure of their supremum as the sequence index tends to infinity.
`reflection_bot` theorem reflection_bot : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E], reflection ⊥ = LinearIsometryEquiv.neg 𝕜 This theorem states that reflection through the trivial subspace constituted only by the zero element is equivalent to the negation operation in a normed space `E`, with respect to a semiring `𝕜`. More specifically, for any semiring `𝕜` and any Normed Additive Commutative Group `E` that also forms an Inner Product Space over `𝕜`, the operation of reflection through the trivial subspace `{0}` is the same as applying the negation operation defined by `LinearIsometryEquiv.neg` in `E`. This is a statement about the isometry between two mathematical operations in the context of linear algebra and analysis. More concisely: In a Normed Additive Commutative Group `E` over a semiring `𝕜` that is also an Inner Product Space, reflection through the trivial subspace `{0}` is equivalent to negation via `LinearIsometryEquiv.neg`.
`norm_eq_iInf_iff_real_inner_eq_zero` theorem norm_eq_iInf_iff_real_inner_eq_zero : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (K : Submodule ℝ F) {u v : F}, v ∈ K → (‖u - v‖ = ⨅ w, ‖u - ↑w‖ ↔ ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0) This theorem provides a characterization of the point that minimizes the distance to a given point in a subspace of a real inner product space. Given a point `u` in a real inner product space and a nonempty subspace `K`, the theorem states that a point `v` in `K` minimizes the distance `‖u - v‖` over all points in `K` if and only if `⟪u - v, w⟫ = 0` for all `w` in `K`. In other words, `v` is a minimizer if and only if the vector `u - v` is orthogonal to every vector in the subspace `K`. Note that this theorem is applicable to any `RCLike` field, as indicated by the theorem `norm_eq_iInf_iff_inner_eq_zero`. More concisely: A point in a subspace of a real inner product space minimizes the distance to a given point if and only if the difference between the given point and that point in the subspace is orthogonal to every vector in the subspace.
`reflection_mul_reflection` theorem reflection_mul_reflection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [inst_3 : HasOrthogonalProjection K], reflection K * reflection K = 1 The theorem 'reflection_mul_reflection' states that the operation of reflection, when applied twice, is equivalent to the identity operation in the context of an inner product space over a ring-like structure. More specifically, for any submodule of a normed additive commutative group forming an inner product space over a type 𝕜 (which obeys ring-like behavior), the composition of reflection operations (represented as multiplication of reflections) is equal to the identity operation (represented as 1). This establishes reflection as an involutive operation. More concisely: In an inner product space over a ring-like structure, the composition of two reflection operations is equal to the identity.

LeanAide GPT-4 documentation

Module: Mathlib.Analysis.InnerProductSpace.Projection

orthogonalProjection_orthogonalProjection_of_le

eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero

Submodule.sup_orthogonal_inf_of_completeSpace

inner_orthogonalProjection_left_eq_right

orthogonalProjection_minimal

theorem orthogonalProjection_minimal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection U] (y : E), ‖y - ↑((orthogonalProjection U) y)‖ = ⨅ x, ‖y - ↑x‖

orthogonalProjection_add_orthogonalProjection_orthogonal

reflection_symm

theorem reflection_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K], (reflection K).symm = reflection K

Submodule.orthogonal_orthogonal

theorem Submodule.orthogonal_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [inst_3 : HasOrthogonalProjection K], K.orthogonal.orthogonal = K

norm_sq_eq_add_norm_sq_projection

orthogonalProjection_singleton

theorem orthogonalProjection_singleton : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {v : E} (w : E), ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = (⟪v, w⟫_𝕜 / ↑(‖v‖ ^ 2)) • v

OrthogonalFamily.projection_directSum_coeAddHom

Dense.eq_of_sub_mem_orthogonal

theorem Dense.eq_of_sub_mem_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} {x y : E}, Dense ↑K → x - y ∈ K.orthogonal → x = y

LinearIsometryEquiv.reflections_generate_dim_aux

reflection_apply

theorem reflection_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] (p : E), (reflection K) p = 2 • ↑((orthogonalProjection K) p) - p

reflection_mem_subspace_orthogonal_precomplement_eq_neg

orthogonalProjection_bot

theorem orthogonalProjection_bot : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E], orthogonalProjection ⊥ = 0

Submodule.topologicalClosure_eq_top_iff

theorem Submodule.topologicalClosure_eq_top_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : CompleteSpace E], K.topologicalClosure = ⊤ ↔ K.orthogonal = ⊥

LinearIsometryEquiv.reflections_generate

theorem LinearIsometryEquiv.reflections_generate : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] [inst_2 : FiniteDimensional ℝ F], Subgroup.closure (Set.range fun v => reflection (Submodule.span ℝ {v}).orthogonal) = ⊤

OrthogonalFamily.isInternal_iff

reflection_mem_subspace_orthogonalComplement_eq_neg

eq_orthogonalProjection_of_mem_orthogonal'

finrank_orthogonal_span_singleton

orthogonalProjection_inner_eq_zero

eq_orthogonalProjection_of_mem_of_inner_eq_zero

maximal_orthonormal_iff_basis_of_finiteDimensional

Submodule.isCompl_orthogonal_of_completeSpace

theorem Submodule.isCompl_orthogonal_of_completeSpace : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K], IsCompl K K.orthogonal

orthogonalProjection_unit_singleton

theorem orthogonalProjection_unit_singleton : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {v : E}, ‖v‖ = 1 → ∀ (w : E), ↑((orthogonalProjection (Submodule.span 𝕜 {v})) w) = ⟪v, w⟫_𝕜 • v

Submodule.finrank_add_inf_finrank_orthogonal

orthogonalProjection_orthogonalComplement_singleton_eq_zero

theorem orthogonalProjection_orthogonalComplement_singleton_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (v : E), (orthogonalProjection (Submodule.span 𝕜 {v}).orthogonal) v = 0

Submodule.finrank_add_finrank_orthogonal

exists_norm_eq_iInf_of_complete_subspace

theorem exists_norm_eq_iInf_of_complete_subspace : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E), IsComplete ↑K → ∀ (u : E), ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖

norm_eq_iInf_iff_real_inner_le_zero

theorem norm_eq_iInf_iff_real_inner_le_zero : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {K : Set F}, Convex ℝ K → ∀ {u v : F}, v ∈ K → (‖u - v‖ = ⨅ w, ‖u - ↑w‖ ↔ ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0)

Submodule.finrank_add_finrank_orthogonal'

maximal_orthonormal_iff_orthogonalComplement_eq_bot

reflection_eq_self_iff

theorem reflection_eq_self_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] (x : E), (reflection K) x = x ↔ x ∈ K

orthogonalProjection_tendsto_self

orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero

OrthogonalFamily.isInternal_iff_of_isComplete

orthogonalProjection_isSymmetric

theorem orthogonalProjection_isSymmetric : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [inst_3 : HasOrthogonalProjection K], (K.subtypeL.comp (orthogonalProjection K)).IsSymmetric

norm_eq_iInf_iff_inner_eq_zero

theorem norm_eq_iInf_iff_inner_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) {u v : E}, v ∈ K → (‖u - v‖ = ⨅ w, ‖u - ↑w‖ ↔ ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0)

OrthogonalFamily.sum_projection_of_mem_iSup

orthogonalProjectionFn_inner_eq_zero

Submodule.IsOrtho.orthogonalProjection_comp_subtypeL

orthogonalProjection_mem_subspace_eq_self

theorem orthogonalProjection_mem_subspace_eq_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] (v : ↥K), (orthogonalProjection K) ↑v = v

orthogonalProjection_norm_le

theorem orthogonalProjection_norm_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [inst_3 : HasOrthogonalProjection K], ‖orthogonalProjection K‖ ≤ 1

eq_orthogonalProjection_of_mem_orthogonal

eq_orthogonalProjection_of_eq_submodule

Submodule.sup_orthogonal_of_completeSpace

theorem Submodule.sup_orthogonal_of_completeSpace : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K], K ⊔ K.orthogonal = ⊤

reflection_map_apply

reflection_inv

theorem reflection_inv : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K], (reflection K)⁻¹ = reflection K

exists_norm_eq_iInf_of_complete_convex

theorem exists_norm_eq_iInf_of_complete_convex : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {K : Set F}, K.Nonempty → IsComplete K → Convex ℝ K → ∀ (u : F), ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖

LinearIsometryEquiv.reflections_generate_dim

orthogonalProjectionFn_mem

theorem orthogonalProjectionFn_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [inst_3 : HasOrthogonalProjection K] (v : E), orthogonalProjectionFn K v ∈ K

reflection_orthogonalComplement_singleton_eq_neg

theorem reflection_orthogonalComplement_singleton_eq_neg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (v : E), (reflection (Submodule.span 𝕜 {v}).orthogonal) v = -v

`orthogonalProjection_orthogonalProjection_of_le`

`eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero`

`Submodule.sup_orthogonal_inf_of_completeSpace`

`inner_orthogonalProjection_left_eq_right`

`orthogonalProjection_minimal`

`orthogonalProjection_add_orthogonalProjection_orthogonal`

`reflection_symm`

`Submodule.orthogonal_orthogonal`

`norm_sq_eq_add_norm_sq_projection`

`orthogonalProjection_singleton`

`OrthogonalFamily.projection_directSum_coeAddHom`

`Dense.eq_of_sub_mem_orthogonal`

`LinearIsometryEquiv.reflections_generate_dim_aux`

`reflection_apply`

`reflection_mem_subspace_orthogonal_precomplement_eq_neg`

`orthogonalProjection_bot`

`Submodule.topologicalClosure_eq_top_iff`

`LinearIsometryEquiv.reflections_generate`

`OrthogonalFamily.isInternal_iff`

`reflection_mem_subspace_orthogonalComplement_eq_neg`

`eq_orthogonalProjection_of_mem_orthogonal'`

`finrank_orthogonal_span_singleton`

`orthogonalProjection_inner_eq_zero`

`eq_orthogonalProjection_of_mem_of_inner_eq_zero`

`maximal_orthonormal_iff_basis_of_finiteDimensional`

`Submodule.isCompl_orthogonal_of_completeSpace`

`orthogonalProjection_unit_singleton`

`Submodule.finrank_add_inf_finrank_orthogonal`

`orthogonalProjection_orthogonalComplement_singleton_eq_zero`

`Submodule.finrank_add_finrank_orthogonal`

`exists_norm_eq_iInf_of_complete_subspace`

`norm_eq_iInf_iff_real_inner_le_zero`

`Submodule.finrank_add_finrank_orthogonal'`

`maximal_orthonormal_iff_orthogonalComplement_eq_bot`

`reflection_eq_self_iff`

`orthogonalProjection_tendsto_self`

`orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero`

`OrthogonalFamily.isInternal_iff_of_isComplete`

`orthogonalProjection_isSymmetric`

`norm_eq_iInf_iff_inner_eq_zero`

`OrthogonalFamily.sum_projection_of_mem_iSup`

`orthogonalProjectionFn_inner_eq_zero`

`Submodule.IsOrtho.orthogonalProjection_comp_subtypeL`

`orthogonalProjection_mem_subspace_eq_self`

`orthogonalProjection_norm_le`

`eq_orthogonalProjection_of_mem_orthogonal`

`eq_orthogonalProjection_of_eq_submodule`

`Submodule.sup_orthogonal_of_completeSpace`

`reflection_map_apply`

`reflection_inv`

`exists_norm_eq_iInf_of_complete_convex`

`LinearIsometryEquiv.reflections_generate_dim`

`orthogonalProjectionFn_mem`

`reflection_orthogonalComplement_singleton_eq_neg`

`Submodule.exists_add_mem_mem_orthogonal`

`Submodule.finrank_add_inf_finrank_orthogonal'`

`Submodule.orthogonal_orthogonal_eq_closure`

`orthogonalProjection_comp_subtypeL_eq_zero_iff`

`reflection_involutive`

`reflection_reflection`

`orthogonalProjection_eq_self_iff`

`reflection_trans_reflection`

`reflection_map`

`sub_orthogonalProjection_mem_orthogonal`

`Submodule.triorthogonal_eq_orthogonal`

`id_eq_sum_orthogonalProjection_self_orthogonalComplement`

`orthogonalProjection_mem_subspace_orthogonal_precomplement_eq_zero`

`orthogonalProjection_tendsto_closure_iSup`

`reflection_bot`

`norm_eq_iInf_iff_real_inner_eq_zero`

`reflection_mul_reflection`