Documentation

Monlib.LinearAlgebra.IsProj'

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.

source
def isProj' {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {U : Submodule R E} {p : E →ₗ[R] E} (hp : LinearMap.IsProj U p) :
E →ₗ[R] ↥U

linear_map.is_proj but as a linear map from E to ↥U

Equations
  • isProj' hp = { toFun := fun (x : E) => ⟨p x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
Instances For
    source
    theorem isProj'_apply {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {U : Submodule R E} {p : E →ₗ[R] E} (hp : LinearMap.IsProj U p) (x : E) :
    ↑((isProj' hp) x) = p x
    source
    theorem isProj'_eq {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] {U : Submodule R E} {p : E →ₗ[R] E} (hp : LinearMap.IsProj U p) (x : ↥U) :
    (isProj' hp) ↑x = x
    source
    theorem orthogonalProjection_eq_linear_proj' {E : Type u_2} {𝕜 : Type u_1} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [HasOrthogonalProjection K] :
    ↑(orthogonalProjection K) = K.linearProjOfIsCompl Kᗮ ⋯
    source
    theorem orthogonalProjection_eq_linear_proj'' {E : Type u_2} {𝕜 : Type u_1} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [HasOrthogonalProjection K] (x : E) :
    (orthogonalProjection K) x = (K.linearProjOfIsCompl Kᗮ ⋯) x
    source
    noncomputable def orthogonalProjection' {E : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [HasOrthogonalProjection U] :
    E →L[𝕜] E
    Equations
    Instances For
      source
      theorem orthogonalProjection'_apply {E : Type u_2} {𝕜 : Type u_1} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [HasOrthogonalProjection U] (x : E) :
      (orthogonalProjection' U) x = ↑((orthogonalProjection U) x)
      source
      @[simp]
      theorem ContinuousLinearMap.range_toLinearMap {E : Type u_3} {𝕜 : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {p : E →L[𝕜] F} :
      LinearMap.range ↑p = LinearMap.range p
      source
      @[simp]
      theorem orthogonalProjection.range {E : Type u_2} {𝕜 : Type u_1} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [HasOrthogonalProjection U] :
      LinearMap.range (orthogonalProjection' U) = U
      source
      @[simp]
      theorem orthogonalProjection'_eq {E : Type u_2} {𝕜 : Type u_1} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) [HasOrthogonalProjection U] :
      orthogonalProjection' U = U.subtypeL.comp (orthogonalProjection U)
      source
      theorem orthogonal_projection'_eq_linear_proj {E : Type u_2} {𝕜 : Type u_1} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [HasOrthogonalProjection K] :
      ↑(K.subtypeL.comp (orthogonalProjection K)) = K.subtype ∘ₗ K.linearProjOfIsCompl Kᗮ ⋯
      source
      theorem orthogonalProjection'_eq_linear_proj' {E : Type u_2} {𝕜 : Type u_1} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {K : Submodule 𝕜 E} [HasOrthogonalProjection K] (x : E) :
      ↑(orthogonalProjection' K) x = (K.subtype ∘ₗ K.linearProjOfIsCompl Kᗮ ⋯) x