OAI/Analysis/KadisonKastler/WeakFieldPullback.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Nonsingular pullback of weak operator fields

Composition preserves the measurable representatives and their uniform bound. Nonsingularity makes the construction independent of representatives.

  1. theorem OAI.KadisonKastler.WeakOperatorRepresentative.eq_of_eval line 24
  2. def OAI.KadisonKastler.WeakOperatorRepresentative.pullback line 32

    Source documentation

    Pullback of bounded measurable representatives by a nonsingular map.

    def pullback (T : D → D) (hT : Measure.QuasiMeasurePreserving T μ μ) :
    WeakOperatorRepresentative (H := H) μ →⋆ₐ[ℂ]
…

    Mentions: OAI.KadisonKastler.WeakOperatorRepresentative

  3. theorem OAI.KadisonKastler.WeakOperatorRepresentative.eval_pullback line 46
  4. theorem OAI.KadisonKastler.WeakOperatorRepresentative.norm_pullback_le line 50
  5. theorem OAI.KadisonKastler.WeakOperatorRepresentative.pullback_congr_ae line 55
  6. theorem OAI.KadisonKastler.WeakOperatorRepresentative.pullback_constant line 61
  7. theorem OAI.KadisonKastler.WeakOperatorRepresentative.pullback_id line 69
  8. theorem OAI.KadisonKastler.WeakOperatorRepresentative.pullback_comp line 75
  9. def OAI.KadisonKastler.WeakOperatorField.pullbackValue line 88
  10. theorem OAI.KadisonKastler.WeakOperatorField.pullbackValue_quotient line 92
  11. theorem OAI.KadisonKastler.WeakOperatorField.pullbackValue_one line 101
  12. theorem OAI.KadisonKastler.WeakOperatorField.pullbackValue_mul line 111
  13. theorem OAI.KadisonKastler.WeakOperatorField.pullbackValue_zero line 118
  14. theorem OAI.KadisonKastler.WeakOperatorField.pullbackValue_add line 128
  15. theorem OAI.KadisonKastler.WeakOperatorField.pullbackValue_algebraMap line 135
  16. theorem OAI.KadisonKastler.WeakOperatorField.pullbackValue_star line 153
  17. def OAI.KadisonKastler.WeakOperatorField.pullback line 161

    Source documentation

    Nonsingular pullback is a unital star-algebra homomorphism of the actual almost-everywhere quotient.

    def pullback (T : D → D) (hT : Measure.QuasiMeasurePreserving T μ μ) :
    WeakOperatorField (H := H) μ →⋆ₐ[ℂ] WeakOperatorField (H := H) μ where
…

    Mentions: OAI.KadisonKastler.WeakOperatorField

  18. theorem OAI.KadisonKastler.WeakOperatorField.pullback_quotient line 171
  19. theorem OAI.KadisonKastler.WeakOperatorField.norm_pullback_le line 177
  20. theorem OAI.KadisonKastler.WeakOperatorField.pullback_constant line 183
  21. theorem OAI.KadisonKastler.WeakOperatorField.pullback_id line 190
  22. theorem OAI.KadisonKastler.WeakOperatorField.pullback_comp line 195
  23. theorem OAI.KadisonKastler.WeakOperatorField.coefficient_pullback line 207

    Source documentation

    Pulling back an operator field pulls back every scalar coefficient.

    theorem coefficient_pullback (T : D → D) (hT : Measure.QuasiMeasurePreserving T μ μ)
    (q : WeakOperatorField (H := H) μ) (ξ η : H) :
…

    Mentions: OAI.KadisonKastler.WeakOperatorField