HilbertContractionFactor.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Contractive factorization through a Hilbert-space operator

This is the range-extension step used for contractive block completions in the finite-nest distance argument. The factor is constructed on the closed range and extended by zero on its orthogonal complement.

def OAI.KadisonKastler.operatorClosedRangeMap line 23
Source documentation
The same operator, with target restricted to the closure of its range.
```
def operatorClosedRangeMap (S : E →L[ℂ] F) :
    E →L[ℂ] S.toLinearMap.range.topologicalClosure :=
…
```
theorem OAI.KadisonKastler.operatorClosedRangeMap_dense line 28
theorem OAI.KadisonKastler.exists_contraction_factor line 37
Source documentation
Norm domination gives a contractive factor on the entire middle Hilbert space, including when the original operator has nonclosed range.
```
theorem exists_contraction_factor (S : E →L[ℂ] F) (T : E →L[ℂ] G)
    (h : ∀ x, ‖T x‖ ≤ ‖S x‖) :
    ∃ C : F →L[ℂ] G, ‖C‖ ≤ 1 ∧ C.comp S = T := by
…
```