AveragedRangeDescent.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Descent when only the averaged conjugates lie in the embedded range

The averaging map acts on the upper ambient operator algebra. Its range on other inputs need not lie in the embedded lower algebra. The map below uses the inverse of a faithful embedding only on the averaged conjugates of the source algebra, which is exactly the range condition in §8.

def OAI.KadisonKastler.linearDescendRange line 25

Source documentation

Restrict a linear map to the range of an injection and invert there.

def linearDescendRange (j : B →ₗ[ℂ] C) (hj : Function.Injective j)
    (F : A →ₗ[ℂ] C) (hF : ∀ a, F a ∈ j.range) : A →ₗ[ℂ] B :=
…

theorem OAI.KadisonKastler.linearDescendRange_spec line 29

theorem OAI.KadisonKastler.averaged_conjugation_complete_bound line 44

Source documentation

An upper UCP average fixes the embedding and retains the usual twice-displacement complete bound, without a global range assumption.

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

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

def OAI.KadisonKastler.averagedUpperMap line 97
Source documentation
The averaged upper map, still valued in all upper ambient operators.
```
def averagedUpperMap : Algebra M →CP (K →L[ℂ] K) :=
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.averagedUpperMap_apply line 102
theorem OAI.KadisonKastler.averagedUpperMap_mem_range line 111
def OAI.KadisonKastler.averagedRangeLinear line 117
Source documentation
The lower linear map is defined only by inversion on the embedded range.
```
def averagedRangeLinear : Algebra M →ₗ[ℂ] (H →L[ℂ] H) :=
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.averagedRangeLinear_spec line 121
theorem OAI.KadisonKastler.averagedRangeLinear_mem line 126
def OAI.KadisonKastler.averagedRangeMap line 134
Source documentation
Complete positivity is reflected through the faithful ambient embedding.
```
def averagedRangeMap : Algebra M →CP (H →L[ℂ] H) :=
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.averagedRangeMap_one line 138
theorem OAI.KadisonKastler.averagedRangeMap_complete_bound line 149
theorem OAI.KadisonKastler.concrete_unitary_of_averaged_range line 177