OAI/Analysis/Commutator/DecomposableOperator.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Kadison.Decomposable.measurable_apply_simple line 20
  2. lemma OAI.Kadison.Decomposable.measurable_apply line 32
  3. lemma OAI.Kadison.Decomposable.memLp_apply line 42
  4. def OAI.Kadison.Decomposable.act line 50
  5. lemma OAI.Kadison.Decomposable.act_ae line 55
  6. lemma OAI.Kadison.Decomposable.act_add line 60
  7. lemma OAI.Kadison.Decomposable.act_smul line 71
  8. lemma OAI.Kadison.Decomposable.act_norm_le line 80
  9. def OAI.Kadison.Decomposable.operator line 89
  10. lemma OAI.Kadison.Decomposable.operator_ae line 97
  11. lemma OAI.Kadison.Decomposable.operator_norm_le line 102