UCPDescent.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Descending an amplified conjugacy through a UCP retraction

These are the operator-space estimates used when a character average or an auxiliary tensor-factor average returns an amplified map to the base.

def OAI.KadisonKastler.completelyPositiveComp line 25
Source documentation
Composition of completely positive linear maps.
```
def completelyPositiveComp (E : B →CP C) (F : A →CP B) : A →CP C where
…
```

def OAI.KadisonKastler.completelyPositive_of_embedding line 32

Source documentation

Positivity at all matrix levels is reflected by a faithful embedding.

def completelyPositive_of_embedding (j : B →⋆ₐ[ℂ] C) (hj : Function.Injective j)
    (φ : A →CP C) (F : A →ₗ[ℂ] B) (hF : ∀ a, j (F a) = φ a) : A →CP B where
…

theorem OAI.KadisonKastler.completelyBoundedBy_comp_contraction line 49

Source documentation

Complete contraction on the outside preserves a complete bound.

theorem completelyBoundedBy_comp_contraction (E : B →ₗ[ℂ] C) (F : A →ₗ[ℂ] B)
    (hE : CompletelyBoundedBy E 1) {c : ℝ} (hF : CompletelyBoundedBy F c) :
    CompletelyBoundedBy (E.comp F) c := by
…

Mentions: OAI.KadisonKastler.CompletelyBoundedBy

theorem OAI.KadisonKastler.completelyBoundedBy_comp_completeIsometry line 61
Source documentation
Restriction along a complete isometry preserves the same complete bound.
```
theorem completelyBoundedBy_comp_completeIsometry (F : B →ₗ[ℂ] C)
    (j : A →ₗ[ℂ] B) {c : ℝ} (hF : CompletelyBoundedBy F c)
    (hj : CompletelyIsometric j) : CompletelyBoundedBy (F.comp j) c := by
…
```
Mentions: OAI.KadisonKastler.CompletelyBoundedBy, OAI.KadisonKastler.CompletelyIsometric

theorem OAI.KadisonKastler.retracted_conjugation_complete_bound line 72

Source documentation

A UCP retraction of a faithful ambient embedding turns a nearby inner conjugation into a map within twice the unitary displacement.

theorem retracted_conjugation_complete_bound
    (j : A →⋆ₐ[ℂ] B) (hj : Function.Injective j)
    (E : B →CP A) (hE : E 1 = 1) (hfix : ∀ a, E (j a) = a)
    (u : unitary B) :
    CompletelyBoundedBy
      (E.toLinearMap.comp ((unitaryConjugationLinear u).comp j.toAlgHom.toLinearMap) -
        LinearMap.id) (2 * ‖(u : B) - 1‖) := by
…

Mentions: OAI.KadisonKastler.CompletelyBoundedBy, OAI.KadisonKastler.unitaryConjugationLinear

theorem OAI.KadisonKastler.concrete_unitary_of_retracted_conjugation line 123

Source documentation

Descend an upstairs unitary through an actual UCP retraction. Range membership and the original metric gap suffice for the final conjugacy.

theorem concrete_unitary_of_retracted_conjugation
    (hCorrection : PublishedMultiplicationCorrection M)
    (hCommutant : PublishedBlockCommutantApproximation (Algebra M) H)
    (j : (H →L[ℂ] H) →⋆ₐ[ℂ] (K →L[ℂ] K)) (hj : Function.Injective j)
    (E : (K →L[ℂ] K) →CP (H →L[ℂ] H)) (hE : E 1 = 1)
    (hfix : ∀ x, E (j x) = x)
    (z : unitary (K →L[ℂ] K))
    (hmem : ∀ x : Algebra M,
      E ((z : K →L[ℂ] K) * j x * star (z : K →L[ℂ] K)) ∈ N)
    {g : ℝ} (hgap : kkDistance M N < g)
    (hsmall : 2 * ‖(z : K →L[ℂ] K) - 1‖ < 1 / 1000)
    (hge : g + 2 * ‖(z : K →L[ℂ] K) - 1‖ < 1) :
…

Mentions: OAI.KadisonKastler.PublishedMultiplicationCorrection, OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.kkDistance