TensorGap.lean`

38 declarations, 0 contain sorry, 0 declared as axioms

def OAI.NuclearUltrapower.operatorMatrixAction line 26
Source documentation
The actual left action of an operator-valued matrix on a Hilbert direct sum.
```
def operatorMatrixAction (M : CStarMatrix n n (H →L[ℂ] H)) :
    PiLp 2 (fun _ : n => H) →L[ℂ] PiLp 2 (fun _ : n => H) where
…
```
theorem OAI.NuclearUltrapower.operatorMatrixAction_apply line 38

def OAI.NuclearUltrapower.operatorMatrixActionHom line 42

Source documentation

Matrix amplification is a genuine unital star homomorphism.

def operatorMatrixActionHom : CStarMatrix n n (H →L[ℂ] H) →⋆ₐ[ℂ]
    (PiLp 2 (fun _ : n => H) →L[ℂ] PiLp 2 (fun _ : n => H)) where
…

theorem OAI.NuclearUltrapower.operatorMatrixActionHom_apply line 65
theorem OAI.NuclearUltrapower.operatorMatrixActionHom_injective line 69
Source documentation
One-column vectors recover every coefficient; amplification is faithful.
```
theorem operatorMatrixActionHom_injective : Function.Injective (operatorMatrixActionHom (n := n) (H := H)) := by
…
```
Mentions: OAI.NuclearUltrapower.operatorMatrixActionHom
theorem OAI.NuclearUltrapower.operatorMatrixActionHom_isometry line 78
def OAI.NuclearUltrapower.tensorPiLinearEquiv line 90
Source documentation
The fixed-factor tensor/direct-sum identification, with its actual Hilbert norm.
```
def tensorPiLinearEquiv (b : OrthonormalBasis n ℂ F) :
    E ⊗[ℂ] F ≃ₗ[ℂ] PiLp 2 (fun _ : n => E) :=
…
```
theorem OAI.NuclearUltrapower.tensorPiLinearEquiv_tmul line 96
theorem OAI.NuclearUltrapower.tensorPiLinearEquiv_inner line 100
def OAI.NuclearUltrapower.tensorPiIsometry line 121
theorem OAI.NuclearUltrapower.tensorPiIsometry_tmul line 125
def OAI.NuclearUltrapower.tensorOperatorMatrix line 131
Source documentation
This matrix has scalar coefficients in the fixed factor; the first factor may be infinite-dimensional.
```
def tensorOperatorMatrix (b : OrthonormalBasis n ℂ F)
    (U : E →L[ℂ] E) (V : F →L[ℂ] F) : CStarMatrix n n (E →L[ℂ] E) :=
…
```
theorem OAI.NuclearUltrapower.tensorOperatorMatrix_apply line 136
theorem OAI.NuclearUltrapower.tensorOperatorMatrix_action line 141
Source documentation
Entry-by-entry compatibility of the operator tensor with matrix amplification.
```
theorem tensorOperatorMatrix_action [CompleteSpace E] (b : OrthonormalBasis n ℂ F)
    (U : E →L[ℂ] E) (V : F →L[ℂ] F) (z : E ⊗[ℂ] F) :
    operatorMatrixActionHom (n := n) (H := E) (tensorOperatorMatrix b U V) (tensorPiIsometry b z) =
…
```
Mentions: OAI.NuclearUltrapower.operatorMatrixActionHom, OAI.NuclearUltrapower.tensorOperatorMatrix, OAI.NuclearUltrapower.tensorPiIsometry
def OAI.NuclearUltrapower.tensorPiUnitary line 167
theorem OAI.NuclearUltrapower.tensorPiUnitary_apply_tensorPi line 172
theorem OAI.NuclearUltrapower.tensorOperatorMatrix_conjugacy line 178

theorem OAI.NuclearUltrapower.tensorMatrix_complement_bound line 193

Source documentation

Fixed-factor matrix norms see precisely the tensor Kazhdan estimate.

theorem tensorMatrix_complement_bound {Γ : Type*} (S : Finset Γ)
    (b : OrthonormalBasis n ℂ F) (U : Γ → (E ≃ₗᵢ[ℂ] E)) (V : Γ → (F ≃ₗᵢ[ℂ] F))
    {κ : ℝ} (hκ : κ ≤ 4 * (S.card : ℝ))
    (hgap : ∀ z : E ⊗[ℂ] F, κ * ‖z‖ ^ 2 ≤
      ∑ s ∈ S, ‖TensorProduct.congrIsometry (U s) (V s) z - z‖ ^ 2) :
    ‖(4 * (S.card : ℝ)) • (1 : CStarMatrix n n (E →L[ℂ] E)) -
      laplacian S (fun s => tensorOperatorMatrix b (U s) (V s))‖ ≤
        4 * (S.card : ℝ) - κ := by
…

Mentions: OAI.NuclearUltrapower.laplacian, OAI.NuclearUltrapower.tensorOperatorMatrix

def OAI.NuclearUltrapower.coefficientMatrix line 242
Source documentation
An elementary tensor in coordinates of the fixed second factor.
```
def coefficientMatrix (c : n → n → ℂ) (a : A) : CStarMatrix n n A :=
…
```
theorem OAI.NuclearUltrapower.coefficientMatrix_apply line 246
theorem OAI.NuclearUltrapower.matrixMap_coefficientMatrix line 249
theorem OAI.NuclearUltrapower.map_laplacian line 254
theorem OAI.NuclearUltrapower.map_laplacian_complement line 258
def OAI.NuclearUltrapower.VariableUltra.eval line 271
Source documentation
Evaluation is an actual unital star homomorphism.
```
def eval (i : ι) : Seq A →⋆ₐ[ℂ] A i where
…
```
Mentions: OAI.NuclearUltrapower.VariableUltra.Seq
theorem OAI.NuclearUltrapower.VariableUltra.eval_apply line 280
def OAI.NuclearUltrapower.VariableUltra.unitarySequence line 283
Source documentation
Arbitrary coordinate unitaries are bounded, without a dimension bound.
```
def unitarySequence (u : ∀ i, unitary (A i)) : unitary (Seq A) :=
…
```
Mentions: OAI.NuclearUltrapower.VariableUltra.Seq
theorem OAI.NuclearUltrapower.VariableUltra.unitarySequence_apply line 291
theorem OAI.NuclearUltrapower.VariableUltra.matrixFamily_eval line 303

theorem OAI.NuclearUltrapower.VariableUltra.coefficient_complement_quotient_bound line 307

Source documentation

Fixed-size polynomial transfer, with only an EVENTUAL coordinate bound.

theorem coefficient_complement_quotient_bound {Γ : Type*} (S : Finset Γ)
    (u : Γ → Seq A) (c : Γ → n → n → ℂ) (R C : ℝ)
    (h : ∀ᶠ i in (ω : Filter ι),
      ‖R • (1 : CStarMatrix n n (A i)) -
        laplacian S (fun s => coefficientMatrix (c s) (u s i))‖ ≤ C) :
    ‖R • (1 : CStarMatrix n n (Algebra A ω)) -
      laplacian S (fun s => coefficientMatrix (c s) (mk A ω (u s)))‖ ≤ C := by
…

Mentions: OAI.NuclearUltrapower.VariableUltra.Seq, OAI.NuclearUltrapower.laplacian, OAI.NuclearUltrapower.coefficientMatrix, OAI.NuclearUltrapower.VariableUltra.Algebra, OAI.NuclearUltrapower.VariableUltra.mk

theorem OAI.NuclearUltrapower.no_invariant_of_complement_norm line 349

Source documentation

A strict complemented-norm gap excludes every common fixed vector.

theorem no_invariant_of_complement_norm (S : Finset Γ) (a : Γ → (H →L[ℂ] H))
    {κ : ℝ} (hκ : 0 < κ)
    (h : ‖(4 * (S.card : ℝ)) • (1 : H →L[ℂ] H) - laplacian S a‖ ≤
      4 * (S.card : ℝ) - κ) (x : H) (hx : ∀ s ∈ S, a s x = x) : x = 0 := by
…

Mentions: OAI.NuclearUltrapower.laplacian

abbrev OAI.NuclearUltrapower.VariableUltra.operatorSeq line 371
abbrev OAI.NuclearUltrapower.VariableUltra.operatorQuotient line 372
def OAI.NuclearUltrapower.VariableUltra.isoSequence line 374
def OAI.NuclearUltrapower.VariableUltra.starAlgToStarMonoid line 377
def OAI.NuclearUltrapower.VariableUltra.quotientIsoUnitary line 384
def OAI.NuclearUltrapower.VariableUltra.representedIso line 391

theorem OAI.NuclearUltrapower.VariableUltra.quotient_tensor_complement_bound line 402

Source documentation

The strict coordinate tensor gap survives in EVERY unital representation of the varying matrix quotient. No faithfulness is needed here.

theorem quotient_tensor_complement_bound {Γ : Type*} (S : Finset Γ)
    (b : OrthonormalBasis n ℂ F) (U : ∀ i, Γ → (E i ≃ₗᵢ[ℂ] E i))
    (V : Γ → (F ≃ₗᵢ[ℂ] F)) {κ : ℝ} (hκ : κ ≤ 4 * (S.card : ℝ))
    (hgap : ∀ᶠ i in (ω : Filter ι), ∀ z : E i ⊗[ℂ] F,
      κ * ‖z‖ ^ 2 ≤ ∑ s ∈ S, ‖TensorProduct.congrIsometry (U i s) (V s) z - z‖ ^ 2)
    (φ : operatorQuotient E ω →⋆ₐ[ℂ] (K →L[ℂ] K)) :
    ‖(4 * (S.card : ℝ)) • (1 : CStarMatrix n n (K →L[ℂ] K)) -
      laplacian S (fun s => tensorOperatorMatrix b
        (representedIso E ω φ (fun i => U i s)) (V s))‖ ≤ 4 * (S.card : ℝ) - κ := by
…

Mentions: OAI.NuclearUltrapower.VariableUltra.operatorQuotient, OAI.NuclearUltrapower.laplacian, OAI.NuclearUltrapower.tensorOperatorMatrix, OAI.NuclearUltrapower.VariableUltra.representedIso

theorem OAI.NuclearUltrapower.VariableUltra.quotient_tensor_no_invariants line 438

Source documentation

In particular a tensor intertwiner in a quotient representation must vanish.

theorem quotient_tensor_no_invariants {Γ : Type*} (S : Finset Γ)
    (b : OrthonormalBasis n ℂ F) (U : ∀ i, Γ → (E i ≃ₗᵢ[ℂ] E i))
    (V : Γ → (F ≃ₗᵢ[ℂ] F)) {κ : ℝ} (hκ0 : 0 < κ) (hκ : κ ≤ 4 * (S.card : ℝ))
    (hgap : ∀ᶠ i in (ω : Filter ι), ∀ z : E i ⊗[ℂ] F,
      κ * ‖z‖ ^ 2 ≤ ∑ s ∈ S, ‖TensorProduct.congrIsometry (U i s) (V s) z - z‖ ^ 2)
    (φ : operatorQuotient E ω →⋆ₐ[ℂ] (K →L[ℂ] K))
    (z : K ⊗[ℂ] F)
    (hz : ∀ s ∈ S, TensorProduct.congrIsometry
      (representedIso E ω φ (fun i => U i s)) (V s) z = z) : z = 0 := by
…

Mentions: OAI.NuclearUltrapower.VariableUltra.operatorQuotient, OAI.NuclearUltrapower.VariableUltra.representedIso