AERepresentationAgreement.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Agreement of the reconstructed fiber representations

For each fixed algebra element, the genuine representations reconstructed from a countable dense subring agree almost everywhere with the original operator representatives. Only countably many approximants are used for that element; no uncountable intersection of conull sets is taken.

theorem OAI.KadisonSimilarity.ae_starRepresentation_agrees_at line 28

Source documentation

Every extension of the dense-subring representatives has the correct value at a fixed a, outside a null set that may depend on a.

theorem ae_starRepresentation_agrees_at
    (S : Subring A) (hdense : Dense (S : Set A))
    (f : ∀ _a : A, ∀ x, K x →L[ℂ] K x)
    (hsub : ∀ a b : A, ∀ᵐ x ∂μ, f (a - b) x = f a x - f b x)
    (hnorm : ∀ a : A, ∀ᵐ x ∂μ, ‖f a x‖ ≤ ‖a‖) (a : A) :
    ∀ᵐ x ∂μ, ∀ σ : A →⋆ₐ[ℂ] (K x →L[ℂ] K x),
      (∀ b : S, σ b = f b x) → σ a = f a x := by
…

theorem OAI.KadisonSimilarity.exists_dense_subring_ae_fiber_representations line 61

Source documentation

Countably many fiber relations suffice for genuine representations, and their values agree almost everywhere with every fixed original section. The statement leaves exceptional fibers unspecified.

theorem exists_dense_subring_ae_fiber_representations
    [TopologicalSpace.SeparableSpace A]
    (f : ∀ _a : A, ∀ x, K x →L[ℂ] K x)
    (hzero : ∀ᵐ x ∂μ, f 0 x = 0)
    (hone : ∀ᵐ x ∂μ, f 1 x = 1)
    (hadd : ∀ a b : A, ∀ᵐ x ∂μ, f (a + b) x = f a x + f b x)
    (hmul : ∀ a b : A, ∀ᵐ x ∂μ, f (a * b) x = f a x * f b x)
    (hnorm : ∀ a : A, ∀ᵐ x ∂μ, ‖f a x‖ ≤ ‖a‖)
    (hstar : ∀ a : A, ∀ᵐ x ∂μ, f (star a) x = star (f a x))
    (hI : ∀ᵐ x ∂μ, f (algebraMap ℂ A Complex.I) x =
      algebraMap ℂ (K x →L[ℂ] K x) Complex.I) :
    ∃ S : Subring A, Countable S ∧ Dense (S : Set A) ∧
…