MeasurableConullRepresentations.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Measurable representatives of a separable operator-algebra field

A single measurable conull set suffices for every algebra element and vector. Countably many dense tests are made measurable there; continuity supplies the remaining evaluations without any uncountable intersection of conull sets.

theorem OAI.KadisonKastler.measurable_of_dense_parameters line 24

theorem OAI.KadisonKastler.exists_conull_measurable_representations line 45

Source documentation

An a.e. measurable representation field is strongly Borel measurable on a single measurable conull subset, simultaneously for all evaluations.

theorem exists_conull_measurable_representations (μ : Measure X)
    (ρ : X → A →⋆ₙₐ[ℂ] (H →L[ℂ] H))
    (hρ : ∀ a v, AEStronglyMeasurable (fun x => ρ x a v) μ) :
    ∃ s : Set X, MeasurableSet s ∧ μ sᶜ = 0 ∧
      ∀ a v, Measurable fun x : s => ρ x.val a v := by
…

theorem OAI.KadisonKastler.exists_measurable_nonunitalRepresentation_version line 75

Source documentation

Extend the common conull restriction by the zero representation. This preserves every fixed algebra element almost everywhere and is Borel everywhere.

theorem exists_measurable_nonunitalRepresentation_version (μ : Measure X)
    (ρ : X → A →⋆ₙₐ[ℂ] (H →L[ℂ] H))
    (hρ : ∀ a v, AEStronglyMeasurable (fun x => ρ x a v) μ) :
    ∃ σ : X → A →⋆ₙₐ[ℂ] (H →L[ℂ] H),
      (∀ a v, Measurable fun x => σ x a v) ∧
      ∀ a, ∀ᵐ x ∂μ, σ x a = ρ x a := by
…