MinimalCyclicExpectation.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Explicit retractions through a minimal cyclic space

The compression proof of type-I injectivity gives a specific contractive retraction. Its coefficients on the minimal cyclic space agree with the original ambient operator. These identities allow the trace-preserving finite-stage construction to retain the original vector state.

theorem OAI.KadisonKastler.typeICyclicEquiv_symm_norm line 24
def OAI.KadisonKastler.minimalCyclicRetraction line 32
Source documentation
The concrete ambient-to-algebra retraction supplied by a minimal projection.
```
def minimalCyclicRetraction : (H →L[ℂ] H) →L[ℂ] Algebra N := by
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.minimalCyclicRetraction_compression line 41
theorem OAI.KadisonKastler.minimalCyclicRetraction_norm line 49
theorem OAI.KadisonKastler.minimalCyclicRetraction_fixed line 58
theorem OAI.KadisonKastler.minimalCyclicRetraction_coefficient line 66
Source documentation
Compression preserves every coefficient with both vectors in the cyclic space.
```
theorem minimalCyclicRetraction_coefficient (T : H →L[ℂ] H)
    (x y : typeICyclicSpace N ξ) :
    inner ℂ y.val ((minimalCyclicRetraction N hN p hp ξ hξ hpξ T).val x.val) =
      inner ℂ y.val (T x.val) := by
…
```
Mentions: OAI.KadisonKastler.typeICyclicSpace, OAI.KadisonKastler.minimalCyclicRetraction
theorem OAI.KadisonKastler.minimalCyclicRetraction_mul_left line 78
Source documentation
The compression retraction respects left multiplication from its range.
```
theorem minimalCyclicRetraction_mul_left (a : Algebra N) (T : H →L[ℂ] H) :
    minimalCyclicRetraction N hN p hp ξ hξ hpξ (a.val * T) =
      a * minimalCyclicRetraction N hN p hp ξ hξ hpξ T := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.minimalCyclicRetraction