GrothendieckUltrapower.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Bounded families turn approximate unitary norm attainment into exact attainment. The source is the ordinary bounded product C-star algebra; only the Hilbert target needs an ultraproduct.

def OAI.KadisonSimilarity.grothendieckConstant line 19
Source documentation
Constants in the bounded product algebra.
```
def grothendieckConstant : B →⋆ₐ[ℂ] lp (fun _ : ℕ => B) ∞ where
…
```
theorem OAI.KadisonSimilarity.grothendieckConstant_apply line 28

def OAI.KadisonSimilarity.grothendieckFamilyLinear line 32

Source documentation

Coordinatewise application, with the ultralimit seminorm on its target.

def grothendieckFamilyLinear (ω : Ultrafilter ℕ) (T : B →L[ℂ] H) :
    lp (fun _ : ℕ => B) ∞ →ₗ[ℂ] UltraPreHilbert (fun _ : ℕ => H) ω where
…

theorem OAI.KadisonSimilarity.grothendieckFamilyLinear_apply line 43

def OAI.KadisonSimilarity.grothendieckFamilyMap line 48

Source documentation

The family map into the completed Hilbert ultraproduct.

def grothendieckFamilyMap (ω : Ultrafilter ℕ) (T : B →L[ℂ] H) :
    lp (fun _ : ℕ => B) ∞ →L[ℂ] HilbertUltraproduct (fun _ : ℕ => H) ω :=
…

theorem OAI.KadisonSimilarity.grothendieckFamilyMap_apply line 57
theorem OAI.KadisonSimilarity.grothendieckFamilyMap_norm_le line 62
theorem OAI.KadisonSimilarity.grothendieckFamilyMap_norm_tendsto line 71
theorem OAI.KadisonSimilarity.grothendieckFamilyMap_constant_norm line 78
def OAI.KadisonSimilarity.grothendieckUnitaryFamily line 85
Source documentation
A bounded family of unitaries is unitary in the bounded product.
```
def grothendieckUnitaryFamily (u : ℕ → unitary B) : unitary (lp (fun _ : ℕ => B) ∞) :=
…
```
theorem OAI.KadisonSimilarity.grothendieckUnitaryFamily_apply line 93
def OAI.KadisonSimilarity.grothendieckRestrict line 110
Source documentation
Restrict a positive functional on bounded families to the constants.
```
def grothendieckRestrict (f : lp (fun _ : ℕ => B) ∞ →ₚ[ℂ] ℂ) : B →ₚ[ℂ] ℂ :=
…
```
theorem OAI.KadisonSimilarity.grothendieckRestrict_apply line 117

theorem OAI.KadisonSimilarity.grothendieckFamily_attains line 122

Source documentation

The norm of a unitary family is attained at the limiting map.

theorem grothendieckFamily_attains (T : B →L[ℂ] H) (u : ℕ → unitary B)
    (hu : Tendsto (fun n => ‖T (u n : B)‖) atTop (𝓝 1)) :
    ‖grothendieckFamilyMap (Ultrafilter.of atTop) T
      (grothendieckUnitaryFamily u : lp (fun _ : ℕ => B) ∞)‖ = 1 :=
…

Mentions: OAI.KadisonSimilarity.grothendieckFamilyMap, OAI.KadisonSimilarity.grothendieckUnitaryFamily

theorem OAI.KadisonSimilarity.grothendieckFamily_states line 132

Source documentation

Apply the proved norm-attaining theorem inside the bounded product.

theorem grothendieckFamily_states (T : B →L[ℂ] H) (hT : ‖T‖ ≤ 1)
    (u : ℕ → unitary B)
    (hu : Tendsto (fun n => ‖T (u n : B)‖) atTop (𝓝 1)) :
    ∃ f g : lp (fun _ : ℕ => B) ∞ →ₚ[ℂ] ℂ, f 1 = 1 ∧ g 1 = 1 ∧
      ∀ X, ‖grothendieckFamilyMap (Ultrafilter.of atTop) T X‖ ^ 2 ≤
        (f (star X * X)).re + (g (X * star X)).re := by
…

Mentions: OAI.KadisonSimilarity.grothendieckFamilyMap

theorem OAI.KadisonSimilarity.approximateUnitary_grothendieck line 148

Source documentation

Approximate norm attainment at unitaries suffices for the exact two-state inequality.

theorem approximateUnitary_grothendieck (T : B →L[ℂ] H) (hT : ‖T‖ ≤ 1)
    (u : ℕ → unitary B)
    (hu : Tendsto (fun n => ‖T (u n : B)‖) atTop (𝓝 1)) :
    ∃ f g : B →ₚ[ℂ] ℂ, f 1 = 1 ∧ g 1 = 1 ∧
      ∀ b, ‖T b‖ ^ 2 ≤ (f (star b * b)).re + (g (b * star b)).re := by
…