CommonRankOneClosure.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Supported rank-one fields belong to the joint fiber bicommutant when the source generates the original central commutant.

theorem OAI.KadisonSimilarity.ae_common_projection_rankOne_mem line 24

Source documentation

Every compressed constant rank-one field lies almost everywhere in the fiber bicommutant. Its original operator is constructed by compression.

theorem ae_common_projection_rankOne_mem
    (σ : B →⋆ₐ[ℂ] (H →L[ℂ] H))
    (hgen : representationVonNeumannAlgebra σ = starSubalgebraCommutant π.range)
    (s : Set (WeakDual.characterSpace ℂ A)) (hs : MeasurableSet s)
    (hnull : (cyclicCommonBaseMeasure π D) sᶜ = 0)
    (ρ : ∀ _x : s, Unitization ℂ B →⋆ₐ[ℂ]
      (ScalarHilbertCoordinates D.generators →L[ℂ] ScalarHilbertCoordinates D.generators))
    (hρ : ∀ b : B, ∀ f : CommonCyclicHilbert π D,
      ∀ᵐ x : s ∂Measure.comap ((↑) : s → WeakDual.characterSpace ℂ A)
        (cyclicCommonBaseMeasure π D),
        isometricExtension (cyclicCommonEmbedding π D) (σ b) f x =
          ρ x (Unitization.inr b) (f x))
…

Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra, OAI.KadisonSimilarity.starSubalgebraCommutant, OAI.KadisonSimilarity.cyclicCommonBaseMeasure, OAI.KadisonSimilarity.ScalarHilbertCoordinates, OAI.KadisonSimilarity.CommonCyclicHilbert, OAI.KadisonSimilarity.isometricExtension, OAI.KadisonSimilarity.cyclicCommonEmbedding