ApproximateOneStep.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite specializations of the one-step-inner calculus in Kirchberg--Rørdam, Infinite non-simple C*-algebras: absorbing the Cuntz algebra O_infinity, Adv. Math. 167 (2002), Lemmas 7.19--7.20 (author preprint pp. 58--59).

These lemmas only perform the finite coefficient and closure steps. They do not assert that a nuclear algebra supplies the abelian-range maps used in that paper.

def OAI.WeakPureInfiniteness.ApproximatelyOneStepInner line 21
Source documentation
Point-norm approximation by a single inner compression.
```
def ApproximatelyOneStepInner (T : A → A) : Prop :=
…
```
def OAI.WeakPureInfiniteness.coefficientEnlargement line 26
Source documentation
Finite coefficient enlargement of a map, as in KR02, equation (7.10).
```
def coefficientEnlargement {ι : Type*} [Fintype ι]
    (T : A → A) (a c : ι → A) (b : A) : A :=
…
```
lemma OAI.WeakPureInfiniteness.coefficientEnlargement_inner line 30
lemma OAI.WeakPureInfiniteness.coefficientEnlargement_error_le line 38
lemma OAI.WeakPureInfiniteness.ApproximatelyOneStepInner.coefficientEnlargement line 76
Source documentation
The finite coefficient step of KR02 Lemma 7.20. No norm bound on the approximating compression is asserted.
```
lemma ApproximatelyOneStepInner.coefficientEnlargement
    {T : A → A} (hT : ApproximatelyOneStepInner T)
    {ι : Type*} [Fintype ι] (a c : ι → A) :
    ApproximatelyOneStepInner (coefficientEnlargement T a c) := by
…
```
Mentions: OAI.WeakPureInfiniteness.ApproximatelyOneStepInner
lemma OAI.WeakPureInfiniteness.ApproximatelyOneStepInner.of_pointNorm_approximation line 105