OriginalUnitary.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.Generator.factorVonNeumann line 18
theorem OAI.Generator.IsII1Factor.factor_smul line 22
theorem OAI.Generator.IsII1Factor.one_ne_zero line 30
def OAI.Generator.normalizedFactorTrace line 56
Source documentation
The constructed faithful normalized trace on the original factor.
```
def normalizedFactorTrace : S →L[ℂ] ℂ := traceFreeTrace hf hS.diffuse hS.finite hu
```
theorem OAI.Generator.normalizedFactorTrace_isNormalizedTrace line 59
Source documentation
The trace constructed from the factor hypotheses is faithful, normal, and normalized.
```
theorem normalizedFactorTrace_isNormalizedTrace :
    RelativeGeneration.IsNormalizedTrace S (normalizedFactorTrace S hS) := by
…
```
Mentions: OAI.RelativeGeneration.IsNormalizedTrace, OAI.Generator.normalizedFactorTrace
structure OAI.Generator.FactorTraceUnitary line 83
Source documentation
Same unitaries, with trace topology rather than the operator-norm topology.
```
structure FactorTraceUnitary (S : StarSubalgebra ℂ (H →L[ℂ] H)) (_hS : IsII1Factor S) where
…
```
Mentions: OAI.Generator.IsII1Factor
def OAI.Generator.FactorTraceUnitary.algebra line 88
def OAI.Generator.FactorTraceUnitary.unitaryEquiv line 91
Source documentation
Forgetting the metric wrapper preserves every genuine unitary of the original factor.
```
def unitaryEquiv : FactorTraceUnitary S hS ≃ unitary S where
…
```
Mentions: OAI.Generator.FactorTraceUnitary
def OAI.Generator.FactorTraceUnitary.represented line 97
def OAI.Generator.FactorTraceUnitary.representedEquiv line 100
instance OAI.Generator.FactorTraceUnitary.(instance at line 110) line 110
def OAI.Generator.FactorTraceUnitary.representedIsometryEquiv line 113
def OAI.Generator.FactorTraceUnitary.representedHomeomorph line 116
theorem OAI.Generator.FactorTraceUnitary.dist_eq_trace line 120
Source documentation
The metric is literally the normalized trace two-norm of the difference.
```
theorem dist_eq_trace (u v : FactorTraceUnitary S hS) :
    dist u v = Real.sqrt ((normalizedFactorTrace S hS)
      (star (u.algebra S hS-v.algebra S hS)*(u.algebra S hS-v.algebra S hS))).re := by
…
```
Mentions: OAI.Generator.FactorTraceUnitary, OAI.Generator.normalizedFactorTrace
def OAI.Generator.FactorTraceUnitary.traceHomeomorph line 130
Source documentation
The transported metric topology agrees with the trace-ball topology on genuine unitaries.
```
def traceHomeomorph :
    @Homeomorph (FactorTraceUnitary S hS) (unitary S) inferInstance
      (RelativeGeneration.traceTopology S (normalizedFactorTrace S hS)) :=
…
```
Mentions: OAI.Generator.FactorTraceUnitary, OAI.RelativeGeneration.traceTopology, OAI.Generator.normalizedFactorTrace

theorem OAI.Generator.FactorTraceUnitary.tendsto_iff line 137

Source documentation

Filter convergence, and hence the topology, is exactly normalized trace-2 convergence.

theorem tendsto_iff {I : Type*} (l : Filter I) (u : I → FactorTraceUnitary S hS)
    (v : FactorTraceUnitary S hS) :
    Filter.Tendsto u l (𝓝 v) ↔ Filter.Tendsto (fun i => Real.sqrt
      ((normalizedFactorTrace S hS)
        (star ((u i).algebra S hS-v.algebra S hS)*((u i).algebra S hS-v.algebra S hS))).re)
      l (𝓝 0) := by
…

Mentions: OAI.Generator.FactorTraceUnitary, OAI.Generator.normalizedFactorTrace, OAI.Generator.FactorTraceUnitary.algebra