HomPolarBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The polar estimate for a bounded homomorphism, proved with approximate polar factors in the source algebra.

theorem OAI.KadisonSimilarity.hom_adjoint_polar_bound line 17

Source documentation

Approximate polar factorization transfers to an adjoint-vector estimate.

theorem hom_adjoint_polar_bound (π : BoundedUnitalHom A H) {M : ℝ} (hM : 0 ≤ M)
    (hπ : ∀ a, ‖π.1 a‖ ≤ M * ‖a‖) (x h : A) (hh : 0 ≤ h)
    (hsq : x * star x = h * h) (ξ : H) :
    ‖(π.1 x).adjoint ξ‖ ≤ M * ‖(π.1 h).adjoint ξ‖ := by
…

Mentions: OAI.KadisonSimilarity.BoundedUnitalHom

theorem OAI.KadisonSimilarity.hom_adjoint_sqrt_bound line 60
Source documentation
The positive square root of xx* is enough; a polar partial isometry or an extension of the homomorphism to a bidual is unnecessary.
```
theorem hom_adjoint_sqrt_bound (π : BoundedUnitalHom A H) {M : ℝ} (hM : 0 ≤ M)
    (hπ : ∀ a, ‖π.1 a‖ ≤ M * ‖a‖) (x : A) (ξ : H) :
    ‖(π.1 x).adjoint ξ‖ ≤ M * ‖(π.1 (CFC.sqrt (x * star x))).adjoint ξ‖ := by
…
```
Mentions: OAI.KadisonSimilarity.BoundedUnitalHom