OAI/Analysis/FactorGeneration/Main.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Single generation of a finite diffuse factor with a separable Banach predual, using its faithful normal trace and given-predual continuity.

  1. theorem OAI.Generator.single_generation_of_II1_separable_predual line 15

    Distinct definitions of this name: ComparatorChallenges/FactorGeneration.lean:41 (same statement text; different proof or body). Qualify references as OAI.Generator.single_generation_of_II1_separable_predual@path.

  2. theorem OAI.Generator.mainTarget line 40