CommonFiberFactors.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The common joint source gives factor fibers for the first algebra, using countably many compressed constant rank-one tests.

theorem OAI.KadisonSimilarity.ae_common_fiber_scalar_center line 25

Source documentation

The first source's genuine range fibers have scalar center almost everywhere when the joint source generates the central commutant.

theorem ae_common_fiber_scalar_center
    (B C : StarSubalgebra ℂ (H →L[ℂ] H))
    [IsClosed (B : Set (H →L[ℂ] H))] [IsClosed (C : Set (H →L[ℂ] H))]
    (hBC : ∀ b : B, ∀ c : C, (b : H →L[ℂ] H) * (c : H →L[ℂ] H) =
      (c : H →L[ℂ] H) * (b : H →L[ℂ] H))
    (hgen : representationVonNeumannAlgebra (jointCStarSource B C).subtype =
      starSubalgebraCommutant π.range)
    (s : Set (WeakDual.characterSpace ℂ A)) (hs : MeasurableSet s)
    (hnull : (cyclicCommonBaseMeasure π D) sᶜ = 0)
    (ρ : ∀ _x : s, Unitization ℂ (jointCStarSource B C) →⋆ₐ[ℂ]
      (ScalarHilbertCoordinates D.generators →L[ℂ] ScalarHilbertCoordinates D.generators))
    (hρ : ∀ b : jointCStarSource B C, ∀ f : CommonCyclicHilbert π D,
…

Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.jointCStarSource, OAI.KadisonSimilarity.starSubalgebraCommutant, OAI.KadisonSimilarity.cyclicCommonBaseMeasure, OAI.KadisonSimilarity.ScalarHilbertCoordinates, OAI.KadisonSimilarity.CommonCyclicHilbert