OAI/Analysis/BoundedHochschild/StarPreduals.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Weak-star continuity of the involution and its predual action.

  1. lemma OAI.HochschildSakai.imag_square line 29
  2. lemma OAI.HochschildSakai.norm_one_bound line 41
  3. lemma OAI.HochschildSakai.norm_imag_add_sq line 46
  4. lemma OAI.HochschildSakai.imag_linear_bound line 56
  5. theorem OAI.HochschildSakai.isSelfAdjoint_of_norm_imag_add line 68
  6. theorem OAI.HochschildSakai.isSelfAdjoint_of_predual_tendsto line 119
  7. lemma OAI.HochschildSakai.star_eq_of_sum_sub_selfAdjoint line 141
  8. theorem OAI.HochschildSakai.predual_tendsto_star_bounded line 160
  9. theorem OAI.HochschildSakai.mem_predual_of_bounded_weak_continuity line 197
  10. theorem OAI.HochschildSakai.exists_star_predual_vector line 288
  11. theorem OAI.HochschildSakai.predual_tendsto_star line 318