OAI/Analysis/KadisonKastler/ConstructedFiniteFactorStability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Removing the common-subfactor restriction

First move a constructed injective subfactor into the neighbor, then apply common-position stability, and compose the two actual ambient unitaries.

  1. def OAI.KadisonKastler.constructedFiniteFactorError line 40

    Source documentation

    Displacement from the initial embedding and the proved finite-factor estimate.

    def constructedFiniteFactorError (t : ℝ) : ℝ :=
…
  2. theorem OAI.KadisonKastler.constructed_finiteFactor_spatial_of_injective_subfactor line 43