SimilarityMetric.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The quantitative positive metric from an invertible star intertwiner

This is the final geometric step of Paulsen's theorem. The intertwiner may map to a different Hilbert space. Its positive metric on the original space and its positive square root yield the actual similarity unit, with exactly the product of the forward and inverse operator norms.

theorem OAI.KadisonSimilarity.intertwiner_metric_identity line 25

Source documentation

The square of any bounded star intertwiner is a metric for the original homomorphism, without an invertibility assumption.

theorem intertwiner_metric_identity (π : BoundedUnitalHom A H)
    (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) (W : H →L[ℂ] K)
    (hW : ∀ a, W.comp (π.1 a) = (σ a).comp W) (a : A) :
    (W.adjoint.comp W).comp (π.1 (star a)) =
      (π.1 a).adjoint.comp (W.adjoint.comp W) := by
…

Mentions: OAI.KadisonSimilarity.BoundedUnitalHom

def OAI.KadisonSimilarity.intertwinerMetricUnit line 42

Source documentation

The metric of a bounded linear isomorphism has an explicit inverse.

def intertwinerMetricUnit (W : H →L[ℂ] K) (L : K →L[ℂ] H)
    (hLW : L.comp W = 1) (hWL : W.comp L = 1) : (H →L[ℂ] H)ˣ where
…

theorem OAI.KadisonSimilarity.intertwinerMetric_nonneg line 56
Source documentation
The metric is positive because it is an adjoint square.
```
theorem intertwinerMetric_nonneg (W : H →L[ℂ] K) : 0 ≤ W.adjoint.comp W := by
…
```

theorem OAI.KadisonSimilarity.exists_positive_sqrt_metric_unit line 62

Source documentation

A square root of the positive metric preserves both operator norms needed for the sharp similarity estimate.

theorem exists_positive_sqrt_metric_unit (W : H →L[ℂ] K) (L : K →L[ℂ] H)
    (hLW : L.comp W = 1) (hWL : W.comp L = 1) :
    ∃ S : (H →L[ℂ] H)ˣ,
      0 ≤ (S : H →L[ℂ] H) ∧
      star (S : H →L[ℂ] H) * (S : H →L[ℂ] H) = W.adjoint.comp W ∧
      ‖(S : H →L[ℂ] H)‖ = ‖W‖ ∧ ‖(↑S⁻¹ : H →L[ℂ] H)‖ = ‖L‖ := by
…

theorem OAI.KadisonSimilarity.exists_sqrt_metric_unit line 107

Source documentation

The positive metric construction gives an invertible star intertwiner.

theorem exists_sqrt_metric_unit (W : H →L[ℂ] K) (L : K →L[ℂ] H)
    (hLW : L.comp W = 1) (hWL : W.comp L = 1) :
    ∃ S : (H →L[ℂ] H)ˣ,
      star (S : H →L[ℂ] H) * (S : H →L[ℂ] H) = W.adjoint.comp W ∧
      ‖(S : H →L[ℂ] H)‖ = ‖W‖ ∧ ‖(↑S⁻¹ : H →L[ℂ] H)‖ = ‖L‖ := by
…

theorem OAI.KadisonSimilarity.quantitative_similarity_of_intertwiner line 117

Source documentation

An invertible bounded intertwiner into a star representation supplies similarity on the original space with its exact condition-number bound.

theorem quantitative_similarity_of_intertwiner (π : BoundedUnitalHom A H)
    (σ : A →⋆ₐ[ℂ] (K →L[ℂ] K)) (W : H →L[ℂ] K) (L : K →L[ℂ] H)
    (hLW : L.comp W = 1) (hWL : W.comp L = 1)
    (hW : ∀ a, W.comp (π.1 a) = (σ a).comp W) :
    ∃ S : (H →L[ℂ] H)ˣ,
      ‖(S : H →L[ℂ] H)‖ * ‖(↑S⁻¹ : H →L[ℂ] H)‖ ≤ ‖W‖ * ‖L‖ ∧
      ∀ a, (S : H →L[ℂ] H) * π.1 (star a) * (↑S⁻¹ : H →L[ℂ] H) =
        star ((S : H →L[ℂ] H) * π.1 a * (↑S⁻¹ : H →L[ℂ] H)) := by
…

Mentions: OAI.KadisonSimilarity.BoundedUnitalHom