OAI/Analysis/KadisonKastler/WeakFieldCoefficients.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic scalar coefficients of weak operator fields

  1. def OAI.KadisonKastler.WeakOperatorField.representative line 20

    Source documentation

    A representative with exactly the quotient norm bound.

    def representative (T : WeakOperatorField (H := H) μ) : WeakOperatorRepresentative (H := H) μ :=
…

    Mentions: OAI.KadisonKastler.WeakOperatorField, OAI.KadisonKastler.WeakOperatorRepresentative

  2. theorem OAI.KadisonKastler.WeakOperatorField.quotient_representative line 23
  3. theorem OAI.KadisonKastler.WeakOperatorField.norm_representative_le line 27
  4. def OAI.KadisonKastler.WeakOperatorField.coefficient line 32

    Source documentation

    Matrix coefficients depend only on the almost-everywhere operator class.

    def coefficient (T : WeakOperatorField (H := H) μ) (ξ η : H) : ScalarLInfinity μ :=
…

    Mentions: OAI.KadisonKastler.WeakOperatorField, OAI.KadisonKastler.ScalarLInfinity

  5. theorem OAI.KadisonKastler.WeakOperatorField.coefficient_quotient line 35
  6. theorem OAI.KadisonKastler.WeakOperatorField.norm_coefficient_le line 42
  7. theorem OAI.KadisonKastler.WeakOperatorField.ext_coeff line 52

    Source documentation

    Intrinsic scalar coefficients separate the quotient.

    theorem ext_coeff {T S : WeakOperatorField (H := H) μ}
…

    Mentions: OAI.KadisonKastler.WeakOperatorField

  8. theorem OAI.KadisonKastler.WeakOperatorField.coefficient_add line 59
  9. theorem OAI.KadisonKastler.WeakOperatorField.coefficient_smul line 74