Model.lean`

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.NuclearUltrapower.Dyadic line 12
Source comment
The dyadic coefficient ring is exactly Z[1/2].
Also declared: ComparatorChallenges/NuclearUltrapower.lean:12 (same declaration text).
```
abbrev Dyadic := Localization.Away (2 : ℤ)
```
abbrev OAI.NuclearUltrapower.Vector3 line 13
Also declared: ComparatorChallenges/NuclearUltrapower.lean:13 (same declaration text).
abbrev OAI.NuclearUltrapower.SL3Z line 14
Also declared: ComparatorChallenges/NuclearUltrapower.lean:14 (same declaration text).
def OAI.NuclearUltrapower.dyadicTwo line 16
Also declared: ComparatorChallenges/NuclearUltrapower.lean:16 (same declaration text).
def OAI.NuclearUltrapower.matrixAction line 19
Also declared: ComparatorChallenges/NuclearUltrapower.lean:19 (same declaration text).
def OAI.NuclearUltrapower.dilationAction line 23
Also declared: ComparatorChallenges/NuclearUltrapower.lean:23 (same declaration text).
def OAI.NuclearUltrapower.groupAction line 27
Also declared: ComparatorChallenges/NuclearUltrapower.lean:27 (same declaration text).
abbrev OAI.NuclearUltrapower.G line 39
Source documentation
The exact group of the semidirect-product construction.
Also declared: ComparatorChallenges/NuclearUltrapower.lean:39 (same declaration text).
```
abbrev G := SemidirectProduct (Multiplicative Vector3)
…
```
Mentions: OAI.NuclearUltrapower.Vector3
abbrev OAI.NuclearUltrapower.BoundedSeq line 46
Source documentation
Bounded sequences, with their supremum norm. N is discrete.
Also declared: ComparatorChallenges/NuclearUltrapower.lean:46 (same declaration text).
```
abbrev BoundedSeq := BoundedContinuousFunction ℕ B
```
def OAI.NuclearUltrapower.ultraRel line 49
Source documentation
Equality modulo I_omega(B). This is equivalent to norm-null difference.
Also declared: ComparatorChallenges/NuclearUltrapower.lean:49 (same declaration text).
```
def ultraRel (x y : BoundedSeq B) : Prop :=
…
```
Mentions: OAI.NuclearUltrapower.BoundedSeq
def OAI.NuclearUltrapower.ultraCon line 53
Source documentation
The ring congruence defining the norm (not algebraic) ultrapower.
Also declared: ComparatorChallenges/NuclearUltrapower.lean:53 (same declaration text).
```
def ultraCon : RingCon (BoundedSeq B) where
…
```
Mentions: OAI.NuclearUltrapower.BoundedSeq
abbrev OAI.NuclearUltrapower.NormUltrapower line 74
Source documentation
The exact quotient l-infinity(N,B)/I_omega(B) as a complex star algebra. The quotient identifies sequences whose difference tends to zero along the ultrafilter.
Also declared: ComparatorChallenges/NuclearUltrapower.lean:74 (same declaration text).
```
abbrev NormUltrapower := (ultraCon B ω).Quotient
```
Mentions: OAI.NuclearUltrapower.ultraCon
instance OAI.NuclearUltrapower.(instance at line 76) line 76
instance OAI.NuclearUltrapower.(instance at line 81) line 81
instance OAI.NuclearUltrapower.(instance at line 97) line 97
def OAI.NuclearUltrapower.IsFree line 104
Source documentation
Freeness: no finite subset of N belongs to the ultrafilter.
Also declared: ComparatorChallenges/NuclearUltrapower.lean:104 (same declaration text).
```
def IsFree (ω : Ultrafilter ℕ) : Prop :=
…
```
structure OAI.NuclearUltrapower.ComplexHilbert line 110
Source documentation
A bundled complex Hilbert space, without any separability assumption.
Also declared: ComparatorChallenges/NuclearUltrapower.lean:110 (same declaration text).
```
structure ComplexHilbert where
…
```
instance OAI.NuclearUltrapower.(instance at line 117) line 117
def OAI.NuclearUltrapower.spatialEval line 124
Source documentation
Spatial evaluation of the algebraic tensor product on separate Hilbert spaces. Its operator norm is unchanged on the Hilbert completion.
Also declared: ComparatorChallenges/NuclearUltrapower.lean:124 (same declaration text).
```
def spatialEval (H K : ComplexHilbert.{w})
    (ρ : B →⋆ₙₐ[ℂ] (H →L[ℂ] H)) (σ : C →⋆ₙₐ[ℂ] (K →L[ℂ] K)) :
    B ⊗[ℂ] C →ₗ[ℂ] ((H ⊗[ℂ] K) →L[ℂ] (H ⊗[ℂ] K)) :=
…
```
def OAI.NuclearUltrapower.commutingEval line 134
Source documentation
Evaluation on one Hilbert space; used only when the two ranges commute.
Also declared: ComparatorChallenges/NuclearUltrapower.lean:134 (same declaration text).
```
def commutingEval (H : ComplexHilbert.{w})
    (ρ : B →⋆ₙₐ[ℂ] (H →L[ℂ] H)) (σ : C →⋆ₙₐ[ℂ] (H →L[ℂ] H)) :
    B ⊗[ℂ] C →ₗ[ℂ] (H →L[ℂ] H) :=
…
```
def OAI.NuclearUltrapower.minTensorNorm line 145
Source documentation
The minimal C*-tensor norm: supremum over spatial representations.
Also declared: ComparatorChallenges/NuclearUltrapower.lean:145 (same declaration text).
```
def minTensorNorm (x : B ⊗[ℂ] C) : ℝ :=
…
```
def OAI.NuclearUltrapower.maxTensorNorm line 151
Source documentation
The maximal C*-tensor norm: supremum over commuting representations.
Also declared: ComparatorChallenges/NuclearUltrapower.lean:151 (same declaration text).
```
def maxTensorNorm (x : B ⊗[ℂ] C) : ℝ :=
…
```
def OAI.NuclearUltrapower.IsNuclear line 158
Source documentation
Nuclearity in the tensor-norm convention of the tensor-norm formulation. The second C*-algebra need not be unital, nonzero, or separable.
Also declared: ComparatorChallenges/NuclearUltrapower.lean:158 (same declaration text).
```
def IsNuclear (B : Type u) [NonUnitalCStarAlgebra B] : Prop :=
…
```
structure OAI.NuclearUltrapower.UnitalCStar line 164
Source documentation
A nonzero unital complex C*-algebra.
Also declared: ComparatorChallenges/NuclearUltrapower.lean:164 (same declaration text).
```
structure UnitalCStar where
…
```
instance OAI.NuclearUltrapower.(instance at line 169) line 169
def OAI.NuclearUltrapower.IsFullGroupAlgebra line 174
Source documentation
The universal property defining the full, not the reduced, group C*-algebra. The dense generation clause makes the intended completion explicit. This is definition data, not a hypothesis silently supplied to the main claim.
Also declared: ComparatorChallenges/NuclearUltrapower.lean:174 (same declaration text).
```
def IsFullGroupAlgebra (A : UnitalCStar.{u}) (ι : G →* unitary A) : Prop :=
…
```
Mentions: OAI.NuclearUltrapower.G
def OAI.NuclearUltrapower.CuntzTwoRelations line 180
Source documentation
The two Cuntz relations, including unit preservation explicitly.
Also declared: ComparatorChallenges/NuclearUltrapower.lean:180 (same declaration text).
```
def CuntzTwoRelations {D : Type u} [CStarAlgebra D] (s : Fin 2 → D) : Prop :=
…
```
def OAI.NuclearUltrapower.IsCuntzTwoAlgebra line 184
Source documentation
The universal nonzero unital C*-algebra on the two Cuntz isometries.
Also declared: ComparatorChallenges/NuclearUltrapower.lean:184 (same declaration text).
```
def IsCuntzTwoAlgebra (O : UnitalCStar.{u}) (s : Fin 2 → O) : Prop :=
…
```
def OAI.NuclearUltrapower.MainStatementWithCuntzCorollary line 191
Source documentation
The manuscript's main statement including its explicitly stated O_2 corollary. Both universal C*-algebras must be constructed to prove this.
Also declared: ComparatorChallenges/NuclearUltrapower.lean:191 (same declaration text).
```
def MainStatementWithCuntzCorollary : Prop :=
…
```