SpatialGap.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.NuclearUltrapower.laplacian_complement_expand line 32

Source documentation

Polynomial form of the complemented Laplacian, retaining arbitrary unitary tuples.

theorem laplacian_complement_expand (S : Finset Γ) (u : Γ → unitary A) :
    (4 * (S.card : ℝ)) • (1 : A) - laplacian S (fun s => (u s : A)) =
      (2 * (S.card : ℝ)) • (1 : A) + ∑ s ∈ S, ((u s : A) + star (u s : A)) := by
…

Mentions: OAI.NuclearUltrapower.laplacian

theorem OAI.NuclearUltrapower.laplacian_complement_expand_complex line 43
def OAI.NuclearUltrapower.laplacianComplement line 55
def OAI.NuclearUltrapower.tensorComplement line 63
Source documentation
The algebraic tensor polynomial whose norm expresses the required lower bound.
```
def tensorComplement (S : Finset Γ) (u : Γ → unitary B) (q : Γ → unitary C) : B ⊗[ℂ] C :=
…
```
def OAI.NuclearUltrapower.pairedTensorUnitary line 71
Source documentation
The tensor of two unitaries as a unitary of the completed tensor Hilbert space.
```
def pairedTensorUnitary (u : unitary (E →L[ℂ] E)) (v : unitary (F →L[ℂ] F)) :
    unitary (TensorHilbert E F →L[ℂ] TensorHilbert E F) :=
…
```
Mentions: OAI.NuclearUltrapower.TensorHilbert
theorem OAI.NuclearUltrapower.pairedTensorUnitary_coe line 79
theorem OAI.NuclearUltrapower.pairedTensorUnitary_action line 83
def OAI.NuclearUltrapower.spatialUnitaryTuple line 88

theorem OAI.NuclearUltrapower.spatial_complement line 97

Source documentation

Spatial evaluation followed by completion is the complemented unitary Laplacian.

theorem spatial_complement (S : Finset Γ) (u : Γ → unitary B) (q : Γ → unitary C)
    (H K : ComplexHilbert) (ρ : B →⋆ₐ[ℂ] (H →L[ℂ] H)) (σ : C →⋆ₐ[ℂ] (K →L[ℂ] K)) :
    (spatialEval H K ρ.toNonUnitalStarAlgHom σ.toNonUnitalStarAlgHom (tensorComplement S u q)).completion =
      (4 * (S.card : ℂ)) • (1 : TensorHilbert H K →L[ℂ] TensorHilbert H K) -
        laplacian S (fun s => completedTensorMap (ρ (u s)) (σ (q s))) := by
…

Mentions: OAI.NuclearUltrapower.ComplexHilbert, OAI.NuclearUltrapower.spatialEval, OAI.NuclearUltrapower.tensorComplement, OAI.NuclearUltrapower.TensorHilbert, OAI.NuclearUltrapower.laplacian, OAI.NuclearUltrapower.completedTensorMap

def OAI.NuclearUltrapower.tupleRepresentation line 133
theorem OAI.NuclearUltrapower.tupleRepresentation_apply line 138
theorem OAI.NuclearUltrapower.unitary_complement_norm_of_energy line 143

theorem OAI.NuclearUltrapower.spatial_complement_bound_unital line 157

Source documentation

The spatial estimate is abstracted from the quotient to keep inference local.

theorem spatial_complement_bound_unital (q : Γ →* unitary C)
    (S : Finset Γ) (κ : ℝ) (hS : S.Nonempty) (hκ0 : 0 < κ) (hκ : κ ≤ 4 * (S.card : ℝ))
    (hgap : HasKazhdanGap.{u,v} S κ)
    (hwm : ∀ (K : ComplexHilbert.{v}) (σ : C →⋆ₐ[ℂ] (K →L[ℂ] K)),
      HasNoFiniteDimensionalSubrep (tupleRepresentation q K σ))
    (u : Γ → unitary B)
    (H K : ComplexHilbert.{v}) (ρ : B →⋆ₐ[ℂ] (H →L[ℂ] H))
    (σ : C →⋆ₐ[ℂ] (K →L[ℂ] K)) :
    ‖spatialEval H K ρ.toNonUnitalStarAlgHom σ.toNonUnitalStarAlgHom (tensorComplement S u q)‖ ≤
      4 * (S.card : ℝ) - κ ^ 2 / (4 * (S.card : ℝ)) := by
…

Mentions: OAI.NuclearUltrapower.HasNoFiniteDimensionalSubrep, OAI.NuclearUltrapower.tupleRepresentation, OAI.NuclearUltrapower.spatialEval, OAI.NuclearUltrapower.tensorComplement

theorem OAI.NuclearUltrapower.spatial_complement_bound line 183