Compactness.lean`

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Closed quasitrace constraints and compactness of normalized two-quasitraces.

inductive OAI.Kaplansky.QuasitraceConstraint line 16
def OAI.Kaplansky.QuasitraceConstraint.Holds line 27
def OAI.Kaplansky.oneQuasitraceOfConstraints line 36
Source documentation
All coordinate requirements reconstruct the original bundled object, including complex linearity on each closed nonunital abelian algebra.
```
def oneQuasitraceOfConstraints (f : A → ℂ)
    (hf : ∀ q : QuasitraceConstraint A, q.Holds f) : OneQuasitrace A where
…
```
Mentions: OAI.Kaplansky.QuasitraceConstraint, OAI.Kaplansky.OneQuasitrace
theorem OAI.Kaplansky.OneQuasitrace.satisfies_constraint line 48
theorem OAI.Kaplansky.QuasitraceConstraint.isClosed line 62
Source documentation
Each requirement is closed in the topology of pointwise convergence.
```
theorem QuasitraceConstraint.isClosed (q : QuasitraceConstraint A) :
    IsClosed {f : A → ℂ | q.Holds f} := by
…
```
Mentions: OAI.Kaplansky.QuasitraceConstraint
abbrev OAI.Kaplansky.QuasitraceCandidate line 88
inductive OAI.Kaplansky.TwoQuasitraceConstraint line 92
Source documentation
Requirements on a function and its actual M₂ corner extension. The extension is deliberately not required to have unit value one.
```
inductive TwoQuasitraceConstraint where
…
```
def OAI.Kaplansky.TwoQuasitraceConstraint.Holds line 100
theorem OAI.Kaplansky.TwoQuasitraceConstraint.isClosed line 106
def OAI.Kaplansky.quasitraceCandidateBox line 118
Source documentation
Compact pointwise disks. The factor four for the extension follows from its unit value two, not an additional assumption.
```
def quasitraceCandidateBox (A : Type*) [CStarAlgebra A] : Set (QuasitraceCandidate A) :=
…
```
Mentions: OAI.Kaplansky.QuasitraceCandidate
theorem OAI.Kaplansky.mem_quasitraceCandidateBox line 123
theorem OAI.Kaplansky.isCompact_quasitraceCandidateBox line 128
theorem OAI.Kaplansky.quasitrace_pair_mem_box line 132
theorem OAI.Kaplansky.normalizedTwoQuasitrace_of_finite_constraints line 147
Source documentation
Compactness assembles all three whole-algebra axioms and the genuine matrix extension from bounded finite satisfiability. This is a conditional construction; finite satisfiability is not deduced from stable finiteness.
```
theorem normalizedTwoQuasitrace_of_finite_constraints
    (hf : ∀ qs : Finset (TwoQuasitraceConstraint A),
      ∃ f ∈ quasitraceCandidateBox A, ∀ q ∈ qs, q.Holds f) :
    ∃ τ : OneQuasitrace A, τ.Normalized ∧ τ.IsTwo := by
…
```
Mentions: OAI.Kaplansky.TwoQuasitraceConstraint, OAI.Kaplansky.quasitraceCandidateBox, OAI.Kaplansky.OneQuasitrace
theorem OAI.Kaplansky.normalizedTwoQuasitrace_iff_finite_constraints line 165
Source documentation
Exact equivalence: the bounded finite condition neither weakens the quasitrace axioms nor strengthens the required matrix normalization.
```
theorem normalizedTwoQuasitrace_iff_finite_constraints :
    (∃ τ : OneQuasitrace A, τ.Normalized ∧ τ.IsTwo) ↔
      ∀ qs : Finset (TwoQuasitraceConstraint A),
        ∃ f ∈ quasitraceCandidateBox A, ∀ q ∈ qs, q.Holds f := by
…
```
Mentions: OAI.Kaplansky.OneQuasitrace, OAI.Kaplansky.TwoQuasitraceConstraint, OAI.Kaplansky.quasitraceCandidateBox