PolishConjugacyRelation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The Borel implementer relation on the Polish unitary model

Measurable evaluation of the countable contraction fields suffices. No measurability in the operator norm topology is imposed.

instance OAI.KadisonKastler.strongUnitarySpaceMeasurable line 23
instance OAI.KadisonKastler.strongUnitarySpaceBorel line 26
theorem OAI.KadisonKastler.measurable_operator_field_apply line 29
theorem OAI.KadisonKastler.measurable_conjugation_on_strongUnitarySpace line 36
theorem OAI.KadisonKastler.measurable_star_conjugation_on_strongUnitarySpace line 53

theorem OAI.KadisonKastler.measurableSet_bounded_implementer_relation line 74

Source documentation

This relation has precisely the algebra-conjugacy and displacement conditions required by the measurable selection step.

theorem measurableSet_bounded_implementer_relation
    (M N : X → VonNeumannAlgebra H)
    (A : ∀ p, StrongUnitBallTestSequence (M p)) (B : ∀ p, StrongUnitBallTestSequence (N p))
    (hA : ∀ j x, Measurable (fun p => (A p).op j x))
    (hB : ∀ j x, Measurable (fun p => (B p).op j x))
    (ξ : ℕ → H) (hξ : DenseRange ξ) {a : ℝ} (ha : 0 ≤ a) :
    MeasurableSet {p : X × StrongUnitarySpace ξ |
      Conjugates (decodeStrongUnitary ξ p.2) (M p.1) (N p.1) ∧
      ‖(decodeStrongUnitary ξ p.2 : H →L[ℂ] H) - 1‖ ≤ a} := by
…

Mentions: OAI.KadisonKastler.StrongUnitBallTestSequence, OAI.KadisonKastler.StrongUnitarySpace, OAI.KadisonKastler.Conjugates, OAI.KadisonKastler.decodeStrongUnitary