OAI/Analysis/Commutator/PointwiseLinearLift.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.PointwiseLift.Good line 26
  2. lemma OAI.Kadison.PointwiseLift.good_ae line 32
  3. def OAI.Kadison.PointwiseLift.raw line 46
  4. def OAI.Kadison.PointwiseLift.rationalField line 51
  5. lemma OAI.Kadison.PointwiseLift.rationalField_subtype line 55
  6. lemma OAI.Kadison.PointwiseLift.rationalField_norm_le line 61
  7. lemma OAI.Kadison.PointwiseLift.rationalField_ae line 73
  8. lemma OAI.Kadison.PointwiseLift.rationalField_measurable line 90
  9. def OAI.Kadison.PointwiseLift.realField line 95
  10. lemma OAI.Kadison.PointwiseLift.realField_norm_le line 98
  11. def OAI.Kadison.PointwiseLift.field line 104
  12. lemma OAI.Kadison.PointwiseLift.field_norm_le line 106
  13. lemma OAI.Kadison.PointwiseLift.field_ae line 109
  14. lemma OAI.Kadison.PointwiseLift.field_measurable line 120