OAI/Analysis/BoundedHochschild/NormalOperators.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Normal parts of scalar functionals and bounded operators.

  1. def OAI.HochschildNormalPart.positiveVector line 35
  2. lemma OAI.HochschildNormalPart.positiveVector_coefficient line 37
  3. lemma OAI.HochschildNormalPart.positiveVector_norm_sq line 43
  4. abbrev OAI.HochschildNormalPart.FourHilbert line 51
  5. def OAI.HochschildNormalPart.fourRepresentation line 55
  6. def OAI.HochschildNormalPart.fourLeft line 60
  7. def OAI.HochschildNormalPart.fourRight line 64
  8. lemma OAI.HochschildNormalPart.four_coefficient line 68
  9. lemma OAI.HochschildNormalPart.four_norm_bound line 77
  10. structure OAI.HochschildNormalPart.FunctionalModel line 91
  11. lemma OAI.HochschildNormalPart.functionalModel_nonempty line 103
  12. def OAI.HochschildNormalPart.functionalModel line 124
  13. def OAI.HochschildNormalPart.normalPartRaw line 130
  14. lemma OAI.HochschildNormalPart.normalPartRaw_coefficient line 136
  15. lemma OAI.HochschildNormalPart.normalPartRaw_add line 140
  16. lemma OAI.HochschildNormalPart.normalPartRaw_smul line 155
  17. lemma OAI.HochschildNormalPart.normalPartRaw_norm line 163
  18. def OAI.HochschildNormalPart.scalarNormalPart line 171
  19. lemma OAI.HochschildNormalPart.scalarNormalPart_coefficient line 177
  20. lemma OAI.HochschildNormalPart.scalarNormalPart_norm line 181
  21. lemma OAI.HochschildNormalPart.scalarNormalPart_mem line 184
  22. lemma OAI.HochschildNormalPart.scalarNormalPart_fixes line 188
  23. lemma OAI.HochschildNormalPart.scalarNormalPart_comp_left line 194
  24. lemma OAI.HochschildNormalPart.scalarNormalPart_comp_right line 206
  25. lemma OAI.HochschildNormalPart.predual_separates line 229
  26. def OAI.HochschildNormalPart.normalPredualVector line 235
  27. lemma OAI.HochschildNormalPart.normalPredualVector_spec line 238
  28. lemma OAI.HochschildNormalPart.normalPredualVector_add line 245
  29. lemma OAI.HochschildNormalPart.normalPredualVector_smul line 250
  30. lemma OAI.HochschildNormalPart.normalPredualVector_norm line 255
  31. def OAI.HochschildNormalPart.normalPreadjoint line 263
  32. def OAI.HochschildNormalPart.normalOperator line 269
  33. lemma OAI.HochschildNormalPart.normalOperator_pairing line 274
  34. lemma OAI.HochschildNormalPart.normalOperator_normal line 280
  35. lemma OAI.HochschildNormalPart.normalOperator_add line 286
  36. lemma OAI.HochschildNormalPart.normalOperator_smul line 292
  37. lemma OAI.HochschildNormalPart.normalOperator_norm line 298
  38. def OAI.HochschildNormalPart.operatorNormalPart line 313
  39. lemma OAI.HochschildNormalPart.operatorNormalPart_pairing line 319
  40. lemma OAI.HochschildNormalPart.operatorNormalPart_normal line 323
  41. lemma OAI.HochschildNormalPart.operatorNormalPart_fixes line 326
  42. lemma OAI.HochschildNormalPart.operatorNormalPart_comp_normal line 336
  43. lemma OAI.HochschildNormalPart.operatorNormalPart_comp_left line 350
  44. lemma OAI.HochschildNormalPart.operatorNormalPart_comp_right line 359