MatrixNearCommutant.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Commutant estimates from individual matrix approximants

A matrix approximant from N commutes entrywise with a contraction in N′. The complete commutator is therefore bounded by twice the matrix error. The commutant distance formula gives distance at most that error to M′; normalization costs a further factor two for unit balls. No linear map selecting the matrix approximants is assumed.

theorem OAI.KadisonKastler.MatrixNearInclusion.scaled_square line 38

Source documentation

Individual approximants scale with the norm of the input matrix.

theorem scaled_square (h : MatrixNearInclusion M N γ)
    (n : ℕ) (X : CStarMatrix (Fin n) (Fin n) (H →L[ℂ] H))
    (hX : ∀ i j, X i j ∈ M) :
    ∃ Y : CStarMatrix (Fin n) (Fin n) (H →L[ℂ] H),
      (∀ i j, Y i j ∈ N) ∧ ‖X - Y‖ ≤ γ * ‖X‖ := by
…

Mentions: OAI.KadisonKastler.MatrixNearInclusion

theorem OAI.KadisonKastler.MatrixNearInclusion.mapped_derivation_eq line 62
theorem OAI.KadisonKastler.MatrixNearInclusion.commutant_complete_bound line 80
Source documentation
Matrix proximity bounds the full derivation of a neighboring commutant contraction, uniformly at every rectangular matrix level.
```
theorem commutant_complete_bound (h : MatrixNearInclusion M N γ)
    (hγ : 0 ≤ γ) (a : H →L[ℂ] H) (ha : a ∈ N.commutant) (han : ‖a‖ ≤ 1) :
    CompletelyBoundedBy
      ((innerDerivation a).comp M.toStarSubalgebra.subtype.toLinearMap) (2 * γ) := by
…
```
Mentions: OAI.KadisonKastler.MatrixNearInclusion, OAI.KadisonKastler.CompletelyBoundedBy, OAI.KadisonKastler.innerDerivation
theorem OAI.KadisonKastler.MatrixNearInclusion.commutant_infDist_le line 113
Source documentation
The factor one-half in the complete commutator distance formula cancels the factor two in the preceding estimate.
```
theorem commutant_infDist_le (h : MatrixNearInclusion M N γ)
    (hγ : 0 ≤ γ)
    (hPublished : PublishedBlockCommutantApproximation (Algebra M) H)
    (a : H →L[ℂ] H) (ha : a ∈ unitBall N.commutant) :
    Metric.infDist a (M.commutant : Set (H →L[ℂ] H)) ≤ γ := by
…
```
Mentions: OAI.KadisonKastler.MatrixNearInclusion, OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.unitBall
theorem OAI.KadisonKastler.MatrixNearInclusion.commutant_nearInclusion line 128
Source documentation
The algebra near-inclusion is contravariant and needs no normalization loss. The larger constant is needed only for proximity of unit balls.
```
theorem commutant_nearInclusion (h : MatrixNearInclusion M N γ)
    (hγ : 0 ≤ γ)
    (hPublished : PublishedBlockCommutantApproximation (Algebra M) H)
    {η : ℝ} (hγη : γ < η) : NearInclusion N.commutant M.commutant η :=
…
```
Mentions: OAI.KadisonKastler.MatrixNearInclusion, OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.NearInclusion
theorem OAI.KadisonKastler.MatrixNearInclusion.exists_commutant_unitBall_approx line 136
Source documentation
Normalization yields a commutant unit-ball approximant with any error strictly larger than twice the matrix gap.
```
theorem exists_commutant_unitBall_approx (h : MatrixNearInclusion M N γ)
    (hγ : 0 ≤ γ)
    (hPublished : PublishedBlockCommutantApproximation (Algebra M) H)
    (a : H →L[ℂ] H) (ha : a ∈ unitBall N.commutant)
    {η : ℝ} (hγη : 2 * γ < η) :
    ∃ b ∈ unitBall M.commutant, ‖a - b‖ < η := by
…
```
Mentions: OAI.KadisonKastler.MatrixNearInclusion, OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.unitBall
theorem OAI.KadisonKastler.MatrixNearInclusion.commutant_kkDistance_le line 149
Source documentation
Two-sided matrix proximity controls the ordinary commutant gap.
```
theorem commutant_kkDistance_le (hMN : MatrixNearInclusion M N γ)
    (hNM : MatrixNearInclusion N M γ) (hγ : 0 ≤ γ)
    (hM : PublishedBlockCommutantApproximation (Algebra M) H)
    (hN : PublishedBlockCommutantApproximation (Algebra N) H) :
    kkDistance M.commutant N.commutant ≤ 2 * γ := by
…
```
Mentions: OAI.KadisonKastler.MatrixNearInclusion, OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.kkDistance