DoubledCorner.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

The particular approximately inner map to which KR02 Theorem 7.21 is applied in the absorption argument: copy the upper-left corner into both diagonal corners. Its approximately inner character is proved here by two explicit coefficients and a nonunital approximate unit.

lemma OAI.WeakPureInfiniteness.completelyPositive_of_pointwise_limit line 25

Source documentation

A point-norm limit of completely positive maps is completely positive.

lemma completelyPositive_of_pointwise_limit
    {ι : Type*} {l : Filter ι} [l.NeBot]
    {B C : Type*} [NonUnitalCStarAlgebra B] [NonUnitalCStarAlgebra C]
    [PartialOrder B] [StarOrderedRing B] [PartialOrder C] [StarOrderedRing C]
    (S : ι → B →L[ℂ] C) (T : B →L[ℂ] C)
    (hS : ∀ i, CompletelyPositive (S i))
    (hlim : ∀ b, Tendsto (fun i => S i b) l (𝓝 (T b))) :
    CompletelyPositive T := by
…

Mentions: OAI.WeakPureInfiniteness.CompletelyPositive

def OAI.WeakPureInfiniteness.ApproximatelyInner line 42
Source documentation
Approximation by finite sums of inner compressions (KR02 Definition 7.1).
```
def ApproximatelyInner {B : Type*} [NonUnitalCStarAlgebra B] (T : B → B) : Prop :=
…
```
def OAI.WeakPureInfiniteness.cornerCoefficient line 47
Source documentation
Matrix-unit coefficient with its only nonzero entry in the top row.
```
def cornerCoefficient (f : A) (j : Fin 2) : CStarMatrix (Fin 2) (Fin 2) A :=
…
```
lemma OAI.WeakPureInfiniteness.cornerCoefficient_apply line 50
lemma OAI.WeakPureInfiniteness.cornerCoefficient_compression line 53
def OAI.WeakPureInfiniteness.doubledCornerLinear line 64
Source documentation
Duplicate the upper-left matrix entry.
```
def doubledCornerLinear : CStarMatrix (Fin 2) (Fin 2) A →ₗ[ℂ]
    CStarMatrix (Fin 2) (Fin 2) A :=
…
```
lemma OAI.WeakPureInfiniteness.doubledCornerLinear_apply line 74
lemma OAI.WeakPureInfiniteness.doubledCornerLinear_norm_le line 77
def OAI.WeakPureInfiniteness.doubledCorner line 82
lemma OAI.WeakPureInfiniteness.doubledCorner_apply line 87
lemma OAI.WeakPureInfiniteness.doubledCorner_norm_le line 90
lemma OAI.WeakPureInfiniteness.cornerCoefficient_tendsto line 95
lemma OAI.WeakPureInfiniteness.doubledCorner_completelyPositive line 122
lemma OAI.WeakPureInfiniteness.doubledCorner_finite_inner_approximation line 133
Source documentation
The two explicit coefficients approximate the doubled-corner map on any finite set. This is the approximately-inner input, not its one-step conclusion.
```
lemma doubledCorner_finite_inner_approximation
    (F : Finset (CStarMatrix (Fin 2) (Fin 2) A)) (ε : ℝ) (hε : 0 < ε) :
    ∃ v : Fin 2 → CStarMatrix (Fin 2) (Fin 2) A,
      ∀ X ∈ F, ‖doubledCorner X - finiteCompression v X‖ < ε := by
…
```
Mentions: OAI.WeakPureInfiniteness.doubledCorner, OAI.WeakPureInfiniteness.finiteCompression
lemma OAI.WeakPureInfiniteness.doubledCorner_approximatelyInner line 148
def OAI.WeakPureInfiniteness.topLeftCorner line 154
Source documentation
The input corner used for the two relative isometries.
```
def topLeftCorner (a : A) : CStarMatrix (Fin 2) (Fin 2) A :=
…
```
lemma OAI.WeakPureInfiniteness.topLeftCorner_apply line 157
lemma OAI.WeakPureInfiniteness.doubledCorner_topLeftCorner line 160
lemma OAI.WeakPureInfiniteness.topLeftCorner_compression_entry line 165

lemma OAI.WeakPureInfiniteness.relativePair_of_doubledCorner_witness line 173

Source documentation

Extract actual bounded relative Cuntz witnesses from a concrete one-step matrix approximation. This step uses multiplicative matrix entries.

lemma relativePair_of_doubledCorner_witness
    (d : CStarMatrix (Fin 2) (Fin 2) A) (hd : ‖d‖ ≤ 1)
    (F : Finset A) (ε : ℝ)
    (happrox : ∀ a ∈ F,
      ‖doubledCorner (topLeftCorner a) - star d * topLeftCorner a * d‖ < ε) :
    ‖d 0 0‖ ≤ 1 ∧ ‖d 0 1‖ ≤ 1 ∧
      ∀ a ∈ F, ‖star (d 0 0) * a * d 0 0 - a‖ < ε ∧
        ‖star (d 0 1) * a * d 0 1 - a‖ < ε ∧
        ‖star (d 0 0) * a * d 0 1‖ < ε := by
…

Mentions: OAI.WeakPureInfiniteness.doubledCorner, OAI.WeakPureInfiniteness.topLeftCorner