AEStarRepresentation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A common conull set for fiber representations

Countability of the dense subring lets all algebraic identities and norm bounds hold on a single conull set. Each of those fibers then has the genuine complex star representation constructed in DenseStarRepresentation. Exceptional fibers are left out of the existence assertion.

theorem OAI.KadisonSimilarity.ae_exists_starRepresentation_of_countable_subring line 26

Source documentation

Pointwise representatives on a countable dense star subring extend to complex star representations almost everywhere. Each input identity is required only almost everywhere for its fixed tuple of arguments.

theorem ae_exists_starRepresentation_of_countable_subring
    (S : Subring A) [Countable S] (hdense : Dense (S : Set A))
    (hstarS : ∀ a ∈ S, star a ∈ S) (hIS : algebraMap ℂ A Complex.I ∈ S)
    (f : ∀ _a : S, ∀ x, K x →L[ℂ] K x)
    (hzero : ∀ᵐ x ∂μ, f 0 x = 0)
    (hone : ∀ᵐ x ∂μ, f 1 x = 1)
    (hadd : ∀ a b : S, ∀ᵐ x ∂μ, f (a + b) x = f a x + f b x)
    (hmul : ∀ a b : S, ∀ᵐ x ∂μ, f (a * b) x = f a x * f b x)
    (hnorm : ∀ a : S, ∀ᵐ x ∂μ, ‖f a x‖ ≤ ‖a‖)
    (hstar : ∀ a : S, ∀ᵐ x ∂μ,
      f ⟨star a.val, hstarS a.val a.property⟩ x = star (f a x))
    (hI : ∀ᵐ x ∂μ, f ⟨algebraMap ℂ A Complex.I, hIS⟩ x =
…