OAI/Analysis/BoundedHochschild/FiniteConstraints.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Finite cocycle constraints and exactness for bounded primitives.

  1. lemma OAI.BoundedHochschild.IsSupportProjection.smul line 33
  2. lemma OAI.BoundedHochschild.trace_mul_pow_swap line 45
  3. lemma OAI.BoundedHochschild.trace_one_sub_pow line 51
  4. lemma OAI.BoundedHochschild.support_trace_eq_of_moments line 63
  5. theorem OAI.BoundedHochschild.support_trace_star_mul_self line 90
  6. lemma OAI.BoundedHochschild.IsSupportProjection.star_mul_self_right line 112
  7. lemma OAI.BoundedHochschild.IsSupportProjection.mul_star_self_left line 123
  8. lemma OAI.BoundedHochschild.IsSupportProjection.left_le line 143
  9. lemma OAI.BoundedHochschild.IsSupportProjection.right_le line 151
  10. theorem OAI.BoundedHochschild.exists_projection_join line 160
  11. lemma OAI.BoundedHochschild.exists_monotone_projection_limit line 218
  12. lemma OAI.BoundedHochschild.exists_projection_finjoin line 251
  13. theorem OAI.BoundedHochschild.exists_projection_countable_join line 277
  14. lemma OAI.BoundedHochschild.trace_star_mul_self_re line 312
  15. theorem OAI.BoundedHochschild.exists_spectral_cut line 320
  16. theorem OAI.BoundedHochschild.exists_small_two_sided_support line 383