GrothendieckMatrix.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

A four-by-four matrix corner supplies unitary norm-attaining tests for an arbitrary bounded linear map without an additional convexity theorem.

def OAI.KadisonSimilarity.grothendieckEntry line 18
Source documentation
Extract an entry with its actual C-star matrix norm bound.
```
def grothendieckEntry (i j : Fin 2) : Mat A →L[ℂ] A :=
…
```
def OAI.KadisonSimilarity.grothendieckMatrixMap line 27
Source documentation
The original map applied to the distinguished off-diagonal entry.
```
def grothendieckMatrixMap (T : A →L[ℂ] H) : Mat (Mat A) →L[ℂ] H :=
…
```
theorem OAI.KadisonSimilarity.grothendieckMatrixMap_apply line 31
theorem OAI.KadisonSimilarity.grothendieckMatrixMap_norm_le line 35

theorem OAI.KadisonSimilarity.grothendieckMatrixMap_approximateUnitary line 46

Source documentation

A norm-one map has norm-attaining unitary tests in its matrix extension.

theorem grothendieckMatrixMap_approximateUnitary (T : A →L[ℂ] H) (hT : ‖T‖ = 1) :
    ∃ u : ℕ → unitary (Mat (Mat A)),
      Tendsto (fun n => ‖grothendieckMatrixMap T (u n : Mat (Mat A))‖) atTop (𝓝 1) := by
…

Mentions: OAI.KadisonSimilarity.grothendieckMatrixMap

def OAI.KadisonSimilarity.grothendieckCorner00 line 69
Source documentation
The two diagonal corner maps used for the two states.
```
def grothendieckCorner00 : A →ₗ[ℂ] Mat (Mat A) where
…
```
def OAI.KadisonSimilarity.grothendieckCorner11 line 74
def OAI.KadisonSimilarity.grothendieckOffDiagonal line 80
Source documentation
The distinguished off-diagonal corner.
```
def grothendieckOffDiagonal (a : A) : Mat (Mat A) := offdiag (offdiag a 0) 0
…
```
theorem OAI.KadisonSimilarity.grothendieckOffDiagonal_entry line 83
lemma OAI.KadisonSimilarity.grothendieck_diag_nonneg line 86
theorem OAI.KadisonSimilarity.grothendieckCorner00_nonneg line 94
theorem OAI.KadisonSimilarity.grothendieckCorner11_nonneg line 99
theorem OAI.KadisonSimilarity.grothendieckCorner00_one_norm line 103
theorem OAI.KadisonSimilarity.grothendieckCorner11_one_norm line 106
theorem OAI.KadisonSimilarity.grothendieckOffDiagonal_star_mul line 110
theorem OAI.KadisonSimilarity.grothendieckOffDiagonal_mul_star line 116
def OAI.KadisonSimilarity.grothendieckState11 line 122
Source documentation
Restrict the first matrix state to its supporting corner.
```
def grothendieckState11 (f : Mat (Mat A) →ₚ[ℂ] ℂ) : A →ₚ[ℂ] ℂ :=
…
```
def OAI.KadisonSimilarity.grothendieckState00 line 126
theorem OAI.KadisonSimilarity.grothendieckState11_apply line 131
theorem OAI.KadisonSimilarity.grothendieckState00_apply line 135
lemma OAI.KadisonSimilarity.grothendieckState11_mass line 138
lemma OAI.KadisonSimilarity.grothendieckState00_mass line 145

theorem OAI.KadisonSimilarity.normOne_grothendieck line 153

Source documentation

The two-state little Grothendieck inequality for a norm-one map.

theorem normOne_grothendieck (T : A →L[ℂ] H) (hT : ‖T‖ = 1) :
    ∃ f g : A →ₚ[ℂ] ℂ, (f 1).re ≤ 1 ∧ (g 1).re ≤ 1 ∧
      ∀ a, ‖T a‖ ^ 2 ≤ (f (star a * a)).re + (g (a * star a)).re := by
…

theorem OAI.KadisonSimilarity.littleGrothendieck_nontrivial line 166
Source documentation
Homogeneity gives the published inequality with its exact operator-norm factor.
```
theorem littleGrothendieck_nontrivial : LittleGrothendieckInput A H := by
…
```
Mentions: OAI.KadisonSimilarity.LittleGrothendieckInput

theorem OAI.KadisonSimilarity.littleGrothendieck_proved line 186

Source documentation

Haagerup's two-state bound, including the zero algebra.

theorem littleGrothendieck_proved {D E : Type*} [CStarAlgebra D] [PartialOrder D]
    [StarOrderedRing D] [NormedAddCommGroup E] [InnerProductSpace ℂ E] :
    LittleGrothendieckInput D E := by
…

Mentions: OAI.KadisonSimilarity.LittleGrothendieckInput