Main.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Generator.relative_generation_of_II1_separable_predual line 21

Source documentation

Relative generation for the original concrete factors and the arbitrary given irreducible inclusion. No ambient separability, cyclicity, or perturbation hypothesis appears. The entire generating locus is Gδ and dense, for the metric identified with normalized trace-2 in FactorTraceUnitary.dist_eq_trace.

theorem relative_generation_of_II1_separable_predual
    (P S : StarSubalgebra ℂ (H →L[ℂ] H)) (hP : IsII1Factor P) (hS : IsII1Factor S)
    (hPS : P ≤ S)
    (hirr : ∀ c : S,
      (∀ a : P,StarSubalgebra.inclusion hPS a*c=c*StarSubalgebra.inclusion hPS a) →
      ∃ z : ℂ,c=algebraMap ℂ S z)
    (hsep : HasSeparablePredual S) :
    IsGδ {u : FactorTraceUnitary S hS |
      wstar ((P : Set (H →L[ℂ] H)) ∪ {(u.algebra S hS).val})=S} ∧
    Dense {u : FactorTraceUnitary S hS |
      wstar ((P : Set (H →L[ℂ] H)) ∪ {(u.algebra S hS).val})=S} := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.Generator.HasSeparablePredual, OAI.Generator.FactorTraceUnitary, OAI.Generator.wstar

theorem OAI.Generator.source_main_reused line 70
Source documentation
A factor with separable predual is singly generated, equivalently generated by two self-adjoint elements.
```
theorem source_main_reused (S : StarSubalgebra ℂ (H →L[ℂ] H))
    (hS : IsII1Factor S) (hsep : HasSeparablePredual S) :
    SinglyGenerated S ∧ ∃ a ∈ S, ∃ b ∈ S,
      IsSelfAdjoint a ∧ IsSelfAdjoint b ∧ wstar {a,b}=S := by
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.Generator.HasSeparablePredual, OAI.Generator.wstar

theorem OAI.RelativeGeneration.IsII1Factor.toGenerator line 84

Source documentation

The concrete finite diffuse factor hypotheses are the ones used in the trace construction.

theorem IsII1Factor.toGenerator {Hilbert : Type level} [NormedAddCommGroup Hilbert]
    [InnerProductSpace ℂ Hilbert] [CompleteSpace Hilbert]
    {algebra : StarSubalgebra ℂ (Hilbert →L[ℂ] Hilbert)} (factor : IsII1Factor algebra) :
    Generator.IsII1Factor algebra :=
…

Mentions: OAI.RelativeGeneration.IsII1Factor, OAI.Generator.IsII1Factor

theorem OAI.RelativeGeneration.main_theorem line 92
Source documentation
The entire relative-generator locus of an irreducible inclusion is dense Gδ in the normalized trace two-topology on the original, genuine unitaries.
Distinct definitions of this name: ComparatorChallenges/RelativeGeneration.lean:103 (same statement text; different proof or body). Qualify references as OAI.RelativeGeneration.main_theorem@path.
```
theorem main_theorem : MainTarget.{level} := by
…
```