ContractionPolarFactor.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Only the factor and its adjoint identity are needed for finite coefficient duality. There is no closed-range or finite-dimensional hypothesis here.

theorem OAI.KadisonKastler.contraction_adjoint_self_of_norm_eq line 21
theorem OAI.KadisonKastler.operator_modulus_norm line 34
Source documentation
The positive modulus has the same vector norms as the original operator.
```
theorem operator_modulus_norm (T : E →L[ℂ] F) (x : E) :
    ‖CFC.sqrt (T.adjoint.comp T) x‖ = ‖T x‖ := by
…
```
theorem OAI.KadisonKastler.exists_contractive_polar_factor line 52
Source documentation
A contractive polar factor suffices for the exact trace-norm duality. The second identity records that its adjoint recovers the positive modulus.
```
theorem exists_contractive_polar_factor (T : E →L[ℂ] F) :
    ∃ U : E →L[ℂ] F, ‖U‖ ≤ 1 ∧
      U.comp (CFC.sqrt (T.adjoint.comp T)) = T ∧
      U.adjoint.comp T = CFC.sqrt (T.adjoint.comp T) := by
…
```