MatrixNearInclusion.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Matrix unit-ball proximity and graph row estimates

The cb distance supplies a separate approximant at each matrix level. No linear selection of those approximants is assumed.

def OAI.KadisonKastler.MatrixNearInclusion line 23
Source documentation
One direction of matrix unit-ball proximity, uniformly in the matrix size.
```
def MatrixNearInclusion (M N : VonNeumannAlgebra H) (γ : ℝ) : Prop :=
…
```
theorem OAI.KadisonKastler.MatrixNearInclusion.mono line 33

theorem OAI.KadisonKastler.MatrixNearInclusion.square line 44

Source documentation

The choice of finite index set does not affect the proximity bound.

theorem square (h : MatrixNearInclusion M N γ) {ι : Type*}
    [Fintype ι] [DecidableEq ι] (X : CStarMatrix ι ι (H →L[ℂ] H))
    (hX : ∀ i j, X i j ∈ M) (hn : ‖X‖ ≤ 1) :
    ∃ Y : CStarMatrix ι ι (H →L[ℂ] H),
      (∀ i j, Y i j ∈ N) ∧ ‖Y‖ ≤ 1 ∧ ‖X - Y‖ ≤ γ := by
…

Mentions: OAI.KadisonKastler.MatrixNearInclusion

def OAI.KadisonKastler.MatrixNearInclusion.rectangularCut line 61
def OAI.KadisonKastler.MatrixNearInclusion.moduleRestrictRight line 65
theorem OAI.KadisonKastler.MatrixNearInclusion.norm_moduleRestrictRight_le line 69
theorem OAI.KadisonKastler.MatrixNearInclusion.norm_rectangularCut_le line 80

theorem OAI.KadisonKastler.MatrixNearInclusion.rectangular line 97

Source documentation

Compression of the square approximant gives rectangular unit-ball proximity.

theorem rectangular (h : MatrixNearInclusion M N γ) {m n : Type*}
    [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
    (X : CStarMatrix m n (H →L[ℂ] H)) (hX : ∀ i j, X i j ∈ M) (hn : ‖X‖ ≤ 1) :
    ∃ Y : CStarMatrix m n (H →L[ℂ] H),
      (∀ i j, Y i j ∈ N) ∧ ‖Y‖ ≤ 1 ∧ ‖X - Y‖ ≤ γ := by
…

Mentions: OAI.KadisonKastler.MatrixNearInclusion

theorem OAI.KadisonKastler.MatrixNearInclusion.graphRow_approx line 111

Source documentation

Rescaling gives a row approximant with error proportional to the row norm.

theorem graphRow_approx (h : MatrixNearInclusion M N γ)
    (k : ℕ) (X : Fin k → H →L[ℂ] H) (hX : ∀ i, X i ∈ M) :
    ∃ Z : Fin k → H →L[ℂ] H, (∀ i, Z i ∈ N) ∧
      ‖operatorRow X - operatorRow Z‖ ≤ γ * ‖operatorRow X‖ := by
…

Mentions: OAI.KadisonKastler.MatrixNearInclusion, OAI.KadisonKastler.operatorRow

theorem OAI.KadisonKastler.MatrixNearInclusion.conjugate_right line 142
Source documentation
Moving the target algebra changes every matrix bound by at most the complete displacement of the conjugation.
```
theorem conjugate_right (h : MatrixNearInclusion M N γ)
    (u : unitary (H →L[ℂ] H)) :
    MatrixNearInclusion M (unitaryConjugateAlgebra u N)
      (γ + 2 * ‖(u : H →L[ℂ] H) - 1‖) := by
…
```
Mentions: OAI.KadisonKastler.MatrixNearInclusion, OAI.KadisonKastler.unitaryConjugateAlgebra
theorem OAI.KadisonKastler.MatrixNearInclusion.conjugate_left line 165
Source documentation
Moving the source algebra has the same matrix displacement bound.
```
theorem conjugate_left (h : MatrixNearInclusion M N γ)
    (u : unitary (H →L[ℂ] H)) :
    MatrixNearInclusion (unitaryConjugateAlgebra u M) N
      (γ + 2 * ‖(u : H →L[ℂ] H) - 1‖) := by
…
```
Mentions: OAI.KadisonKastler.MatrixNearInclusion, OAI.KadisonKastler.unitaryConjugateAlgebra
theorem OAI.KadisonKastler.MatrixNearInclusion.of_common_matrix_units line 195
Source documentation
A common countable matrix algebra supplies proximity from the ordinary gap.
```
theorem of_common_matrix_units (M N : VonNeumannAlgebra H)
    (D : Submodule ℂ H) [CompleteSpace D] (F : FullMatrixCorner D)
    (hM : ∀ i j, F.entry i j ∈ M) (hN : ∀ i j, F.entry i j ∈ N)
    {r : ℝ} (hr : kkDistance M N < r) : MatrixNearInclusion M N r := by
…
```
Mentions: OAI.KadisonKastler.FullMatrixCorner, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.MatrixNearInclusion
theorem OAI.KadisonKastler.MatrixNearInclusion.regularTensor_gap line 213
Source documentation
Matrix proximity in both directions controls the regular tensor product.
```
theorem regularTensor_gap (hMN : MatrixNearInclusion M N γ)
    (hNM : MatrixNearInclusion N M γ) (hγ : 0 ≤ γ) :
    kkDistance (regularTensorAlgebra M) (regularTensorAlgebra N) ≤ γ :=
…
```
Mentions: OAI.KadisonKastler.MatrixNearInclusion, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.regularTensorAlgebra