ConullStarRepresentations.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Genuine fiber representations on a measurable conull base

Restricting to a measurable conull set allows the almost-everywhere representation theorem to be used as an actual family of representations. The original section for each fixed algebra element remains unchanged almost everywhere after this restriction.

theorem OAI.KadisonSimilarity.exists_conull_starRepresentations line 25

Source documentation

Choose genuine representations on a measurable conull set, retaining the prescribed representatives almost everywhere for each fixed element.

theorem exists_conull_starRepresentations
    (S : Subring A) (f : ∀ _a : A, ∀ x, K x →L[ℂ] K x)
    (hexists : ∀ᵐ x ∂μ, ∃ σ : A →⋆ₐ[ℂ] (K x →L[ℂ] K x),
      ∀ b : S, σ b = f b x)
    (hagrees : ∀ a : A, ∀ᵐ x ∂μ, ∀ σ : A →⋆ₐ[ℂ] (K x →L[ℂ] K x),
      (∀ b : S, σ b = f b x) → σ a = f a x) :
    ∃ s : Set Ω, MeasurableSet s ∧ μ sᶜ = 0 ∧
      ∃ σ : ∀ x : s, A →⋆ₐ[ℂ] (K x →L[ℂ] K x),
        ∀ a : A, ∀ᵐ x ∂Measure.comap ((↑) : s → Ω) μ, σ x a = f a x := by
…