Ultrapower.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

Commutation with every bounded subalgebra sequence implies uniform coordinate commutator decay.

theorem OAI.UltrapowerBridge.operator_norm_one_le line 20
def OAI.UltrapowerBridge.boundedSequences line 24
Source documentation
Operator-norm bounded sequences, as an actual star subalgebra of pointwise sequences.
```
def boundedSequences (M : VonNeumannAlgebra H) : StarSubalgebra ℂ (ℕ → M.toStarSubalgebra) where
…
```
abbrev OAI.UltrapowerBridge.Bounded line 47
def OAI.UltrapowerBridge.TraceRel line 51
Source documentation
The trace-null equivalence relation, before descending algebra operations.
```
def TraceRel (a b : Bounded M) : Prop :=
…
```
Mentions: OAI.UltrapowerBridge.Bounded
theorem OAI.UltrapowerBridge.traceRel_refl line 54
theorem OAI.UltrapowerBridge.traceRel_symm line 58
theorem OAI.UltrapowerBridge.traceRel_trans line 61
theorem OAI.UltrapowerBridge.traceRel_add line 69
theorem OAI.UltrapowerBridge.traceRel_mul line 79
theorem OAI.UltrapowerBridge.traceRel_star line 93
def OAI.UltrapowerBridge.traceCongruence line 99
Source documentation
Algebra congruence proved from actual trace-norm estimates.
```
def traceCongruence : RingCon (Bounded M) where
…
```
Mentions: OAI.UltrapowerBridge.Bounded
abbrev OAI.UltrapowerBridge.TracialQuotient line 106
Source documentation
Underlying ring of the tracial ultrapower when l is a free ultrafilter.
```
abbrev TracialQuotient := (traceCongruence τ l).Quotient
```
Mentions: OAI.UltrapowerBridge.traceCongruence
def OAI.UltrapowerBridge.quotientMap line 108
theorem OAI.UltrapowerBridge.quotientMap_eq_iff line 117
theorem OAI.UltrapowerBridge.quotientMap_surjective line 120
instance OAI.UltrapowerBridge.(instance at line 122) line 122
theorem OAI.UltrapowerBridge.quotientMap_star line 125
instance OAI.UltrapowerBridge.(instance at line 128) line 128
theorem OAI.UltrapowerBridge.quotientMap_smul line 139
instance OAI.UltrapowerBridge.(instance at line 142) line 142
def OAI.UltrapowerBridge.quotientStarAlgHom line 146
theorem OAI.UltrapowerBridge.TracialRepresentation.trace_sub line 158
theorem OAI.UltrapowerBridge.TracialRepresentation.trace_add line 161
theorem OAI.UltrapowerBridge.TracialRepresentation.trace_smul line 164
def OAI.UltrapowerBridge.traceRep line 167
theorem OAI.UltrapowerBridge.traceRep_tendsto line 169
theorem OAI.UltrapowerBridge.traceRep_eq_of_rel line 181
def OAI.UltrapowerBridge.quotientTrace line 192
Source documentation
The actual ultralimit trace on the operator-algebra quotient.
```
def quotientTrace : TracialQuotient τ (ω : Filter ℕ) → ℂ :=
…
```
Mentions: OAI.UltrapowerBridge.TracialQuotient
theorem OAI.UltrapowerBridge.quotientTrace_mk line 195
theorem OAI.UltrapowerBridge.quotientTrace_one line 198
theorem OAI.UltrapowerBridge.quotientTrace_mul_comm line 202
theorem OAI.Generator.Tracial.unitary_norm_le line 226
Source documentation
Unitary norm bound without requiring a separate nontriviality instance.
```
theorem unitary_norm_le (w : M.toStarSubalgebra) (hw : star w*w = 1) : ‖w‖ ≤ 1 := by
…
```

theorem OAI.Generator.Tracial.uniform_commutator_decay line 234

Source documentation

A quotient commutant condition controls all coordinate unitaries uniformly. The filter need not be ultra for this diagonal-selection step.

theorem uniform_commutator_decay
    (P : StarSubalgebra ℂ M.toStarSubalgebra) (b : Bounded M)
    (hcomm : ∀ w : Bounded M, (∀ n, w.val n ∈ P) →
      quotientMap τ l w * quotientMap τ l b = quotientMap τ l b * quotientMap τ l w)
    (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ n in l, ∀ w : M.toStarSubalgebra, w ∈ P → star w*w = 1 → w*star w = 1 →
      τ.norm₂ (w*b.val n-b.val n*w) < ε := by
…