is_proj' #
This file contains the definition of linear_map.is_proj' and lemmas relating to it, which is essentially linear_map.is_proj but as a linear map from E to ↥U.
def
is_proj'
{R : Type u_1}
{E : Type u_2}
[ring R]
[add_comm_group E]
[module R E]
{U : submodule R E}
{p : E →ₗ[R] E}
(hp : linear_map.is_proj U p) :
linear_map.is_proj but as a linear map from E to ↥U
theorem
orthogonal_projection_eq_linear_proj'
{E : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{K : submodule 𝕜 E}
[complete_space ↥K] :
theorem
orthogonal_projection_eq_linear_proj''
{E : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{K : submodule 𝕜 E}
[complete_space ↥K]
(x : E) :
noncomputable
def
orthogonal_projection'
{E : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
(U : submodule 𝕜 E)
[complete_space ↥U] :
Equations
theorem
orthogonal_projection'_apply
{E : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
(U : submodule 𝕜 E)
[complete_space ↥U]
(x : E) :
⇑(orthogonal_projection' U) x = ↑(⇑(orthogonal_projection U) x)
@[simp]
theorem
continuous_linear_map.range_to_linear_map
{E : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{p : E →L[𝕜] E} :
@[simp]
theorem
orthogonal_projection.range
{E : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
(U : submodule 𝕜 E)
[complete_space ↥U] :
@[simp]
theorem
orthogonal_projection'_eq
{E : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
(U : submodule 𝕜 E)
[complete_space ↥U] :
theorem
orthogonal_projection'_eq_linear_proj
{E : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{K : submodule 𝕜 E}
[complete_space ↥K] :
theorem
orthogonal_projection'_eq_linear_proj'
{E : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
{K : submodule 𝕜 E}
[complete_space ↥K]
(x : E) :