OAI/Analysis/BoundedHochschild/MomentNorms.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Recovery of operator norms from moments and free-word boundary decompositions.

  1. lemma OAI.HochschildMoments.norm_le_of_positive_moment_bound line 15
  2. lemma OAI.HochschildMoments.positive_moment_le_norm_pow line 83
  3. theorem OAI.HochschildMoments.norm_eq_of_positive_moments line 95
  4. theorem OAI.HochschildMoments.norm_eq_of_star_mul_moments line 112
  5. theorem OAI.HochschildFreeWords.boundary_decomposition line 128
  6. theorem OAI.HochschildFreeWords.boundary_reduction line 161
  7. abbrev OAI.HochschildLength.Vector line 181
  8. lemma OAI.HochschildLength.norm_sum_single_sq line 183
  9. lemma OAI.HochschildLength.norm_sum_mul_sq_le line 204
  10. lemma OAI.HochschildLength.block_matrix_bound line 214
  11. lemma OAI.HochschildLength.masked_block_matrix_bound line 228