TensorNorms.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.NuclearUltrapower.spatialEval_tmul line 30
theorem OAI.NuclearUltrapower.commutingEval_tmul line 34

theorem OAI.NuclearUltrapower.evals_bounded line 40

Source documentation

Uniform finite projective bound on all spatial and commuting evaluations. In particular the real suprema defining the tensor norms are genuine bounds.

theorem evals_bounded (x : B ⊗[ℂ] C) :
    ∃ M : ℝ, (∀ (H K : ComplexHilbert.{w})
      (ρ : B →⋆ₙₐ[ℂ] (H →L[ℂ] H)) (σ : C →⋆ₙₐ[ℂ] (K →L[ℂ] K)),
      ‖spatialEval H K ρ σ x‖ ≤ M) ∧
      (∀ (H : ComplexHilbert.{w}) (ρ : B →⋆ₙₐ[ℂ] (H →L[ℂ] H))
      (σ : C →⋆ₙₐ[ℂ] (H →L[ℂ] H)), ‖commutingEval H ρ σ x‖ ≤ M) := by
…

Mentions: OAI.NuclearUltrapower.spatialEval, OAI.NuclearUltrapower.commutingEval

theorem OAI.NuclearUltrapower.norm_spatialEval_le line 69
theorem OAI.NuclearUltrapower.norm_commutingEval_le line 80

theorem OAI.NuclearUltrapower.nuclear_transfer_norm line 95

Source documentation

Nuclearity precisely transfers a bound in every spatial realization to every commuting realization. This is the sole tensor-norm step in the source nuclear-finiteness proof, with no identification with coordinate quotients.

theorem nuclear_transfer_norm (hB : IsNuclear.{u,v} B) (x : B ⊗[ℂ] C) (M : ℝ)
    (hM : ∀ (H K : ComplexHilbert.{max u v})
      (ρ : B →⋆ₙₐ[ℂ] (H →L[ℂ] H)) (σ : C →⋆ₙₐ[ℂ] (K →L[ℂ] K)),
        ‖spatialEval H K ρ σ x‖ ≤ M)
    (H : ComplexHilbert.{max u v}) (ρ : B →⋆ₙₐ[ℂ] (H →L[ℂ] H))
    (σ : C →⋆ₙₐ[ℂ] (H →L[ℂ] H)) (hcomm : ∀ b c, Commute (ρ b) (σ c)) :
    ‖commutingEval H ρ σ x‖ ≤ M := by
…

Mentions: OAI.NuclearUltrapower.spatialEval, OAI.NuclearUltrapower.commutingEval

def OAI.NuclearUltrapower.representationSupport line 121
Source documentation
The nondegenerate support of a possibly nonunital representation.
```
def representationSupport (φ : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) : Submodule ℂ H :=
…
```
theorem OAI.NuclearUltrapower.mem_representationSupport line 124
instance OAI.NuclearUltrapower.supportComplete line 128
def OAI.NuclearUltrapower.supportProjection line 133
Source documentation
Projection to the support, without invoking separability or nonzero spaces.
```
def supportProjection (φ : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) :
    H →L[ℂ] representationSupport φ :=
…
```
Mentions: OAI.NuclearUltrapower.representationSupport
theorem OAI.NuclearUltrapower.supportProjection_coe line 140
theorem OAI.NuclearUltrapower.supportProjection_subtype line 143
def OAI.NuclearUltrapower.supportRepresentation line 149
Source documentation
A possibly degenerate representation becomes unital on its actual support.
```
def supportRepresentation (φ : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) :
    A →⋆ₐ[ℂ] (representationSupport φ →L[ℂ] representationSupport φ) where
…
```
Mentions: OAI.NuclearUltrapower.representationSupport
theorem OAI.NuclearUltrapower.supportRepresentation_coe line 170
theorem OAI.NuclearUltrapower.representation_support_factor line 174
Source documentation
The original representation is its unital support plus a zero representation.
```
theorem representation_support_factor (φ : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) (a : A) :
    φ a = (representationSupport φ).subtypeL.comp ((supportRepresentation φ a).comp
      (supportProjection φ)) := by
…
```
Mentions: OAI.NuclearUltrapower.representationSupport, OAI.NuclearUltrapower.supportRepresentation, OAI.NuclearUltrapower.supportProjection
theorem OAI.NuclearUltrapower.supportProjection_norm_le line 182
Source documentation
Orthogonal projection has norm at most one, including the zero support.
```
theorem supportProjection_norm_le (φ : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) :
    ‖supportProjection φ‖ ≤ 1 := by
…
```
Mentions: OAI.NuclearUltrapower.supportProjection
abbrev OAI.NuclearUltrapower.supportHilbert line 204

theorem OAI.NuclearUltrapower.spatialEval_support_factor line 209

Source documentation

Degenerate spatial representations factor through their two unital supports.

theorem spatialEval_support_factor (x : B ⊗[ℂ] C) (H K : ComplexHilbert.{w})
    (ρ : B →⋆ₙₐ[ℂ] (H →L[ℂ] H)) (σ : C →⋆ₙₐ[ℂ] (K →L[ℂ] K)) :
    spatialEval H K ρ σ x =
      (TensorProduct.mapL (representationSupport ρ).subtypeL (representationSupport σ).subtypeL).comp
        ((spatialEval (supportHilbert H ρ) (supportHilbert K σ)
          (supportRepresentation ρ).toNonUnitalStarAlgHom
          (supportRepresentation σ).toNonUnitalStarAlgHom x).comp
            (TensorProduct.mapL (supportProjection ρ) (supportProjection σ))) := by
…

Mentions: OAI.NuclearUltrapower.spatialEval, OAI.NuclearUltrapower.representationSupport, OAI.NuclearUltrapower.supportHilbert, OAI.NuclearUltrapower.supportRepresentation, OAI.NuclearUltrapower.supportProjection

theorem OAI.NuclearUltrapower.spatialEval_norm_le_support line 229

Source documentation

No unitality was hidden in the minimal tensor norm quantifier.

theorem spatialEval_norm_le_support (x : B ⊗[ℂ] C) (H K : ComplexHilbert.{w})
    (ρ : B →⋆ₙₐ[ℂ] (H →L[ℂ] H)) (σ : C →⋆ₙₐ[ℂ] (K →L[ℂ] K)) :
    ‖spatialEval H K ρ σ x‖ ≤
      ‖spatialEval (supportHilbert H ρ) (supportHilbert K σ)
        (supportRepresentation ρ).toNonUnitalStarAlgHom
        (supportRepresentation σ).toNonUnitalStarAlgHom x‖ := by
…

Mentions: OAI.NuclearUltrapower.spatialEval, OAI.NuclearUltrapower.supportHilbert, OAI.NuclearUltrapower.supportRepresentation

theorem OAI.NuclearUltrapower.spatial_bound_of_unital line 256

Source documentation

It suffices to bound all unital spatial realizations, not to assume away the others.

theorem spatial_bound_of_unital (x : B ⊗[ℂ] C) (M : ℝ)
    (h : ∀ (H K : ComplexHilbert.{w}) (ρ : B →⋆ₐ[ℂ] (H →L[ℂ] H))
      (σ : C →⋆ₐ[ℂ] (K →L[ℂ] K)),
      ‖spatialEval H K ρ.toNonUnitalStarAlgHom σ.toNonUnitalStarAlgHom x‖ ≤ M)
    (H K : ComplexHilbert.{w}) (ρ : B →⋆ₙₐ[ℂ] (H →L[ℂ] H))
    (σ : C →⋆ₙₐ[ℂ] (K →L[ℂ] K)) : ‖spatialEval H K ρ σ x‖ ≤ M := by
…

Mentions: OAI.NuclearUltrapower.spatialEval

def OAI.NuclearUltrapower.scalarHilbert line 289
theorem OAI.NuclearUltrapower.minTensorNorm_nonneg line 291
def OAI.NuclearUltrapower.tensorLeftRep line 296
def OAI.NuclearUltrapower.tensorRightRep line 300
theorem OAI.NuclearUltrapower.tensorLeftRep_apply line 304
theorem OAI.NuclearUltrapower.tensorRightRep_apply line 307
theorem OAI.NuclearUltrapower.tensor_reps_commute line 311
theorem OAI.NuclearUltrapower.completed_spatial_eq line 318
Source documentation
Spatial evaluation is the commuting evaluation on the Hilbert completion; completion does not change its operator norm.
```
theorem completed_spatial_eq (H K : ComplexHilbert.{0})
    (R : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) (S : C →⋆ₙₐ[ℂ] (K →L[ℂ] K)) (x : A ⊗[ℂ] C) :
    (spatialEval H K R S x).completion =
      commutingEval ⟨TensorHilbert H K⟩ (tensorLeftRep R) (tensorRightRep S) x := by
…
```
Mentions: OAI.NuclearUltrapower.spatialEval, OAI.NuclearUltrapower.commutingEval, OAI.NuclearUltrapower.TensorHilbert, OAI.NuclearUltrapower.tensorLeftRep, OAI.NuclearUltrapower.tensorRightRep
theorem OAI.NuclearUltrapower.minTensorNorm_le_maxTensorNorm line 330
Source documentation
The easy inequality holds for every C*-algebra, including nonunital ones.
```
theorem minTensorNorm_le_maxTensorNorm (x : A ⊗[ℂ] C) :
    minTensorNorm.{0,0,0} x ≤ maxTensorNorm.{0,0,0} x := by
…
```
theorem OAI.NuclearUltrapower.maxTensorNorm_le_of_commuting line 339