OAI/Analysis/RelativeGeneration/RepresentedLocus.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Generator.Tracial.represented_full_relative_generation line 17

   Source documentation

   Full represented theorem: the previously proved residual subset is reused only for density.

   theorem represented_full_relative_generation
       (hfactor : ∀ c : N.toStarSubalgebra,
         (∀ a : N.toStarSubalgebra, a*c=c*a) → ∃ z : ℂ,c=z • (1 : N.toStarSubalgebra))
       (hdiff : ∀ r : N.toStarSubalgebra, IsStarProjection r → r ≠ 0 →
         ∃ q : N.toStarSubalgebra, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ r ∧ r*q=q ∧ q*r=q)
       (hirr : ∀ c : M.toStarSubalgebra,
         (∀ a : N.toStarSubalgebra, coordinateInclusion hNM a*c=c*coordinateInclusion hNM a) →
         ∃ z : ℂ,c=z • (1 : M.toStarSubalgebra))
       (hsep : TopologicalSpace.IsSeparable (Set.range (baseVector τ))) :
       IsGδ {u : TraceUnitary τ |
         wstar ((N : Set (H →L[ℂ] H)) ∪ {(u.algebra τ).val}) = M.toStarSubalgebra} ∧
       Dense {u : TraceUnitary τ |
   …

   Mentions: OAI.Generator.Tracial.coordinateInclusion, OAI.Generator.Tracial.baseVector, OAI.Generator.Tracial.TraceUnitary, OAI.Generator.wstar