OAI/Analysis/Commutator/HilbertSequenceOperator.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Kadison.HilbertSequence.point_action_bound line 24
  2. def OAI.Kadison.HilbertSequence.actPreLinear line 29
  3. lemma OAI.Kadison.HilbertSequence.actPreLinear_seq line 48
  4. lemma OAI.Kadison.HilbertSequence.norm_actPreLinear_le line 51
  5. def OAI.Kadison.HilbertSequence.actPre line 57
  6. def OAI.Kadison.HilbertSequence.act line 60
  7. lemma OAI.Kadison.HilbertSequence.act_coe line 63
  8. lemma OAI.Kadison.HilbertSequence.norm_act_apply_le line 67
  9. lemma OAI.Kadison.HilbertSequence.norm_act_le line 73
  10. lemma OAI.Kadison.HilbertSequence.act_eq_of_coe line 76
  11. lemma OAI.Kadison.HilbertSequence.act_add line 83
  12. lemma OAI.Kadison.HilbertSequence.act_smul line 89
  13. lemma OAI.Kadison.HilbertSequence.act_constant line 95
  14. lemma OAI.Kadison.HilbertSequence.norm_act_constant line 100
  15. lemma OAI.Kadison.HilbertSequence.act_zero line 109
  16. lemma OAI.Kadison.HilbertSequence.act_mul line 115
  17. lemma OAI.Kadison.HilbertSequence.act_one line 121
  18. lemma OAI.Kadison.HilbertSequence.act_star line 129
  19. def OAI.Kadison.HilbertSequence.actionHom line 144