OAI/Analysis/KadisonKastler/DecomposableNorm.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Norm bounds for concrete decomposable fields

Uniqueness on finite-measure indicator tests transfers the norm bound in the published diagonal decomposition to any representing field. Applying this to a difference avoids a measurable nearest-point choice.

  1. theorem OAI.KadisonKastler.RepresentsOperatorField.ae_norm_le_of_diagonal line 23
  2. theorem OAI.KadisonKastler.RepresentsOperatorField.sub_real line 36
  3. theorem OAI.KadisonKastler.RepresentsOperatorField.ae_norm_sub_le_of_diagonal line 49

    Source documentation

    The operator-norm distance of two decomposable operators bounds the essential uniform distance of their representing fields.

    theorem RepresentsOperatorField.ae_norm_sub_le_of_diagonal
    (hSpectral : PublishedRealSpectralCommutant.{u})
    (hDiagonal : PublishedRealDiagonalDecomposition.{u})
    {F G : ℝ → H →L[ℂ] H}
    {T S : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H}
    (hF : RepresentsOperatorField volume F T) (hG : RepresentsOperatorField volume G S)
    (hT : ∀ a : ℝ, Commute T (regularCharacterUnitary (H := H) a :
…

    Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.RepresentsOperatorField, OAI.KadisonKastler.regularCharacterUnitary