conj_starProjection — Mathlib

English

Let U be a subspace with an orthogonal projection star-projection; if T is positive, then U.starProjection ∘ T ∘ U.starProjection is positive.

Русский

Пусть U — подпространство с ортогональной проекцией, тогда U.starProjection ∘ T ∘ U.starProjection положителен при T положительном.

LaTeX

$$$ (U^{\star} \circ T \circ U^{\star}).IsPositive $$$

Lean4

theorem conj_starProjection (U : Submodule 𝕜 E) {T : E →L[𝕜] E} (hT : T.IsPositive) [U.HasOrthogonalProjection] :
    (U.starProjection ∘L T ∘L U.starProjection).IsPositive :=
  by
  have := hT.conj_adjoint (U.starProjection)
  rwa [(isSelfAdjoint_starProjection U).adjoint_eq] at this

Похожие утверждения