Topology.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.RelativeGeneration.WOTClosed line 15
Source documentation
Weak operator closedness of a concrete unital star subalgebra.
Also declared: ComparatorChallenges/RelativeGeneration.lean:15 (same declaration text).
```
def WOTClosed (algebra : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert)) : Prop :=
…
```
def OAI.RelativeGeneration.wstar line 19
Source documentation
The weakly closed unital star algebra generated by a set of operators.
Also declared: ComparatorChallenges/RelativeGeneration.lean:19 (same declaration text).
```
def wstar (operators : Set (Hilbert →L[ℂ] Hilbert)) :
    StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert) :=
…
```
structure OAI.RelativeGeneration.IsII1Factor line 24
Source documentation
A nonzero, weakly closed, finite diffuse algebra with scalar center.
Also declared: ComparatorChallenges/RelativeGeneration.lean:24 (same declaration text).
```
structure IsII1Factor (algebra : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert)) : Prop where
…
```
def OAI.RelativeGeneration.HasSeparablePredual line 37
Source documentation
A same-universe separable Banach predual, with the conjugate-linear dual convention. This imposes no separability on the Hilbert representation or the operator norm topology.
Also declared: ComparatorChallenges/RelativeGeneration.lean:37 (same declaration text).
```
def HasSeparablePredual (algebra : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert)) : Prop :=
…
```
abbrev OAI.RelativeGeneration.ultraweakTopology line 43
Source documentation
The ultraweak topology is generated by absolutely summable vector functionals.
Also declared: ComparatorChallenges/RelativeGeneration.lean:43 (same declaration text).
```
abbrev ultraweakTopology (Hilbert : Type level) [NormedAddCommGroup Hilbert]
    [InnerProductSpace ℂ Hilbert] [CompleteSpace Hilbert] :
    TopologicalSpace (Hilbert →L[ℂ] Hilbert) :=
…
```
abbrev OAI.RelativeGeneration.algebraUltraweakTopology line 53
Source documentation
The concrete algebra carries the induced ultraweak topology.
Also declared: ComparatorChallenges/RelativeGeneration.lean:53 (same declaration text).
```
abbrev algebraUltraweakTopology (algebra : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert)) :
    TopologicalSpace algebra :=
…
```
structure OAI.RelativeGeneration.IsNormalizedTrace line 59
Source documentation
A faithful normal normalized trace, not an additional hypothesis on the inclusion.
Also declared: ComparatorChallenges/RelativeGeneration.lean:59 (same declaration text).
```
structure IsNormalizedTrace (algebra : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert))
    (trace : algebra →L[ℂ] ℂ) : Prop where
…
```
def OAI.RelativeGeneration.traceDistance line 69
Source documentation
The normalized trace two-distance between genuine unitaries of the original algebra.
Also declared: ComparatorChallenges/RelativeGeneration.lean:69 (same declaration text).
```
def traceDistance (algebra : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert))
    (trace : algebra →L[ℂ] ℂ) (left right : unitary algebra) : ℝ :=
…
```
abbrev OAI.RelativeGeneration.traceTopology line 75
Source documentation
The topology generated by trace two-distance balls, not the inherited operator norm topology.
Also declared: ComparatorChallenges/RelativeGeneration.lean:75 (same declaration text).
```
abbrev traceTopology (algebra : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert))
    (trace : algebra →L[ℂ] ℂ) : TopologicalSpace (unitary algebra) :=
…
```

def OAI.RelativeGeneration.traceUnitaryHomeomorph line 82

Source documentation

A metric presentation with the trace two-distance gives precisely the trace-ball topology on all genuine unitaries.

def traceUnitaryHomeomorph (algebra : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert))
    (trace : algebra →L[ℂ] ℂ) {UnitarySpace : Type*} [MetricSpace UnitarySpace]
    (unitaryEquiv : UnitarySpace ≃ unitary algebra)
    (distance_eq : ∀ first second, dist first second =
      traceDistance algebra trace (unitaryEquiv first) (unitaryEquiv second)) :
    @Homeomorph UnitarySpace (unitary algebra) inferInstance (traceTopology algebra trace) := by
…

Mentions: OAI.RelativeGeneration.traceDistance, OAI.RelativeGeneration.traceTopology

def OAI.RelativeGeneration.relativeGeneratorLocus line 125
Source documentation
The entire relative-generator locus in the original unitary group.
Also declared: ComparatorChallenges/RelativeGeneration.lean:81 (same declaration text).
```
def relativeGeneratorLocus (small large : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert)) :
    Set (unitary large) :=
…
```
def OAI.RelativeGeneration.MainTarget line 134
Source documentation
Every irreducible inclusion of concrete type II₁ factors with separable predual of the larger factor has a dense Gδ full relative-generator locus in the normalized trace two-topology. The normalized faithful normal trace is asserted to exist; no representation, transport, cyclicity, or perturbation premise is imposed.
Also declared: ComparatorChallenges/RelativeGeneration.lean:90 (same declaration text).
```
def MainTarget : Prop :=
…
```