Target.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Weak operator generation of concrete finite diffuse factors with separable Banach preduals.

def OAI.Generator.WOTClosed line 14
Source documentation
Weak operator closedness, not operator norm closedness.
Also declared: ComparatorChallenges/FactorGeneration.lean:17 (same declaration text).
```
def WOTClosed (S : StarSubalgebra ℂ (H →L[ℂ] H)) : Prop :=
…
```
def OAI.Generator.wstar line 19
Source documentation
The manuscript's W*(s), as the intersection of all weakly closed unital star subalgebras containing s. This does not invoke a double-commutant theorem.
Also declared: ComparatorChallenges/FactorGeneration.lean:20 (same declaration text).
```
def wstar (s : Set (H →L[ℂ] H)) : StarSubalgebra ℂ (H →L[ℂ] H) :=
…
```
theorem OAI.Generator.subset_wstar line 22
theorem OAI.Generator.wstar_le line 26
theorem OAI.Generator.wstar_mono line 30
theorem OAI.Generator.wstar_closed line 36
theorem OAI.Generator.wstar_eq line 46
theorem OAI.Generator.wstar_idempotent line 50
structure OAI.Generator.IsII1Factor line 56
Source documentation
A nonzero finite diffuse factor, stated by its center, isometries, and projections. These hypotheses do not include any generation conclusion.
Also declared: ComparatorChallenges/FactorGeneration.lean:23 (same declaration text).
```
structure IsII1Factor (S : StarSubalgebra ℂ (H →L[ℂ] H)) : Prop where
…
```
def OAI.Generator.HasSeparablePredual line 66
Source documentation
Separable Banach predual, matching the existential predual convention of mathlib's WStarAlgebra. This is not norm separability of S.
Also declared: ComparatorChallenges/FactorGeneration.lean:31 (same declaration text).
```
def HasSeparablePredual (S : StarSubalgebra ℂ (H →L[ℂ] H)) : Prop :=
…
```
def OAI.Generator.SinglyGenerated line 72
Source documentation
Generation of the same algebra by one of its bounded operators.
Distinct definitions of this name: ComparatorChallenges/FactorGeneration.lean:36 (same statement text; different proof or body). Qualify references as OAI.Generator.SinglyGenerated@path.
```
def SinglyGenerated (S : StarSubalgebra ℂ (H →L[ℂ] H)) : Prop :=
…
```
def OAI.Generator.MainTarget line 76
Source documentation
The single-generation proposition for nonzero finite diffuse factors with separable Banach preduals.
```
def MainTarget : Prop :=
…
```